Mathlib.Order.BoundedOrder.Lattice

Module docstring

{"# 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 ","#### In this section we prove some properties about monotone and antitone operations on Prop "}

top_sup_eq theorem

(a : α) : ⊤ ⊔ a = ⊤

Full source

theorem top_sup_eq (a : α) : ⊤⊤ ⊔ a = ⊤ :=
  sup_of_le_left le_top

Supremum with Top Element is Top

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the supremum of $\top$ and $a$ is equal to $\top$, i.e., $\top \sqcup a = \top$.

sup_top_eq theorem

(a : α) : a ⊔ ⊤ = ⊤

Full source

theorem sup_top_eq (a : α) : a ⊔ ⊤ = ⊤ :=
  sup_of_le_right le_top

Supremum with Top Element Yields Top

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the supremum of $a$ and $\top$ equals $\top$, i.e., $a \sqcup \top = \top$.

bot_sup_eq theorem

(a : α) : ⊥ ⊔ a = a

Full source

theorem bot_sup_eq (a : α) : ⊥⊥ ⊔ a = a :=
  sup_of_le_right bot_le

Bottom Element Absorbs in Supremum

Informal description

For any element $a$ in a lattice with a bottom element $\bot$, the supremum of $\bot$ and $a$ equals $a$, i.e., $\bot \sqcup a = a$.

sup_bot_eq theorem

(a : α) : a ⊔ ⊥ = a

Full source

theorem sup_bot_eq (a : α) : a ⊔ ⊥ = a :=
  sup_of_le_left bot_le

Supremum with Bottom Element

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the supremum of $a$ and $\bot$ is equal to $a$, i.e., $a \sqcup \bot = a$.

sup_eq_bot_iff theorem

: a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Full source

@[simp]
theorem sup_eq_bot_iff : a ⊔ ba ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥ := by rw [eq_bot_iff, sup_le_iff]; simp

Supremum Equals Bottom iff Both Elements Are Bottom

Informal description

For any elements $a$ and $b$ in a lattice with a bottom element $\bot$, the supremum $a \sqcup b$ equals $\bot$ if and only if both $a$ and $b$ equal $\bot$.

top_inf_eq theorem

(a : α) : ⊤ ⊓ a = a

Full source

lemma top_inf_eq (a : α) : ⊤⊤ ⊓ a = a := inf_of_le_right le_top

Infimum with Top Element: $\top \sqcap a = a$

Informal description

For any element $a$ in a lattice with a top element $\top$, the infimum of $\top$ and $a$ is equal to $a$, i.e., $\top \sqcap a = a$.

inf_top_eq theorem

(a : α) : a ⊓ ⊤ = a

Full source

lemma inf_top_eq (a : α) : a ⊓ ⊤ = a := inf_of_le_left le_top

Infimum with Top Element is Identity

Informal description

For any element $a$ in a bounded lattice $\alpha$, the infimum of $a$ and the top element $\top$ is equal to $a$, i.e., $a \sqcap \top = a$.

inf_eq_top_iff theorem

: a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤

Full source

@[simp]
theorem inf_eq_top_iff : a ⊓ ba ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤ :=
  @sup_eq_bot_iff αᵒᵈ _ _ _ _

Infimum Equals Top iff Both Elements Are Top

Informal description

For any elements $a$ and $b$ in a lattice with a top element $\top$, the infimum $a \sqcap b$ equals $\top$ if and only if both $a$ and $b$ equal $\top$.

bot_inf_eq theorem

(a : α) : ⊥ ⊓ a = ⊥

Full source

lemma bot_inf_eq (a : α) : ⊥⊥ ⊓ a = ⊥ := inf_of_le_left bot_le

Infimum with Bottom Element is Bottom

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the infimum of $\bot$ and $a$ equals $\bot$, i.e., $\bot \sqcap a = \bot$.

inf_bot_eq theorem

(a : α) : a ⊓ ⊥ = ⊥

Full source

lemma inf_bot_eq (a : α) : a ⊓ ⊥ = ⊥ := inf_of_le_right bot_le

Infimum with Bottom Element Yields Bottom

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the infimum of $a$ and $\bot$ is equal to $\bot$, i.e., $a \sqcap \bot = \bot$.

exists_ge_and_iff_exists theorem

{P : α → Prop} {x₀ : α} (hP : Monotone P) : (∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x

Full source

theorem exists_ge_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Monotone P) :
    (∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x :=
  ⟨fun h => h.imp fun _ h => h.2, fun ⟨x, hx⟩ => ⟨x ⊔ x₀, le_sup_right, hP le_sup_left hx⟩⟩

Existence of Greater Element with Monotone Predicate is Equivalent to Existence

Informal description

Let $P$ be a monotone predicate on a type $\alpha$ with a partial order, and let $x_0 \in \alpha$. Then the existence of an element $x$ such that $x_0 \leq x$ and $P(x)$ holds is equivalent to the existence of some element $x$ for which $P(x)$ holds. In other words: $$(\exists x, x_0 \leq x \land P(x)) \leftrightarrow (\exists x, P(x))$$

exists_and_iff_of_monotone theorem

{P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) : ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x)

Full source

lemma exists_and_iff_of_monotone {P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) :
    ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
  ⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊔ y, ⟨hP le_sup_left hPx, hQ le_sup_right hQx⟩⟩,
    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩

Conjunction of Existential Quantifiers for Monotone Predicates is Equivalent to Existential Quantifier of Conjunction

Informal description

Let $P$ and $Q$ be monotone predicates on a partially ordered type $\alpha$. Then the conjunction of the existence of an element satisfying $P$ and the existence of an element satisfying $Q$ is equivalent to the existence of an element satisfying both $P$ and $Q$ simultaneously. In other words: $$(\exists x, P(x)) \land (\exists x, Q(x)) \leftrightarrow \exists x, P(x) \land Q(x)$$

exists_le_and_iff_exists theorem

{P : α → Prop} {x₀ : α} (hP : Antitone P) : (∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x

Full source

theorem exists_le_and_iff_exists {P : α → Prop} {x₀ : α} (hP : Antitone P) :
    (∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x :=
  exists_ge_and_iff_exists <| hP.dual_left

Existence of Lesser Element with Antitone Predicate is Equivalent to Existence

Informal description

Let $P$ be an antitone predicate on a type $\alpha$ with a partial order, and let $x_0 \in \alpha$. Then the existence of an element $x$ such that $x \leq x_0$ and $P(x)$ holds is equivalent to the existence of some element $x$ for which $P(x)$ holds. In other words: $$(\exists x, x \leq x_0 \land P(x)) \leftrightarrow (\exists x, P(x))$$

exists_and_iff_of_antitone theorem

{P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) : ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x)

Full source

lemma exists_and_iff_of_antitone {P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) :
    ((∃ x, P x) ∧ ∃ x, Q x) ↔ (∃ x, P x ∧ Q x) :=
  ⟨fun ⟨⟨x, hPx⟩, ⟨y, hQx⟩⟩ ↦ ⟨x ⊓ y, ⟨hP inf_le_left hPx, hQ inf_le_right hQx⟩⟩,
    fun ⟨x, hPx, hQx⟩ ↦ ⟨⟨x, hPx⟩, ⟨x, hQx⟩⟩⟩

Existence Conjunction for Antitone Predicates

Informal description

For any antitone predicates $P$ and $Q$ on a type $\alpha$, the conjunction of the existence of an $x$ satisfying $P(x)$ and the existence of an $x$ satisfying $Q(x)$ is equivalent to the existence of an $x$ satisfying both $P(x)$ and $Q(x)$. In symbols: $$(\exists x, P(x)) \land (\exists x, Q(x)) \leftrightarrow \exists x, P(x) \land Q(x)$$

min_bot_left theorem

[OrderBot α] (a : α) : min ⊥ a = ⊥

Full source

theorem min_bot_left [OrderBot α] (a : α) : min ⊥ a = ⊥ := bot_inf_eq _

Minimum with Bottom Element is Bottom

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the minimum of $\bot$ and $a$ equals $\bot$, i.e., $\min(\bot, a) = \bot$.

max_top_left theorem

[OrderTop α] (a : α) : max ⊤ a = ⊤

Full source

theorem max_top_left [OrderTop α] (a : α) : max ⊤ a = ⊤ := top_sup_eq _

Maximum with Top Element is Top

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the maximum of $\top$ and $a$ equals $\top$, i.e., $\max(\top, a) = \top$.

min_top_left theorem

[OrderTop α] (a : α) : min ⊤ a = a

Full source

theorem min_top_left [OrderTop α] (a : α) : min ⊤ a = a := top_inf_eq _

Minimum with Top Element: $\min(\top, a) = a$

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the minimum of $\top$ and $a$ equals $a$, i.e., $\min(\top, a) = a$.

max_bot_left theorem

[OrderBot α] (a : α) : max ⊥ a = a

Full source

theorem max_bot_left [OrderBot α] (a : α) : max ⊥ a = a := bot_sup_eq _

Maximum with Bottom Element is Identity

Informal description

In a lattice with a bottom element $\bot$, for any element $a$, the maximum of $\bot$ and $a$ equals $a$, i.e., $\max(\bot, a) = a$.

min_top_right theorem

[OrderTop α] (a : α) : min a ⊤ = a

Full source

theorem min_top_right [OrderTop α] (a : α) : min a ⊤ = a := inf_top_eq _

Minimum with Top Element is Identity

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the minimum of $a$ and $\top$ equals $a$, i.e., $\min(a, \top) = a$.

max_bot_right theorem

[OrderBot α] (a : α) : max a ⊥ = a

Full source

theorem max_bot_right [OrderBot α] (a : α) : max a ⊥ = a := sup_bot_eq _

Maximum with Bottom Element Equals Itself

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the maximum of $a$ and $\bot$ is equal to $a$, i.e., $\max(a, \bot) = a$.

min_bot_right theorem

[OrderBot α] (a : α) : min a ⊥ = ⊥

Full source

theorem min_bot_right [OrderBot α] (a : α) : min a ⊥ = ⊥ := inf_bot_eq _

Minimum with Bottom Element Yields Bottom

Informal description

For any element $a$ in a lattice $\alpha$ with a bottom element $\bot$, the minimum of $a$ and $\bot$ is equal to $\bot$, i.e., $\min(a, \bot) = \bot$.

max_top_right theorem

[OrderTop α] (a : α) : max a ⊤ = ⊤

Full source

theorem max_top_right [OrderTop α] (a : α) : max a ⊤ = ⊤ := sup_top_eq _

Maximum with Top Element Yields Top

Informal description

For any element $a$ in a lattice $\alpha$ with a top element $\top$, the maximum of $a$ and $\top$ equals $\top$, i.e., $\max(a, \top) = \top$.

max_eq_bot theorem

[OrderBot α] {a b : α} : max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Full source

theorem max_eq_bot [OrderBot α] {a b : α} : maxmax a b = ⊥ ↔ a = ⊥ ∧ b = ⊥ :=
  sup_eq_bot_iff

Characterization of when maximum equals bottom: $\max(a,b) = \bot \leftrightarrow a = \bot \land b = \bot$

Informal description

For any elements $a$ and $b$ in a lattice with a bottom element $\bot$, the maximum $\max(a, b)$ equals $\bot$ if and only if both $a = \bot$ and $b = \bot$.

min_eq_top theorem

[OrderTop α] {a b : α} : min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤

Full source

theorem min_eq_top [OrderTop α] {a b : α} : minmin a b = ⊤ ↔ a = ⊤ ∧ b = ⊤ :=
  inf_eq_top_iff

Characterization of when minimum equals top: $\min(a,b) = \top \leftrightarrow a = \top \land b = \top$

Informal description

For any elements $a$ and $b$ in a lattice $\alpha$ with a top element $\top$, the minimum $\min(a, b)$ equals $\top$ if and only if both $a = \top$ and $b = \top$.

min_eq_bot theorem

[OrderBot α] {a b : α} : min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Full source

@[simp]
theorem min_eq_bot [OrderBot α] {a b : α} : minmin a b = ⊥ ↔ a = ⊥ ∨ b = ⊥ := by
  simp_rw [← le_bot_iff, inf_le_iff]

Characterization of when minimum equals bottom: $\min(a,b) = \bot \leftrightarrow a = \bot \lor b = \bot$

Informal description

Let $\alpha$ be a type with a bottom element $\bot$ (i.e., an instance of `OrderBot α`). For any elements $a, b \in \alpha$, the minimum of $a$ and $b$ equals $\bot$ if and only if either $a = \bot$ or $b = \bot$.

max_eq_top theorem

[OrderTop α] {a b : α} : max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Full source

@[simp]
theorem max_eq_top [OrderTop α] {a b : α} : maxmax a b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
  @min_eq_bot αᵒᵈ _ _ a b

Characterization of when maximum equals top: $\max(a,b) = \top \leftrightarrow a = \top \lor b = \top$

Informal description

Let $\alpha$ be a type with a top element $\top$ (i.e., an instance of `OrderTop α`). For any elements $a, b \in \alpha$, the maximum of $a$ and $b$ equals $\top$ if and only if either $a = \top$ or $b = \top$.