Bounded lattices

This file defines top and bottom elements (greatest and least elements) of a type, the bounded variants of different kinds of lattices, sets up the typeclass hierarchy between them, and provides instances for Prop and fun.

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} [SemilatticeSup α] [OrderTop α] (a : α) : ⊤ ⊔ a = ⊤

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

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

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

@[simp]

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

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

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

@[simp]

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

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

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

In this section we prove some properties about monotone and antitone operations on Prop

theorem exists_ge_and_iff_exists {α : Type u} [SemilatticeSup α] {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∃ (x : α), x₀ ≤ x ∧ P x) ↔ ∃ (x : α), P x

theorem exists_and_iff_of_monotone {α : Type u} [SemilatticeSup α] {P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) : ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

theorem exists_le_and_iff_exists {α : Type u} [SemilatticeInf α] {P : α → Prop} {x₀ : α} (hP : Antitone P) : (∃ (x : α), x ≤ x₀ ∧ P x) ↔ ∃ (x : α), P x

theorem exists_and_iff_of_antitone {α : Type u} [SemilatticeInf α] {P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) : ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Induction on WellFoundedGT and WellFoundedLT

theorem WellFoundedGT.induction_top {α : Type u} [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} [Preorder α] [WellFoundedLT α] [OrderBot α] {P : α → Prop} (hexists : ∃ (M : α), P M) (hind : ∀ (N : α), N ≠ ⊥ → P N → ∃ (M : α), M < N ∧ P M) : P ⊥