Complete lattice algebra

The laws of ⊤, ⊥, ⊓, ⊔, ⨅ and ⨆ at an abstract carrier: the order laws, the units, the monoid laws of ⊓ and ⊔, monotonicity, and the characterizations of ⊑ against the connectives.

theorem Lean.Order.le_top {α : Type uₗ} [CompleteLattice α] (x : α) : PartialOrder.rel x top

theorem Lean.Order.meet_le_left {α : Type uₗ} [CompleteLattice α] (x y : α) : PartialOrder.rel (meet x y) x

theorem Lean.Order.meet_le_right {α : Type uₗ} [CompleteLattice α] (x y : α) : PartialOrder.rel (meet x y) y

theorem Lean.Order.le_meet {α : Type uₗ} [CompleteLattice α] (x y z : α) : PartialOrder.rel x y → PartialOrder.rel x z → PartialOrder.rel x (meet y z)

theorem Lean.Order.left_le_join {α : Type uₗ} [CompleteLattice α] (x y : α) : PartialOrder.rel x (join x y)

theorem Lean.Order.right_le_join {α : Type uₗ} [CompleteLattice α] (x y : α) : PartialOrder.rel y (join x y)

theorem Lean.Order.join_le {α : Type uₗ} [CompleteLattice α] (x y z : α) : PartialOrder.rel x z → PartialOrder.rel y z → PartialOrder.rel (join x y) z

theorem Lean.Order.iInf_le {α : Type uₗ} [CompleteLattice α] {ι : Sort vₗ} (f : ι → α) (i : ι) : PartialOrder.rel (iInf f) (f i)

theorem Lean.Order.le_iInf {α : Type uₗ} [CompleteLattice α] {ι : Sort vₗ} (f : ι → α) (x : α) : (∀ (i : ι), PartialOrder.rel x (f i)) → PartialOrder.rel x (iInf f)

theorem Lean.Order.le_iSup {α : Type uₗ} [CompleteLattice α] {ι : Sort vₗ} (f : ι → α) (i : ι) : PartialOrder.rel (f i) (iSup f)

theorem Lean.Order.iSup_le {α : Type uₗ} [CompleteLattice α] {ι : Sort vₗ} (f : ι → α) (x : α) : (∀ (i : ι), PartialOrder.rel (f i) x) → PartialOrder.rel (iSup f) x

Derived laws of CompleteLattice

Lattice algebra derived from the laws of CompleteLattice: monotonicity of the connectives, the monoid laws of ⊓ and ⊔ with their units ⊤ and ⊥, and the characterizations of ⊑ against ⊤, ⊥, ⊓, ⊔, ⨅ and ⨆.

Connectives

theorem Lean.Order.le_meet_left {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) : PartialOrder.rel P (meet Q P)

theorem Lean.Order.le_meet_right {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) : PartialOrder.rel P (meet P Q)

theorem Lean.Order.le_meet_of_eq {l : Type uₗ} [CompleteLattice l] {P Q R T : l} (hand : T = meet Q R) (hQ : PartialOrder.rel P Q) (hR : PartialOrder.rel P R) : PartialOrder.rel P T

theorem Lean.Order.meet_le_of_left_le {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P R) : PartialOrder.rel (meet P Q) R

theorem Lean.Order.meet_le_of_right_le {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel Q R) : PartialOrder.rel (meet P Q) R

theorem Lean.Order.le_join_of_le_left {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P Q) : PartialOrder.rel P (join Q R)

theorem Lean.Order.le_join_of_le_right {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h : PartialOrder.rel P R) : PartialOrder.rel P (join Q R)

theorem Lean.Order.meet_le_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel (meet P Q) (meet Q P)

theorem Lean.Order.join_le_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel (join P Q) (join Q P)

theorem Lean.Order.le_of_le_of_meet_le {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h₁ : PartialOrder.rel P Q) (h₂ : PartialOrder.rel (meet P Q) R) : PartialOrder.rel P R

theorem Lean.Order.le_iSup_of_le {l : Type uₗ} [CompleteLattice l] {P : l} {β : Sort u_1} {Ψ : β → l} (a : β) (h : PartialOrder.rel P (Ψ a)) : PartialOrder.rel P (iSup Ψ)

theorem Lean.Order.le_of_le_bot {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P bot) : PartialOrder.rel P Q

Monotonicity

theorem Lean.Order.meet_mono {l : Type uₗ} [CompleteLattice l] {P P' Q Q' : l} (hp : PartialOrder.rel P P') (hq : PartialOrder.rel Q Q') : PartialOrder.rel (meet P Q) (meet P' Q')

theorem Lean.Order.meet_mono_left {l : Type uₗ} [CompleteLattice l] {P P' Q : l} (h : PartialOrder.rel P P') : PartialOrder.rel (meet P Q) (meet P' Q)

theorem Lean.Order.meet_mono_right {l : Type uₗ} [CompleteLattice l] {P Q Q' : l} (h : PartialOrder.rel Q Q') : PartialOrder.rel (meet P Q) (meet P Q')

theorem Lean.Order.join_mono {l : Type uₗ} [CompleteLattice l] {P P' Q Q' : l} (hp : PartialOrder.rel P P') (hq : PartialOrder.rel Q Q') : PartialOrder.rel (join P Q) (join P' Q')

theorem Lean.Order.join_mono_left {l : Type uₗ} [CompleteLattice l] {P P' Q : l} (h : PartialOrder.rel P P') : PartialOrder.rel (join P Q) (join P' Q)

theorem Lean.Order.join_mono_right {l : Type uₗ} [CompleteLattice l] {P Q Q' : l} (h : PartialOrder.rel Q Q') : PartialOrder.rel (join P Q) (join P Q')

theorem Lean.Order.iInf_mono {l : Type uₗ} [CompleteLattice l] {β : Sort u_1} {Φ Ψ : β → l} (h : ∀ (a : β), PartialOrder.rel (Φ a) (Ψ a)) : PartialOrder.rel (iInf Φ) (iInf Ψ)

theorem Lean.Order.iSup_mono {l : Type uₗ} [CompleteLattice l] {β : Sort u_1} {Φ Ψ : β → l} (h : ∀ (a : β), PartialOrder.rel (Φ a) (Ψ a)) : PartialOrder.rel (iSup Φ) (iSup Ψ)

Boolean algebra

theorem Lean.Order.meet_self {l : Type uₗ} [CompleteLattice l] {P : l} : meet P P = P

theorem Lean.Order.join_self {l : Type uₗ} [CompleteLattice l] {P : l} : join P P = P

theorem Lean.Order.meet_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} : meet P Q = meet Q P

theorem Lean.Order.join_comm {l : Type uₗ} [CompleteLattice l] {P Q : l} : join P Q = join Q P

theorem Lean.Order.meet_assoc {l : Type uₗ} [CompleteLattice l] {P Q R : l} : meet (meet P Q) R = meet P (meet Q R)

theorem Lean.Order.join_assoc {l : Type uₗ} [CompleteLattice l] {P Q R : l} : join (join P Q) R = join P (join Q R)

theorem Lean.Order.le_iff_meet_eq_right {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel P Q ↔ meet Q P = P

theorem Lean.Order.le_iff_meet_eq_left {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel P Q ↔ meet P Q = P

theorem Lean.Order.le_iff_join_eq_left {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel P Q ↔ join Q P = Q

theorem Lean.Order.le_iff_join_eq_right {l : Type uₗ} [CompleteLattice l] {P Q : l} : PartialOrder.rel P Q ↔ join P Q = Q

@[simp]

theorem Lean.Order.top_meet {l : Type uₗ} [CompleteLattice l] {P : l} : meet top P = P

@[simp]

theorem Lean.Order.meet_top {l : Type uₗ} [CompleteLattice l] {P : l} : meet P top = P

theorem Lean.Order.meet_top_le_of_le {l : Type uₗ} [CompleteLattice l] {P Q : l} (h : PartialOrder.rel P Q) : PartialOrder.rel (meet P top) Q

Cancel a redundant ⊓ ⊤ on the left of an entailment.

@[simp]

theorem Lean.Order.bot_meet {l : Type uₗ} [CompleteLattice l] {P : l} : meet bot P = bot

@[simp]

theorem Lean.Order.meet_bot {l : Type uₗ} [CompleteLattice l] {P : l} : meet P bot = bot

@[simp]

theorem Lean.Order.top_join {l : Type uₗ} [CompleteLattice l] {P : l} : join top P = top

@[simp]

theorem Lean.Order.join_top {l : Type uₗ} [CompleteLattice l] {P : l} : join P top = top

@[simp]

theorem Lean.Order.bot_join {l : Type uₗ} [CompleteLattice l] {P : l} : join bot P = P

@[simp]

theorem Lean.Order.join_bot {l : Type uₗ} [CompleteLattice l] {P : l} : join P bot = P

@[simp]

theorem Lean.Order.iSup_bot {l : Type uₗ} [CompleteLattice l] {ι : Type u_1} : (iSup fun (x : ι) => bot) = bot

@[simp]

theorem Lean.Order.iInf_top {l : Type uₗ} [CompleteLattice l] {ι : Type u_1} : (iInf fun (x : ι) => top) = top

Miscellaneous

theorem Lean.Order.meet_left_comm {l : Type uₗ} [CompleteLattice l] {P Q R : l} : meet P (meet Q R) = meet Q (meet P R)

theorem Lean.Order.meet_right_comm {l : Type uₗ} [CompleteLattice l] {P Q R : l} : meet (meet P Q) R = meet (meet P R) Q

Working with entailment

@[simp]

theorem Lean.Order.le_top_iff {l : Type uₗ} [CompleteLattice l] {Q : l} : PartialOrder.rel Q top ↔ True

@[simp]

theorem Lean.Order.bot_le_iff {l : Type uₗ} [CompleteLattice l] {Q : l} : PartialOrder.rel bot Q ↔ True

@[simp]

theorem Lean.Order.join_le_iff {l : Type uₗ} [CompleteLattice l] {P Q R : l} : PartialOrder.rel (join P Q) R ↔ PartialOrder.rel P R ∧ PartialOrder.rel Q R

@[simp]

theorem Lean.Order.le_meet_iff {l : Type uₗ} [CompleteLattice l] {P Q R : l} : PartialOrder.rel P (meet Q R) ↔ PartialOrder.rel P Q ∧ PartialOrder.rel P R

@[simp]

theorem Lean.Order.iSup_le_iff {l : Type uₗ} [CompleteLattice l] {P : l} {ι : Type u_1} {Φ : ι → l} : PartialOrder.rel (iSup Φ) P ↔ ∀ (i : ι), PartialOrder.rel (Φ i) P

@[simp]

theorem Lean.Order.le_iInf_iff {l : Type uₗ} [CompleteLattice l] {P : l} {ι : Type u_1} {Φ : ι → l} : PartialOrder.rel P (iInf Φ) ↔ ∀ (i : ι), PartialOrder.rel P (Φ i)

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

theorem Lean.Order.le_trans_meet {l : Type uₗ} [CompleteLattice l] {P Q R : l} (h₁ : PartialOrder.rel P Q) (h₂ : PartialOrder.rel (meet P Q) R) : PartialOrder.rel P R