Mathlib.Order.CompleteLattice.Defs

OrderDual.supSet instance

(α) [InfSet α] : SupSet αᵒᵈ

Full source

instance OrderDual.supSet (α) [InfSet α] : SupSet αᵒᵈ :=
  ⟨(sInf : Set α → α)⟩

Supremum Structure on Order Dual via Infimum

Informal description

For any type $\alpha$ equipped with an infimum operator $\bigwedge$, the order dual $\alpha^\text{op}$ is equipped with a supremum operator $\bigvee$ where $\bigvee s = \bigwedge s$ for any subset $s \subseteq \alpha^\text{op}$.

OrderDual.infSet instance

(α) [SupSet α] : InfSet αᵒᵈ

Full source

instance OrderDual.infSet (α) [SupSet α] : InfSet αᵒᵈ :=
  ⟨(sSup : Set α → α)⟩

Infimum Structure on Order Dual via Supremum

Informal description

For any type $\alpha$ equipped with a supremum operator $\bigvee$, the order dual $\alpha^\text{op}$ is equipped with an infimum operator $\bigwedge$ where $\bigwedge s = \bigvee s$ for any subset $s \subseteq \alpha^\text{op}$.

CompleteSemilatticeSup structure

(α : Type*) extends PartialOrder α, SupSet α

Full source

/-- Note that we rarely use `CompleteSemilatticeSup`
(in fact, any such object is always a `CompleteLattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.
-/
class CompleteSemilatticeSup (α : Type*) extends PartialOrder α, SupSet α where
  /-- Any element of a set is less than the set supremum. -/
  le_sSup : ∀ s, ∀ a ∈ s, a ≤ sSup s
  /-- Any upper bound is more than the set supremum. -/
  sSup_le : ∀ s a, (∀ b ∈ s, b ≤ a) → sSup s ≤ a

Complete Semilattice with Supremum

Informal description

A structure representing a complete semilattice with supremum, which is a partially ordered set equipped with a supremum operation for any subset. Specifically, it consists of a type $\alpha$ with a partial order and a supremum operation $\bigvee$ such that for any subset $s \subseteq \alpha$, $\bigvee s$ is the least upper bound of $s$.

le_sSup theorem

: a ∈ s → a ≤ sSup s

Full source

theorem le_sSup : a ∈ s → a ≤ sSup s :=
  CompleteSemilatticeSup.le_sSup s a

Element is Less Than or Equal to Supremum

Informal description

For any element $a$ in a subset $s$ of a complete semilattice with supremum, $a$ is less than or equal to the supremum of $s$, i.e., $a \leq \bigvee s$.

sSup_le theorem

: (∀ b ∈ s, b ≤ a) → sSup s ≤ a

Full source

theorem sSup_le : (∀ b ∈ s, b ≤ a) → sSup s ≤ a :=
  CompleteSemilatticeSup.sSup_le s a

Supremum is the Least Upper Bound

Informal description

For any subset $s$ of a complete semilattice with supremum and any element $a$, if every element $b \in s$ satisfies $b \leq a$, then the supremum of $s$ is less than or equal to $a$.

isLUB_sSup theorem

(s : Set α) : IsLUB s (sSup s)

Full source

theorem isLUB_sSup (s : Set α) : IsLUB s (sSup s) :=
  ⟨fun _ ↦ le_sSup, fun _ ↦ sSup_le⟩

Supremum is the Least Upper Bound

Informal description

For any subset $s$ of a complete semilattice with supremum, the supremum $\bigvee s$ is the least upper bound of $s$. That is, $\bigvee s$ is an upper bound for $s$ (i.e., $x \leq \bigvee s$ for all $x \in s$) and is less than or equal to any other upper bound of $s$.

isLUB_iff_sSup_eq theorem

: IsLUB s a ↔ sSup s = a

Full source

lemma isLUB_iff_sSup_eq : IsLUBIsLUB s a ↔ sSup s = a :=
  ⟨(isLUB_sSup s).unique, by rintro rfl; exact isLUB_sSup _⟩

Characterization of Least Upper Bound via Supremum Equality

Informal description

For any subset $s$ of a complete semilattice with supremum and any element $a$, the element $a$ is the least upper bound of $s$ if and only if the supremum of $s$ equals $a$. That is, $a$ is the least upper bound of $s$ precisely when $\bigvee s = a$.

le_sSup_of_le theorem

(hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s

Full source

theorem le_sSup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
  le_trans h (le_sSup hb)

Transitivity of Inequality with Supremum

Informal description

For any subset $s$ of a complete semilattice with supremum, if $b \in s$ and $a \leq b$, then $a \leq \bigvee s$.

sSup_le_sSup theorem

(h : s ⊆ t) : sSup s ≤ sSup t

Full source

@[gcongr]
theorem sSup_le_sSup (h : s ⊆ t) : sSup s ≤ sSup t :=
  (isLUB_sSup s).mono (isLUB_sSup t) h

Monotonicity of Supremum under Set Inclusion: $\bigvee s \leq \bigvee t$ when $s \subseteq t$

Informal description

For any subsets $s$ and $t$ of a complete semilattice with supremum, if $s \subseteq t$, then the supremum of $s$ is less than or equal to the supremum of $t$, i.e., $\bigvee s \leq \bigvee t$.

sSup_le_iff theorem

: sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

Full source

@[simp]
theorem sSup_le_iff : sSupsSup s ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  isLUB_le_iff (isLUB_sSup s)

Supremum Comparison Criterion: $\bigvee s \leq a \leftrightarrow \forall b \in s, b \leq a$

Informal description

For any subset $s$ of a complete semilattice with supremum and any element $a$, the supremum $\bigvee s$ is less than or equal to $a$ if and only if every element $b \in s$ satisfies $b \leq a$.

le_sSup_iff theorem

: a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

Full source

theorem le_sSup_iff : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b :=
  ⟨fun h _ hb => le_trans h (sSup_le hb), fun hb => hb _ fun _ => le_sSup⟩

Characterization of Supremum via Upper Bounds: $a \leq \bigvee s \leftrightarrow (\forall b \in \text{upperBounds}(s), a \leq b)$

Informal description

For any element $a$ in a complete semilattice with supremum and any subset $s$, $a$ is less than or equal to the supremum of $s$ if and only if $a$ is less than or equal to every upper bound of $s$. In other words, $a \leq \bigvee s \leftrightarrow \forall b \in \text{upperBounds}(s), a \leq b$.

le_iSup_iff theorem

{s : ι → α} : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b

Full source

theorem le_iSup_iff {s : ι → α} : a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b := by
  simp [iSup, le_sSup_iff, upperBounds]

Characterization of Supremum via Upper Bounds: $a \leq \bigsqcup_i s_i \leftrightarrow (\forall b, (\forall i, s_i \leq b) \to a \leq b)$

Informal description

For any indexed family of elements $(s_i)_{i \in \iota}$ in a complete semilattice with supremum, an element $a$ satisfies $a \leq \bigsqcup_i s_i$ if and only if for every upper bound $b$ of the family (i.e., $s_i \leq b$ for all $i$), we have $a \leq b$.

CompleteSemilatticeInf structure

(α : Type*) extends PartialOrder α, InfSet α

Full source

/-- Note that we rarely use `CompleteSemilatticeInf`
(in fact, any such object is always a `CompleteLattice`, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.
-/
class CompleteSemilatticeInf (α : Type*) extends PartialOrder α, InfSet α where
  /-- Any element of a set is more than the set infimum. -/
  sInf_le : ∀ s, ∀ a ∈ s, sInf s ≤ a
  /-- Any lower bound is less than the set infimum. -/
  le_sInf : ∀ s a, (∀ b ∈ s, a ≤ b) → a ≤ sInf s

Complete meet-semilattice

Informal description

A structure representing a complete meet-semilattice, which is a partially ordered set $\alpha$ equipped with an infimum operation $\bigwedge$ that computes the greatest lower bound for any subset of $\alpha$. This structure extends both a partial order and an infimum set operation.

sInf_le theorem

: a ∈ s → sInf s ≤ a

Full source

theorem sInf_le : a ∈ s → sInf s ≤ a :=
  CompleteSemilatticeInf.sInf_le s a

Infimum is Lower Bound: $\bigwedge s \leq a$ for $a \in s$

Informal description

For any element $a$ in a complete meet-semilattice $\alpha$ and any subset $s \subseteq \alpha$, if $a$ belongs to $s$, then the infimum of $s$ is less than or equal to $a$, i.e., $\bigwedge s \leq a$.

le_sInf theorem

: (∀ b ∈ s, a ≤ b) → a ≤ sInf s

Full source

theorem le_sInf : (∀ b ∈ s, a ≤ b) → a ≤ sInf s :=
  CompleteSemilatticeInf.le_sInf s a

Infimum is Greatest Lower Bound: $a \leq \bigwedge s$ for all lower bounds $a$ of $s$

Informal description

For any element $a$ in a complete meet-semilattice $\alpha$ and any subset $s \subseteq \alpha$, if $a$ is a lower bound for $s$ (i.e., $a \leq b$ for all $b \in s$), then $a$ is less than or equal to the infimum of $s$, i.e., $a \leq \bigwedge s$.

isGLB_sInf theorem

(s : Set α) : IsGLB s (sInf s)

Full source

theorem isGLB_sInf (s : Set α) : IsGLB s (sInf s) :=
  ⟨fun _ => sInf_le, fun _ => le_sInf⟩

Infimum is Greatest Lower Bound: $\bigwedge s = \text{GLB}(s)$

Informal description

For any subset $s$ of a complete meet-semilattice $\alpha$, the infimum $\bigwedge s$ is the greatest lower bound of $s$. That is, $\bigwedge s$ is a lower bound for $s$ (i.e., $\bigwedge s \leq a$ for all $a \in s$) and is greater than or equal to any other lower bound of $s$.

isGLB_iff_sInf_eq theorem

: IsGLB s a ↔ sInf s = a

Full source

lemma isGLB_iff_sInf_eq : IsGLBIsGLB s a ↔ sInf s = a :=
  ⟨(isGLB_sInf s).unique, by rintro rfl; exact isGLB_sInf _⟩

Characterization of Greatest Lower Bound via Infimum: $\text{GLB}(s) = a \leftrightarrow \bigwedge s = a$

Informal description

For any subset $s$ of a complete meet-semilattice $\alpha$ and any element $a \in \alpha$, the element $a$ is the greatest lower bound of $s$ if and only if the infimum of $s$ equals $a$, i.e., $\text{IsGLB}(s, a) \leftrightarrow \bigwedge s = a$.

sInf_le_of_le theorem

(hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a

Full source

theorem sInf_le_of_le (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a :=
  le_trans (sInf_le hb) h

Infimum Bound Under Element Comparison: $\bigwedge s \leq a$ when $b \leq a$ for some $b \in s$

Informal description

For any subset $s$ of a complete meet-semilattice $\alpha$, if $b \in s$ and $b \leq a$ for some $a \in \alpha$, then the infimum of $s$ satisfies $\bigwedge s \leq a$.

sInf_le_sInf theorem

(h : s ⊆ t) : sInf t ≤ sInf s

Full source

@[gcongr]
theorem sInf_le_sInf (h : s ⊆ t) : sInf t ≤ sInf s :=
  (isGLB_sInf s).mono (isGLB_sInf t) h

Monotonicity of Infimum under Set Inclusion: $\bigwedge t \leq \bigwedge s$ when $s \subseteq t$

Informal description

For any subsets $s$ and $t$ of a complete meet-semilattice $\alpha$, if $s \subseteq t$, then the infimum of $t$ is less than or equal to the infimum of $s$, i.e., $\bigwedge t \leq \bigwedge s$.

le_sInf_iff theorem

: a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

Full source

@[simp]
theorem le_sInf_iff : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b :=
  le_isGLB_iff (isGLB_sInf s)

Characterization of Lower Bounds via Infimum: $a \leq \bigwedge s$

Informal description

For any subset $s$ of a complete meet-semilattice $\alpha$ and any element $a \in \alpha$, the inequality $a \leq \bigwedge s$ holds if and only if $a$ is a lower bound for $s$, i.e., $a \leq b$ for every $b \in s$.

sInf_le_iff theorem

: sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a

Full source

theorem sInf_le_iff : sInfsInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a :=
  ⟨fun h _ hb => le_trans (le_sInf hb) h, fun hb => hb _ fun _ => sInf_le⟩

Characterization of Infimum Inequality via Lower Bounds: $\bigwedge s \leq a$

Informal description

For any subset $s$ of a complete meet-semilattice $\alpha$ and any element $a \in \alpha$, the infimum $\bigwedge s$ is less than or equal to $a$ if and only if every lower bound $b$ of $s$ satisfies $b \leq a$.

iInf_le_iff theorem

{s : ι → α} : iInf s ≤ a ↔ ∀ b, (∀ i, b ≤ s i) → b ≤ a

Full source

theorem iInf_le_iff {s : ι → α} : iInfiInf s ≤ a ↔ ∀ b, (∀ i, b ≤ s i) → b ≤ a := by
  simp [iInf, sInf_le_iff, lowerBounds]

Characterization of Infimum Inequality: $\bigsqcap_i s_i \leq a$

Informal description

For an indexed family of elements $(s_i)_{i \in \iota}$ in a complete meet-semilattice $\alpha$ and an element $a \in \alpha$, the infimum $\bigsqcap_i s_i$ is less than or equal to $a$ if and only if for every element $b \in \alpha$ that is a lower bound of the family $(s_i)$ (i.e., $b \leq s_i$ for all $i \in \iota$), we have $b \leq a$.

instCompleteSemilatticeSupOrderDualOfCompleteSemilatticeInf instance

{α : Type*} [CompleteSemilatticeInf α] : CompleteSemilatticeSup αᵒᵈ

Full source

instance {α : Type*} [CompleteSemilatticeInf α] : CompleteSemilatticeSup αᵒᵈ where
  le_sSup := @CompleteSemilatticeInf.sInf_le α _
  sSup_le := @CompleteSemilatticeInf.le_sInf α _

Complete Join-Semilattice Structure on Order Dual of Complete Meet-Semilattice

Informal description

For any complete meet-semilattice $\alpha$, the order dual $\alpha^\text{op}$ is a complete join-semilattice.

instCompleteSemilatticeInfOrderDualOfCompleteSemilatticeSup instance

{α : Type*} [CompleteSemilatticeSup α] : CompleteSemilatticeInf αᵒᵈ

Full source

instance {α : Type*} [CompleteSemilatticeSup α] : CompleteSemilatticeInf αᵒᵈ where
  le_sInf := @CompleteSemilatticeSup.sSup_le α _
  sInf_le := @CompleteSemilatticeSup.le_sSup α _

Complete Meet-Semilattice Structure on Order Dual of Complete Join-Semilattice

Informal description

For any type $\alpha$ equipped with a complete join-semilattice structure, the order dual $\alpha^\text{op}$ is a complete meet-semilattice.

CompleteLattice structure

(α : Type*) extends Lattice α, CompleteSemilatticeSup α,
  CompleteSemilatticeInf α, Top α, Bot α

Full source

/-- A complete lattice is a bounded lattice which has suprema and infima for every subset. -/
class CompleteLattice (α : Type*) extends Lattice α, CompleteSemilatticeSup α,
  CompleteSemilatticeInf α, Top α, Bot α where
  /-- Any element is less than the top one. -/
  protected le_top : ∀ x : α, x ≤ ⊤
  /-- Any element is more than the bottom one. -/
  protected bot_le : ∀ x : α, ⊥ ≤ x

Complete Lattice

Informal description

A complete lattice is a bounded lattice where every subset has both a supremum (least upper bound) and an infimum (greatest lower bound). It extends the structure of a lattice with top and bottom elements and the properties that any subset has well-defined suprema and infima.

CompleteLattice.toBoundedOrder instance

[CompleteLattice α] : BoundedOrder α

Full source

instance (priority := 100) CompleteLattice.toBoundedOrder [CompleteLattice α] :
    BoundedOrder α :=
  { ‹CompleteLattice α› with }

Complete Lattices are Bounded Orders

Informal description

Every complete lattice $\alpha$ is a bounded order, meaning it has both a greatest element $\top$ and a least element $\bot$.

completeLatticeOfInf definition

 (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_sInf : ∀ s : Set α, IsGLB s (sInf s)) : CompleteLattice α

Full source

/-- Create a `CompleteLattice` from a `PartialOrder` and `InfSet`
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities.  If other fields are known explicitly, they should be
provided; for example, if `inf` is known explicitly, construct the `CompleteLattice`
instance as
```
instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sSup, bot, top
  __ := completeLatticeOfInf my_T _
```
-/
def completeLatticeOfInf (α : Type*) [H1 : PartialOrder α] [H2 : InfSet α]
    (isGLB_sInf : ∀ s : Set α, IsGLB s (sInf s)) : CompleteLattice α where
  __ := H1; __ := H2
  bot := sInf univ
  bot_le _ := (isGLB_sInf univ).1 trivial
  top := sInf ∅
  le_top a := (isGLB_sInf ∅).2 <| by simp
  sup a b := sInf { x : α | a ≤ x ∧ b ≤ x }
  inf a b := sInf {a, b}
  le_inf a b c hab hac := by
    apply (isGLB_sInf _).2
    simp [*]
  inf_le_right _ _ := (isGLB_sInf _).1 <| mem_insert_of_mem _ <| mem_singleton _
  inf_le_left _ _ := (isGLB_sInf _).1 <| mem_insert _ _
  sup_le a b c hac hbc := (isGLB_sInf _).1 <| by simp [*]
  le_sup_left _ _ := (isGLB_sInf _).2 fun _ => And.left
  le_sup_right _ _ := (isGLB_sInf _).2 fun _ => And.right
  le_sInf s _ ha := (isGLB_sInf s).2 ha
  sInf_le s _ ha := (isGLB_sInf s).1 ha
  sSup s := sInf (upperBounds s)
  le_sSup s _ ha := (isGLB_sInf (upperBounds s)).2 fun _ hb => hb ha
  sSup_le s _ ha := (isGLB_sInf (upperBounds s)).1 ha

Construction of a complete lattice from an infimum structure

Informal description

Given a type $\alpha$ with a partial order and an infimum structure (i.e., a function `sInf` that computes the greatest lower bound of any subset of $\alpha$), if `sInf` indeed returns the greatest lower bound for every subset, then $\alpha$ can be equipped with the structure of a complete lattice. Specifically: - The bottom element $\bot$ is defined as the infimum of the universal set. - The top element $\top$ is defined as the infimum of the empty set. - The supremum $\sup a b$ of two elements is defined as the infimum of the set of upper bounds of $\{a, b\}$. - The infimum $\inf a b$ of two elements is defined as the infimum of the set $\{a, b\}$. - The supremum $\sup s$ of a subset $s$ is defined as the infimum of the set of upper bounds of $s$. All other lattice operations (e.g., $\leq$, $\vee$, $\wedge$) are derived from these definitions, ensuring that $\alpha$ satisfies the axioms of a complete lattice.

completeLatticeOfCompleteSemilatticeInf definition

(α : Type*) [CompleteSemilatticeInf α] : CompleteLattice α

Full source

/-- Any `CompleteSemilatticeInf` is in fact a `CompleteLattice`.

Note that this construction has bad definitional properties:
see the doc-string on `completeLatticeOfInf`.
-/
def completeLatticeOfCompleteSemilatticeInf (α : Type*) [CompleteSemilatticeInf α] :
    CompleteLattice α :=
  completeLatticeOfInf α fun s => isGLB_sInf s

Complete lattice structure from a complete meet-semilattice

Informal description

Given a complete meet-semilattice $\alpha$, the function `completeLatticeOfCompleteSemilatticeInf` constructs a complete lattice structure on $\alpha$ by defining all other lattice operations (including suprema, top, and bottom elements) in terms of the existing infimum operation. Specifically, the supremum of a set $s$ is defined as the infimum of its upper bounds, ensuring that $\alpha$ satisfies all axioms of a complete lattice.

completeLatticeOfSup definition

 (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_sSup : ∀ s : Set α, IsLUB s (sSup s)) : CompleteLattice α

Full source

/-- Create a `CompleteLattice` from a `PartialOrder` and `SupSet`
that returns the least upper bound of a set. Usually this constructor provides
poor definitional equalities.  If other fields are known explicitly, they should be
provided; for example, if `inf` is known explicitly, construct the `CompleteLattice`
instance as
```
instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sInf, bot, top
  __ := completeLatticeOfSup my_T _
```
-/
def completeLatticeOfSup (α : Type*) [H1 : PartialOrder α] [H2 : SupSet α]
    (isLUB_sSup : ∀ s : Set α, IsLUB s (sSup s)) : CompleteLattice α where
  __ := H1; __ := H2
  top := sSup univ
  le_top _ := (isLUB_sSup univ).1 trivial
  bot := sSup ∅
  bot_le x := (isLUB_sSup ∅).2 <| by simp
  sup a b := sSup {a, b}
  sup_le a b c hac hbc := (isLUB_sSup _).2 (by simp [*])
  le_sup_left _ _ := (isLUB_sSup _).1 <| mem_insert _ _
  le_sup_right _ _ := (isLUB_sSup _).1 <| mem_insert_of_mem _ <| mem_singleton _
  inf a b := sSup { x | x ≤ a ∧ x ≤ b }
  le_inf a b c hab hac := (isLUB_sSup _).1 <| by simp [*]
  inf_le_left _ _ := (isLUB_sSup _).2 fun _ => And.left
  inf_le_right _ _ := (isLUB_sSup _).2 fun _ => And.right
  sInf s := sSup (lowerBounds s)
  sSup_le s _ ha := (isLUB_sSup s).2 ha
  le_sSup s _ ha := (isLUB_sSup s).1 ha
  sInf_le s _ ha := (isLUB_sSup (lowerBounds s)).2 fun _ hb => hb ha
  le_sInf s _ ha := (isLUB_sSup (lowerBounds s)).1 ha

Construction of a complete lattice from a supremum operator

Informal description

Given a type $\alpha$ with a partial order and a supremum operator `sSup` that satisfies the least upper bound property (i.e., for any subset $s \subseteq \alpha$, `sSup s` is the least upper bound of $s$), the function `completeLatticeOfSup` constructs a complete lattice structure on $\alpha$. In this complete lattice: - The top element $\top$ is defined as the supremum of the universal set. - The bottom element $\bot$ is defined as the supremum of the empty set. - The join (supremum) of two elements $a$ and $b$ is the supremum of the set $\{a, b\}$. - The meet (infimum) of two elements $a$ and $b$ is the supremum of the set of all lower bounds of $\{a, b\}$. - The infimum of a subset $s$ is defined as the supremum of the set of all lower bounds of $s$. The construction ensures that all the axioms of a complete lattice are satisfied, including the existence of suprema and infima for arbitrary subsets.

completeLatticeOfCompleteSemilatticeSup definition

(α : Type*) [CompleteSemilatticeSup α] : CompleteLattice α

Full source

/-- Any `CompleteSemilatticeSup` is in fact a `CompleteLattice`.

Note that this construction has bad definitional properties:
see the doc-string on `completeLatticeOfSup`.
-/
def completeLatticeOfCompleteSemilatticeSup (α : Type*) [CompleteSemilatticeSup α] :
    CompleteLattice α :=
  completeLatticeOfSup α fun s => isLUB_sSup s

Complete lattice construction from a complete semilattice with suprema

Informal description

Given a type $\alpha$ equipped with a complete semilattice structure with suprema (i.e., a partial order where every subset has a supremum), the function `completeLatticeOfCompleteSemilatticeSup` constructs a complete lattice structure on $\alpha$. In this complete lattice: - The top element $\top$ is the supremum of the entire set $\alpha$. - The bottom element $\bot$ is the supremum of the empty set. - The meet (infimum) of any subset $s \subseteq \alpha$ is defined as the supremum of all lower bounds of $s$. - The join (supremum) of any subset is already provided by the complete semilattice structure. The construction ensures that all complete lattice axioms are satisfied, including the existence of suprema and infima for arbitrary subsets.

CompleteLinearOrder structure

(α : Type*) extends CompleteLattice α, BiheytingAlgebra α, Ord α

Full source

/-- A complete linear order is a linear order whose lattice structure is complete. -/
-- Note that we do not use `extends LinearOrder α`,
-- and instead construct the forgetful instance manually.
class CompleteLinearOrder (α : Type*) extends CompleteLattice α, BiheytingAlgebra α, Ord α where
  /-- A linear order is total. -/
  le_total (a b : α) : a ≤ b ∨ b ≤ a
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableLE : DecidableLE α
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableEq : DecidableEq α := @decidableEqOfDecidableLE _ _ toDecidableLE
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableLT : DecidableLT α := @decidableLTOfDecidableLE _ _ toDecidableLE
  compare a b := compareOfLessAndEq a b
  /-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`. -/
  compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
    compareOfLessAndEq_rfl

Complete Linear Order

Informal description

A complete linear order is a linear order $(α, ≤)$ where every subset $S ⊆ α$ has both a least upper bound (supremum) $\sup S$ and a greatest lower bound (infimum) $\inf S$ in $α$. This structure combines the properties of a complete lattice with those of a linear order, ensuring that the order is total and the lattice operations are well-defined for all subsets.

CompleteLinearOrder.toLinearOrder instance

[i : CompleteLinearOrder α] : LinearOrder α

Full source

instance CompleteLinearOrder.toLinearOrder [i : CompleteLinearOrder α] : LinearOrder α where
  __ := i
  min_def a b := by
    split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]
  max_def a b := by
    split_ifs with h
    · simp [h]
    · simp [(CompleteLinearOrder.le_total a b).resolve_left h]

Complete Linear Orders are Linear Orders

Informal description

Every complete linear order is a linear order.

OrderDual.instCompleteLattice instance

[CompleteLattice α] : CompleteLattice αᵒᵈ

Full source

instance instCompleteLattice [CompleteLattice α] : CompleteLattice αᵒᵈ where
  __ := instBoundedOrder α
  le_sSup := @CompleteLattice.sInf_le α _
  sSup_le := @CompleteLattice.le_sInf α _
  sInf_le := @CompleteLattice.le_sSup α _
  le_sInf := @CompleteLattice.sSup_le α _

Order Dual of a Complete Lattice is Complete

Informal description

For any complete lattice $\alpha$, the order dual $\alpha^{\text{op}}$ is also a complete lattice.

OrderDual.instCompleteLinearOrder instance

[CompleteLinearOrder α] : CompleteLinearOrder αᵒᵈ

Full source

instance instCompleteLinearOrder [CompleteLinearOrder α] : CompleteLinearOrder αᵒᵈ where
  __ := instCompleteLattice
  __ := instBiheytingAlgebra
  __ := instLinearOrder α

Order Dual of a Complete Linear Order is Complete Linear Order

Informal description

For any complete linear order $\alpha$, the order dual $\alpha^{\text{op}}$ is also a complete linear order. This means that in $\alpha^{\text{op}}$, every subset has both a supremum and an infimum, and the order is total.

toDual_sSup theorem

[SupSet α] (s : Set α) : toDual (sSup s) = sInf (ofDual ⁻¹' s)

Full source

@[simp]
theorem toDual_sSup [SupSet α] (s : Set α) : toDual (sSup s) = sInf (ofDualofDual ⁻¹' s) :=
  rfl

Duality between Supremum and Infimum under Order Dual

Informal description

Let $\alpha$ be a type equipped with a supremum operator $\bigvee$. For any subset $s \subseteq \alpha$, the image of the supremum $\bigvee s$ under the order dual map $\alpha \to \alpha^{\text{op}}$ is equal to the infimum of the preimage of $s$ under the inverse order dual map $\alpha^{\text{op}} \to \alpha$. In symbols: \[ \text{toDual}(\bigvee s) = \bigwedge (\text{ofDual}^{-1}(s)) \]

toDual_sInf theorem

[InfSet α] (s : Set α) : toDual (sInf s) = sSup (ofDual ⁻¹' s)

Full source

@[simp]
theorem toDual_sInf [InfSet α] (s : Set α) : toDual (sInf s) = sSup (ofDualofDual ⁻¹' s) :=
  rfl

Duality between Infimum and Supremum under Order Dual

Informal description

Let $\alpha$ be a type equipped with an infimum operator $\bigwedge$. For any subset $s \subseteq \alpha$, the image of the infimum $\bigwedge s$ under the order dual map $\alpha \to \alpha^\text{op}$ is equal to the supremum of the preimage of $s$ under the inverse order dual map $\alpha^\text{op} \to \alpha$. In symbols: \[ \text{toDual}(\bigwedge s) = \bigvee (\text{ofDual}^{-1}(s)) \]

ofDual_sSup theorem

[InfSet α] (s : Set αᵒᵈ) : ofDual (sSup s) = sInf (toDual ⁻¹' s)

Full source

@[simp]
theorem ofDual_sSup [InfSet α] (s : Set αᵒᵈ) : ofDual (sSup s) = sInf (toDualtoDual ⁻¹' s) :=
  rfl

Supremum in Order Dual Equals Infimum in Original Order via Preimage

Informal description

Let $\alpha$ be a type equipped with an infimum operator $\bigwedge$. For any subset $s$ of the order dual $\alpha^\text{op}$, the image of the supremum $\bigvee s$ under the identity map from $\alpha^\text{op}$ to $\alpha$ equals the infimum of the preimage of $s$ under the identity map from $\alpha$ to $\alpha^\text{op}$. In symbols: \[ \text{ofDual}(\bigvee s) = \bigwedge (\text{toDual}^{-1}(s)) \]

ofDual_sInf theorem

[SupSet α] (s : Set αᵒᵈ) : ofDual (sInf s) = sSup (toDual ⁻¹' s)

Full source

@[simp]
theorem ofDual_sInf [SupSet α] (s : Set αᵒᵈ) : ofDual (sInf s) = sSup (toDualtoDual ⁻¹' s) :=
  rfl

Infimum in Order Dual Equals Supremum of Preimage in Original Order

Informal description

Let $\alpha$ be a type equipped with a supremum operator $\bigvee$. For any subset $s$ of the order dual $\alpha^{\text{op}}$, the image under the identity map $\text{ofDual} : \alpha^{\text{op}} \to \alpha$ of the infimum $\bigwedge s$ in $\alpha^{\text{op}}$ equals the supremum $\bigvee (\text{toDual}^{-1}(s))$ in $\alpha$, where $\text{toDual} : \alpha \to \alpha^{\text{op}}$ is the identity map to the order dual.

toDual_iSup theorem

[SupSet α] (f : ι → α) : toDual (⨆ i, f i) = ⨅ i, toDual (f i)

Full source

@[simp]
theorem toDual_iSup [SupSet α] (f : ι → α) : toDual (⨆ i, f i) = ⨅ i, toDual (f i) :=
  rfl

Order Dual Preserves Supremum as Infimum

Informal description

For any type $\alpha$ equipped with a supremum operator and any indexed family $f : \iota \to \alpha$, the image under the order dual map of the supremum $\bigsqcup_i f_i$ is equal to the infimum $\bigsqcap_i$ of the images of $f_i$ under the order dual map. In symbols: \[ \text{toDual}\left(\bigsqcup_i f_i\right) = \bigsqcap_i \text{toDual}(f_i) \]

toDual_iInf theorem

[InfSet α] (f : ι → α) : toDual (⨅ i, f i) = ⨆ i, toDual (f i)

Full source

@[simp]
theorem toDual_iInf [InfSet α] (f : ι → α) : toDual (⨅ i, f i) = ⨆ i, toDual (f i) :=
  rfl

Order Dual Preserves Infimum as Supremum

Informal description

For any type $\alpha$ equipped with an infimum operator and any indexed family $f : \iota \to \alpha$, the image under the order dual map of the infimum $\bigsqcap_i f_i$ is equal to the supremum $\bigsqcup_i$ of the images of $f_i$ under the order dual map. In symbols: \[ \text{toDual}\left(\bigsqcap_i f_i\right) = \bigsqcup_i \text{toDual}(f_i) \]

ofDual_iSup theorem

[InfSet α] (f : ι → αᵒᵈ) : ofDual (⨆ i, f i) = ⨅ i, ofDual (f i)

Full source

@[simp]
theorem ofDual_iSup [InfSet α] (f : ι → αᵒᵈ) : ofDual (⨆ i, f i) = ⨅ i, ofDual (f i) :=
  rfl

Order Dual Supremum-Infimum Duality: $\text{ofDual}(\bigsqcup_i f_i) = \bigsqcap_i \text{ofDual}(f_i)$

Informal description

For any type $\alpha$ equipped with an infimum operator and any indexed family $f : \iota \to \alpha^\text{op}$ (where $\alpha^\text{op}$ is the order dual of $\alpha$), the image under the order dual map of the supremum $\bigsqcup_i f_i$ in $\alpha^\text{op}$ is equal to the infimum $\bigsqcap_i$ of the images of $f_i$ under the order dual map in $\alpha$. In symbols: \[ \text{ofDual}\left(\bigsqcup_i f_i\right) = \bigsqcap_i \text{ofDual}(f_i) \]

ofDual_iInf theorem

[SupSet α] (f : ι → αᵒᵈ) : ofDual (⨅ i, f i) = ⨆ i, ofDual (f i)

Full source

@[simp]
theorem ofDual_iInf [SupSet α] (f : ι → αᵒᵈ) : ofDual (⨅ i, f i) = ⨆ i, ofDual (f i) :=
  rfl

Order Dual Infimum-Supremum Relation: $\text{ofDual}(\bigsqcap_i f(i)) = \bigsqcup_i \text{ofDual}(f(i))$

Informal description

Let $\alpha$ be a type equipped with a supremum operator $\bigvee$, and let $f : \iota \to \alpha^\text{op}$ be an indexed family in the order dual of $\alpha$. Then the image under the order-reversing equivalence $\alpha^\text{op} \simeq \alpha$ of the infimum $\bigsqcap_i f(i)$ in $\alpha^\text{op}$ equals the supremum $\bigsqcup_i \text{ofDual}(f(i))$ in $\alpha$.

lt_sSup_iff theorem

: b < sSup s ↔ ∃ a ∈ s, b < a

Full source

theorem lt_sSup_iff : b < sSup s ↔ ∃ a ∈ s, b < a :=
  lt_isLUB_iff <| isLUB_sSup s

Characterization of elements strictly below the supremum: $b < \sup s \leftrightarrow \exists a \in s, b < a$

Informal description

For any subset $s$ of a complete linear order $\alpha$ and any element $b \in \alpha$, we have $b < \sup s$ if and only if there exists an element $a \in s$ such that $b < a$.

sInf_lt_iff theorem

: sInf s < b ↔ ∃ a ∈ s, a < b

Full source

theorem sInf_lt_iff : sInfsInf s < b ↔ ∃ a ∈ s, a < b :=
  isGLB_lt_iff <| isGLB_sInf s

Characterization of elements strictly above the infimum: $\inf s < b \leftrightarrow \exists a \in s, a < b$

Informal description

For any subset $s$ of a complete linear order $\alpha$ and any element $b \in \alpha$, the infimum of $s$ is strictly less than $b$ if and only if there exists an element $a \in s$ such that $a < b$. In symbols: \[ \inf s < b \leftrightarrow \exists a \in s, a < b \]

sSup_eq_top theorem

: sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a

Full source

theorem sSup_eq_top : sSupsSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a :=
  ⟨fun h _ hb => lt_sSup_iff.1 <| hb.trans_eq h.symm, fun h =>
    top_unique <|
      le_of_not_gt fun h' =>
        let ⟨_, ha, h⟩ := h _ h'
        (h.trans_le <| le_sSup ha).false⟩

Supremum Equals Top Element Characterization

Informal description

For a subset $s$ of a complete linear order $\alpha$ with a greatest element $\top$, the supremum of $s$ equals $\top$ if and only if for every element $b < \top$, there exists an element $a \in s$ such that $b < a$. In symbols: \[ \sup s = \top \leftrightarrow \forall b < \top, \exists a \in s, b < a. \]

sInf_eq_bot theorem

: sInf s = ⊥ ↔ ∀ b > ⊥, ∃ a ∈ s, a < b

Full source

theorem sInf_eq_bot : sInfsInf s = ⊥ ↔ ∀ b > ⊥, ∃ a ∈ s, a < b :=
  @sSup_eq_top αᵒᵈ _ _

Infimum Equals Bottom Element Characterization

Informal description

For a subset $s$ of a complete linear order $\alpha$ with a least element $\bot$, the infimum of $s$ equals $\bot$ if and only if for every element $b > \bot$, there exists an element $a \in s$ such that $a < b$. In symbols: \[ \inf s = \bot \leftrightarrow \forall b > \bot, \exists a \in s, a < b. \]

lt_iSup_iff theorem

{f : ι → α} : a < iSup f ↔ ∃ i, a < f i

Full source

theorem lt_iSup_iff {f : ι → α} : a < iSup f ↔ ∃ i, a < f i :=
  lt_sSup_iff.trans exists_range_iff

Characterization of elements strictly below the indexed supremum: $a < \bigsqcup_i f_i \leftrightarrow \exists i, a < f_i$

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ in a complete linear order $\alpha$ and any element $a \in \alpha$, we have $a < \bigsqcup_{i \in \iota} f_i$ if and only if there exists an index $i \in \iota$ such that $a < f_i$.

iInf_lt_iff theorem

{f : ι → α} : iInf f < a ↔ ∃ i, f i < a

Full source

theorem iInf_lt_iff {f : ι → α} : iInfiInf f < a ↔ ∃ i, f i < a :=
  sInf_lt_iff.trans exists_range_iff

Characterization of elements strictly above the indexed infimum: $\bigsqcap_i f_i < a \leftrightarrow \exists i, f_i < a$

Informal description

For any indexed family of elements $(f_i)_{i \in \iota}$ in a complete linear order $\alpha$ and any element $a \in \alpha$, the infimum of the family is strictly less than $a$ if and only if there exists an index $i \in \iota$ such that $f_i < a$. In symbols: \[ \bigsqcap_{i \in \iota} f_i < a \leftrightarrow \exists i \in \iota, f_i < a \]

Mathlib.Order.CompleteLattice.Defs

Main definitions

Naming conventions

Notation