Bounded lattices

This file contains miscellaneous lemmas about lattices with top or bottom elements.

Common lattices

• Distributive lattices with a bottom element. Notated by [DistribLattice α] [OrderBot α]. It captures the properties of Disjoint that are common to GeneralizedBooleanAlgebra and DistribLattice when OrderBot.
• Bounded and distributive lattice. Notated by [DistribLattice α] [BoundedOrder α]. Typical examples include Prop and Set α.

Top, bottom element

theorem top_sup_eq {α : Type u_1} [SemilatticeSup α] [OrderTop α] (a : α) : ⊤ ⊔ a = ⊤

theorem bot_inf_eq {α : Type u_1} [SemilatticeInf α] [OrderBot α] (a : α) : ⊥ ⊓ a = ⊥

theorem sup_top_eq {α : Type u_1} [SemilatticeSup α] [OrderTop α] (a : α) : a ⊔ ⊤ = ⊤

theorem inf_bot_eq {α : Type u_1} [SemilatticeInf α] [OrderBot α] (a : α) : a ⊓ ⊥ = ⊥

theorem bot_sup_eq {α : Type u_1} [SemilatticeSup α] [OrderBot α] (a : α) : ⊥ ⊔ a = a

theorem top_inf_eq {α : Type u_1} [SemilatticeInf α] [OrderTop α] (a : α) : ⊤ ⊓ a = a

theorem sup_bot_eq {α : Type u_1} [SemilatticeSup α] [OrderBot α] (a : α) : a ⊔ ⊥ = a

theorem inf_top_eq {α : Type u_1} [SemilatticeInf α] [OrderTop α] (a : α) : a ⊓ ⊤ = a

@[simp]

theorem sup_eq_bot_iff {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a b : α} : a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

@[simp]

theorem inf_eq_top_iff {α : Type u_1} [SemilatticeInf α] [OrderTop α] {a b : α} : a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤

theorem min_bot_left {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : min ⊥ a = ⊥

theorem max_top_left {α : Type u_1} [LinearOrder α] [OrderTop α] (a : α) : max ⊤ a = ⊤

theorem min_bot_right {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : min a ⊥ = ⊥

theorem max_top_right {α : Type u_1} [LinearOrder α] [OrderTop α] (a : α) : max a ⊤ = ⊤

theorem max_bot_left {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : max ⊥ a = a

theorem min_top_left {α : Type u_1} [LinearOrder α] [OrderTop α] (a : α) : min ⊤ a = a

theorem max_bot_right {α : Type u_1} [LinearOrder α] [OrderBot α] (a : α) : max a ⊥ = a

theorem min_top_right {α : Type u_1} [LinearOrder α] [OrderTop α] (a : α) : min a ⊤ = a

theorem max_eq_bot {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥

theorem min_eq_top {α : Type u_1} [LinearOrder α] [OrderTop α] {a b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤

@[simp]

theorem min_eq_bot {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

@[simp]

theorem max_eq_top {α : Type u_1} [LinearOrder α] [OrderTop α] {a b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤

theorem min_ne_bot {α : Type u_1} [LinearOrder α] [OrderBot α] {a b : α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : min a b ≠ ⊥

theorem max_ne_top {α : Type u_1} [LinearOrder α] [OrderTop α] {a b : α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : max a b ≠ ⊤

Induction on WellFoundedGT and WellFoundedLT

theorem WellFoundedGT.induction_top {α : Type u_1} [Preorder α] [WellFoundedGT α] [OrderTop α] {P : α → Prop} (hexists : ∃ (M : α), P M) (hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M) : P ⊤

theorem WellFoundedLT.induction_bot {α : Type u_1} [Preorder α] [WellFoundedLT α] [OrderBot α] {P : α → Prop} (hexists : ∃ (M : α), P M) (hind : ∀ (N : α), N ≠ ⊥ → P N → ∃ (M : α), N > M ∧ P M) : P ⊥