Projections of lattice operations

The lattice operations on functions, pairs and PProd are pointwise and componentwise: applying a function or projecting a component commutes with ⊤, ⊥, ⊓, ⊔, ⨅, ⨆, ⌜·⌝ and ⇨, and ⊑ on functions and pairs is pointwise and componentwise.

Functions

@[simp]

theorem Lean.Order.iInf_apply {ι : Sort vₗ} {σ : Type wₗ} {β : Type uₗ} [CompleteLattice β] (f : ι → σ → β) (s : σ) : iInf f s = iInf fun (i : ι) => f i s

Pointwise characterization of indexed infimum on function lattices.

@[simp]

theorem Lean.Order.iSup_apply {ι : Sort vₗ} {σ : Type wₗ} {β : Type uₗ} [CompleteLattice β] (f : ι → σ → β) (s : σ) : iSup f s = iSup fun (i : ι) => f i s

Pointwise characterization of indexed supremum on function lattices.

theorem Lean.Order.sup_apply {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → CompleteLattice (β s)] (c : ((s : σ) → β s) → Prop) (s : σ) : CompleteLattice.sup c s = CompleteLattice.sup fun (y : β s) => ∃ (f : (s : σ) → β s), c f ∧ f s = y

Pointwise characterization of CompleteLattice.sup on function lattices: (sup c) s = sup (fun y => ∃ f, c f ∧ f s = y).

@[simp]

theorem Lean.Order.meet_apply {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → CompleteLattice (β s)] (a b : (s : σ) → β s) (s : σ) : meet a b s = meet (a s) (b s)

Pointwise characterization of binary meet on function lattices.

@[simp]

theorem Lean.Order.join_apply {σ : Type vₗ} {β : Type wₗ} [CompleteLattice β] (a b : σ → β) (s : σ) : join a b s = join (a s) (b s)

Pointwise characterization of binary join on function lattices.

@[simp]

theorem Lean.Order.top_apply {σ : Type vₗ} {β : Type wₗ} [CompleteLattice β] (s : σ) : top s = top

Pointwise characterization of ⊤ on a function lattice.

@[simp]

theorem Lean.Order.bot_apply {σ : Type vₗ} {β : Type wₗ} [CCPO β] (s : σ) : bot s = bot

Pointwise characterization of ⊥ on a function lattice.

theorem Lean.Order.le_pi_eq_forall {σ : Type vₗ} {β : σ → Type wₗ} [(s : σ) → PartialOrder (β s)] (a b : (s : σ) → β s) : PartialOrder.rel a b = ∀ (s : σ), PartialOrder.rel (a s) (b s)

Entailment on a function lattice is pointwise.

theorem Lean.Order.le_prod_eq_and {α : Type vₗ} {β : Type wₗ} [PartialOrder α] [PartialOrder β] (a b : α × β) : PartialOrder.rel a b = (PartialOrder.rel a.fst b.fst ∧ PartialOrder.rel a.snd b.snd)

Entailment on a pair lattice is componentwise.

theorem Lean.Order.le_of_forall_le {σ : Type uₗ} {β : Type vₗ} [PartialOrder β] {f g : σ → β} : (∀ (s : σ), PartialOrder.rel (f s) (g s)) → PartialOrder.rel f g

Entailment between functions follows from pointwise entailment.

theorem Lean.Order.top_le_of_forall_top_le {σ : Type uₗ} {β : Type vₗ} [CompleteLattice β] {g : σ → β} : (∀ (s : σ), PartialOrder.rel top (g s)) → PartialOrder.rel top g

⊤ ⊑ g for a function g follows from pointwise ⊤ ⊑ g s.

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le {σ : Type uₗ} {β : Type vₗ} [PartialOrder β] {f g : σ → β} : PartialOrder.rel f g ↔ ∀ (s : σ), PartialOrder.rel (f s) (g s)

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le_1 {l : Type uₗ} [CompleteLattice l] {σ : Type vₗ} {P Q : σ → l} : PartialOrder.rel P Q ↔ ∀ (s : σ), PartialOrder.rel (P s) (Q s)

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le_2 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ : Type vₗ} {P Q : σ₁ → σ₂ → l} : PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂), PartialOrder.rel (P s₁ s₂) (Q s₁ s₂)

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le_3 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → l} : PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), PartialOrder.rel (P s₁ s₂ s₃) (Q s₁ s₂ s₃)

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le_4 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → l} : PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄), PartialOrder.rel (P s₁ s₂ s₃ s₄) (Q s₁ s₂ s₃ s₄)

@[deprecated Lean.Order.le_pi_eq_forall (since := "2026-09-24")]

theorem Lean.Order.le_iff_forall_le_5 {l : Type uₗ} [CompleteLattice l] {σ₁ σ₂ σ₃ σ₄ σ₅ : Type vₗ} {P Q : σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → l} : PartialOrder.rel P Q ↔ ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅), PartialOrder.rel (P s₁ s₂ s₃ s₄ s₅) (Q s₁ s₂ s₃ s₄ s₅)

@[simp]

theorem Lean.Order.CompleteLattice.ofProp_apply {σ : Type v} {β : Type u} [CompleteLattice β] (p : Prop) (s : σ) : ofProp p s = ofProp p

Pointwise characterization of CompleteLattice.ofProp on a function lattice.

@[deprecated Lean.Order.CompleteLattice.ofProp_apply (since := "2026-09-24")]

theorem Lean.Order.CompleteLattice.ofProp_apply_1 {σ1 : Type u_1} (p : Prop) (s1 : σ1) : ofProp p s1 = p

@[deprecated Lean.Order.CompleteLattice.ofProp_apply (since := "2026-09-24")]

theorem Lean.Order.CompleteLattice.ofProp_apply_2 {σ1 : Type u_1} {σ2 : Type u_2} (p : Prop) (s1 : σ1) (s2 : σ2) : ofProp p s1 s2 = p

@[deprecated Lean.Order.CompleteLattice.ofProp_apply (since := "2026-09-24")]

theorem Lean.Order.CompleteLattice.ofProp_apply_3 {σ1 : Type u_1} {σ2 : Type u_2} {σ3 : Type u_3} (p : Prop) (s1 : σ1) (s2 : σ2) (s3 : σ3) : ofProp p s1 s2 s3 = p

@[deprecated Lean.Order.CompleteLattice.ofProp_apply (since := "2026-09-24")]

theorem Lean.Order.CompleteLattice.ofProp_apply_4 {σ1 : Type u_1} {σ2 : Type u_2} {σ3 : Type u_3} {σ4 : Type u_4} (p : Prop) (s1 : σ1) (s2 : σ2) (s3 : σ3) (s4 : σ4) : ofProp p s1 s2 s3 s4 = p

@[deprecated Lean.Order.CompleteLattice.ofProp_apply (since := "2026-09-24")]

theorem Lean.Order.CompleteLattice.ofProp_apply_5 {σ1 : Type u_1} {σ2 : Type u_2} {σ3 : Type u_3} {σ4 : Type u_4} {σ5 : Type u_5} (p : Prop) (s1 : σ1) (s2 : σ2) (s3 : σ3) (s4 : σ4) (s5 : σ5) : ofProp p s1 s2 s3 s4 s5 = p

@[simp]

theorem Lean.Order.himp_apply {σ : Type v} {β : Type u} [CompleteLattice β] (a b : σ → β) (s : σ) : himp a b s = himp (a s) (b s)

Pointwise characterization of Heyting implication on function lattices.

PProd

theorem Lean.Order.PProd.mk_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α ×' β) : ⟨meet p.fst q.fst, meet p.snd q.snd⟩ = meet p q

mk of the componentwise meets is the meet on a product.

theorem Lean.Order.PProd.mk_sup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (c : α ×' β → Prop) : ⟨CompleteLattice.sup fun (a : α) => ∃ (b : β), c ⟨a, b⟩, CompleteLattice.sup fun (b : β) => ∃ (a : α), c ⟨a, b⟩⟩ = CompleteLattice.sup c

mk of the componentwise least upper bounds is the least upper bound on a product.

Pairs

theorem Lean.Order.Prod.mk_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p.fst q.fst, meet p.snd q.snd) = meet p q

mk of the componentwise meets is the meet on a product.

@[simp]

theorem Lean.Order.Prod.fst_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p q).fst = meet p.fst q.fst

The first component of a meet is the meet of the first components.

@[simp]

theorem Lean.Order.Prod.snd_meet {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (meet p q).snd = meet p.snd q.snd

The second component of a meet is the meet of the second components.

@[simp]

theorem Lean.Order.Prod.fst_join {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (join p q).fst = join p.fst q.fst

@[simp]

theorem Lean.Order.Prod.snd_join {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (p q : α × β) : (join p q).snd = join p.snd q.snd

@[simp]

theorem Lean.Order.Prod.fst_iSup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] {ι : Type w} (f : ι → α × β) : (iSup f).fst = iSup fun (i : ι) => (f i).fst

@[simp]

theorem Lean.Order.Prod.snd_iSup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] {ι : Type w} (f : ι → α × β) : (iSup f).snd = iSup fun (i : ι) => (f i).snd

@[simp]

theorem Lean.Order.Prod.fst_iInf {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] {ι : Type w} (f : ι → α × β) : (iInf f).fst = iInf fun (i : ι) => (f i).fst

@[simp]

theorem Lean.Order.Prod.snd_iInf {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] {ι : Type w} (f : ι → α × β) : (iInf f).snd = iInf fun (i : ι) => (f i).snd

theorem Lean.Order.Prod.mk_sup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (c : α × β → Prop) : (CompleteLattice.sup fun (a : α) => ∃ (b : β), c (a, b), CompleteLattice.sup fun (b : β) => ∃ (a : α), c (a, b)) = CompleteLattice.sup c

theorem Lean.Order.Prod.fst_sup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (c : α × β → Prop) : (CompleteLattice.sup c).fst = CompleteLattice.sup fun (a : α) => ∃ (b : β), c (a, b)

theorem Lean.Order.Prod.snd_sup {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] (c : α × β → Prop) : (CompleteLattice.sup c).snd = CompleteLattice.sup fun (b : β) => ∃ (a : α), c (a, b)

@[simp]

theorem Lean.Order.Prod.fst_bot {α : Type u} {β : Type v} [CCPO α] [CCPO β] : bot.fst = bot

The first component of the bottom element is the bottom element. Propositional (not definitional), because ⊥ is csup ∅, not a constructor application.

@[simp]

theorem Lean.Order.Prod.snd_bot {α : Type u} {β : Type v} [CCPO α] [CCPO β] : bot.snd = bot

The second component of the bottom element is the bottom element. Propositional (not definitional), because ⊥ is csup ∅, not a constructor application.

@[simp]

theorem Lean.Order.Prod.fst_top {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] : top.fst = top

The first component of the top element is the top element. Propositional (not definitional), because ⊤ is a supremum, not a constructor application.

@[simp]

theorem Lean.Order.Prod.snd_top {α : Type u} [CompleteLattice α] {β : Type v} [CompleteLattice β] : top.snd = top

The second component of the top element is the top element. Propositional (not definitional), because ⊤ is a supremum, not a constructor application.

@[simp]

theorem Lean.Order.Prod.fst_ofProp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (p : Prop) : (CompleteLattice.ofProp p).fst = CompleteLattice.ofProp p

@[simp]

theorem Lean.Order.Prod.snd_ofProp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (p : Prop) : (CompleteLattice.ofProp p).snd = CompleteLattice.ofProp p

@[simp]

theorem Lean.Order.Prod.fst_himp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (a b : α × β) : (himp a b).fst = himp a.fst b.fst

@[simp]

theorem Lean.Order.Prod.snd_himp {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] (a b : α × β) : (himp a b).snd = himp a.snd b.snd