Mathlib.Order.ConditionallyCompleteLattice.Basic

WithTop.instSupSet instance

[SupSet α] : SupSet (WithTop α)

Full source

noncomputable instance WithTop.instSupSet [SupSet α] :
    SupSet (WithTop α) :=
  ⟨fun S =>
    if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then
      ↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩

Supremum Operation on $\text{WithTop}\ \alpha$

Informal description

For any type $\alpha$ equipped with a supremum operation $\bigsqcup$ (as in a complete lattice or conditionally complete lattice), the type $\text{WithTop}\ \alpha$ (which adds a top element $\top$ to $\alpha$) inherits a supremum operation. This operation extends the original supremum operation on $\alpha$ to handle subsets of $\text{WithTop}\ \alpha$ that may include $\top$.

WithTop.instInfSet instance

[InfSet α] : InfSet (WithTop α)

Full source

noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
  ⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩

Infimum Structure on `WithTop α`

Informal description

For any type $\alpha$ equipped with an `InfSet` structure (a way to compute infima of subsets), the type `WithTop α` (which adds a top element $\top$ to $\alpha$) also inherits an `InfSet` structure. This means that we can compute infima of subsets of $\alpha$ extended with $\top$.

WithBot.instSupSet instance

[SupSet α] : SupSet (WithBot α)

Full source

noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
  ⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩

Supremum Operation on $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ equipped with a supremum operation (as in a complete lattice or conditionally complete lattice), the type $\text{WithBot}\ \alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a supremum operation. This operation extends the original supremum operation on $\alpha$ to handle subsets of $\text{WithBot}\ \alpha$ that may include $\bot$.

WithBot.instInfSet instance

[InfSet α] : InfSet (WithBot α)

Full source

noncomputable instance WithBot.instInfSet [InfSet α] :
    InfSet (WithBot α) :=
  ⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩

Infimum Operation on $\text{WithBot}\ \alpha$

Informal description

For any type $\alpha$ equipped with an infimum operation $\bigsqcap$ (as in a complete lattice or conditionally complete lattice), the type $\text{WithBot}\ \alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits an infimum operation. This operation extends the original infimum operation on $\alpha$ to handle subsets of $\text{WithBot}\ \alpha$ that may include $\bot$.

WithTop.sSup_eq theorem

 [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) (hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α)

Full source

theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤⊤ ∉ s)
    (hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
  (if_neg hs).trans <| if_pos hs'

Supremum in $\text{WithTop}\ \alpha$ for Sets Excluding Top and Bounded Below

Informal description

Let $\alpha$ be a type equipped with a supremum operation $\bigsqcup$, and let $s$ be a subset of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$). If $\top \notin s$ and the preimage of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is bounded above in $\alpha$, then the supremum of $s$ in $\text{WithTop}\ \alpha$ is equal to the image under the canonical embedding of the supremum of the preimage of $s$ in $\alpha$. In other words, $\bigsqcup s = \bigsqcup ((\uparrow)^{-1} s)$.

WithTop.sInf_eq theorem

[InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α)

Full source

theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
    sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
  if_neg <| by simp [hs, h's]

Infimum in `WithTop α` for Non-Top Subsets

Informal description

Let $\alpha$ be a type equipped with an `InfSet` structure, and let $s$ be a subset of `WithTop α` (the type $\alpha$ extended with a top element $\top$). If $s$ is not entirely contained in $\{\top\}$ and is bounded below, then the infimum of $s$ in `WithTop α` is equal to the image under the canonical embedding of the infimum of the preimage of $s$ in $\alpha$, i.e., $\inf s = \uparrow (\inf ((\uparrow)^{-1} s))$.

WithBot.sSup_eq theorem

[SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α)

Full source

theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
    sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
  WithTop.sInf_eq (α := αᵒᵈ) hs h's

Supremum in $\text{WithBot}\ \alpha$ for Non-Bottom Subsets

Informal description

Let $\alpha$ be a type equipped with a supremum operation (SupSet). For any subset $s$ of $\text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$) that is not entirely contained in $\{\bot\}$ and is bounded above, the supremum of $s$ in $\text{WithBot}\ \alpha$ is equal to the image under the canonical embedding of the supremum of the preimage of $s$ in $\alpha$, i.e., $\sup s = \uparrow (\sup ((\uparrow)^{-1} s))$.

WithTop.sInf_empty theorem

[InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤

Full source

@[simp]
theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
  if_pos <| by simp

Infimum of Empty Set in $\WithTop \alpha$ is Top Element

Informal description

For any type $\alpha$ equipped with an infimum structure, the infimum of the empty set in $\WithTop \alpha$ (the type $\alpha$ extended with a top element $\top$) is equal to $\top$.

WithTop.coe_sInf' theorem

 [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α)

Full source

theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
    ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
  classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _

Infimum Preservation under Canonical Embedding to `WithTop α`

Informal description

For a nonempty set $s$ of elements in a type $\alpha$ with an `InfSet` structure, if $s$ is bounded below, then the image of the infimum of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is equal to the infimum of the image of $s$ in $\text{WithTop}\ \alpha$. In other words, $\uparrow(\text{sInf}\ s) = \text{sInf}\ (\uparrow '' s)$.

WithTop.coe_sSup' theorem

[SupSet α] {s : Set α} (hs : BddAbove s) : ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α)

Full source

theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
    ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
  classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩

Preservation of Supremum under Canonical Embedding to $\text{WithTop}\ \alpha$ for Bounded Above Sets

Informal description

Let $\alpha$ be a type equipped with a supremum operation $\bigsqcup$, and let $s$ be a nonempty subset of $\alpha$ that is bounded above. Then the image of the supremum of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is equal to the supremum of the image of $s$ under this embedding in $\text{WithTop}\ \alpha$. In other words, if $s \subseteq \alpha$ is nonempty and bounded above, then $\uparrow(\bigsqcup s) = \bigsqcup \{\uparrow a \mid a \in s\}$ in $\text{WithTop}\ \alpha$.

WithBot.sSup_empty theorem

[SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥

Full source

@[simp]
theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
  WithTop.sInf_empty (α := αᵒᵈ)

Supremum of Empty Set in $\text{WithBot}\ \alpha$ is Bottom Element

Informal description

For any type $\alpha$ equipped with a supremum operation, the supremum of the empty set in $\text{WithBot}\ \alpha$ (the type $\alpha$ extended with a bottom element $\bot$) is equal to $\bot$.

WithBot.coe_sSup' theorem

 [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) : ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α)

Full source

@[norm_cast]
theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
    ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
  WithTop.coe_sInf' (α := αᵒᵈ) hs h's

Preservation of Supremum under Canonical Embedding to $\text{WithBot}\ \alpha$ for Nonempty Bounded Above Sets

Informal description

Let $\alpha$ be a type equipped with a supremum operation $\bigsqcup$, and let $s$ be a nonempty subset of $\alpha$ that is bounded above. Then the image of the supremum of $s$ under the canonical embedding $\alpha \to \text{WithBot}\ \alpha$ is equal to the supremum of the image of $s$ under this embedding in $\text{WithBot}\ \alpha$. In other words, if $s \subseteq \alpha$ is nonempty and bounded above, then $\uparrow(\bigsqcup s) = \bigsqcup \{\uparrow a \mid a \in s\}$ in $\text{WithBot}\ \alpha$.

WithBot.coe_sInf' theorem

[InfSet α] {s : Set α} (hs : BddBelow s) : ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α)

Full source

@[norm_cast]
theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
    ↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
  WithTop.coe_sSup' (α := αᵒᵈ) hs

Preservation of Infimum under Canonical Embedding to $\text{WithBot}\ \alpha$ for Bounded Below Sets

Informal description

Let $\alpha$ be a type equipped with an infimum operation $\bigsqcap$, and let $s$ be a subset of $\alpha$ that is bounded below. Then the image of the infimum of $s$ under the canonical embedding $\alpha \to \text{WithBot}\ \alpha$ is equal to the infimum of the image of $s$ under this embedding in $\text{WithBot}\ \alpha$. In other words, if $s \subseteq \alpha$ is bounded below, then $\uparrow(\bigsqcap s) = \bigsqcap \{\uparrow a \mid a \in s\}$ in $\text{WithBot}\ \alpha$.

ConditionallyCompleteLinearOrder.toLinearOrder instance

[ConditionallyCompleteLinearOrder α] : LinearOrder α

Full source

instance ConditionallyCompleteLinearOrder.toLinearOrder [ConditionallyCompleteLinearOrder α] :
    LinearOrder α :=
  { ‹ConditionallyCompleteLinearOrder α› with
    min_def := fun a b ↦ by
      by_cases hab : a = b
      · simp [hab]
      · rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
        · simp [h₁]
        · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂]
    max_def := fun a b ↦ by
      by_cases hab : a = b
      · simp [hab]
      · rcases ConditionallyCompleteLinearOrder.le_total a b with (h₁ | h₂)
        · simp [h₁]
        · simp [show ¬(a ≤ b) from fun h => hab (le_antisymm h h₂), h₂] }

Conditionally Complete Linear Orders are Linear Orders

Informal description

Every conditionally complete linear order is a linear order.

CompleteLattice.toConditionallyCompleteLattice instance

[CompleteLattice α] : ConditionallyCompleteLattice α

Full source

/-- A complete lattice is a conditionally complete lattice, as there are no restrictions
on the properties of sInf and sSup in a complete lattice. -/
instance (priority := 100) CompleteLattice.toConditionallyCompleteLattice [CompleteLattice α] :
    ConditionallyCompleteLattice α :=
  { ‹CompleteLattice α› with
    le_csSup := by intros; apply le_sSup; assumption
    csSup_le := by intros; apply sSup_le; assumption
    csInf_le := by intros; apply sInf_le; assumption
    le_csInf := by intros; apply le_sInf; assumption }

Complete Lattices as Conditionally Complete Lattices

Informal description

Every complete lattice is a conditionally complete lattice.

CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instance

{α : Type*} [h : CompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot α

Full source

instance (priority := 100) CompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α : Type*}
    [h : CompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot α :=
  { CompleteLattice.toConditionallyCompleteLattice, h with
    csSup_empty := sSup_empty
    csSup_of_not_bddAbove := fun s H ↦ (H (OrderTop.bddAbove s)).elim
    csInf_of_not_bddBelow := fun s H ↦ (H (OrderBot.bddBelow s)).elim }

Complete Linear Orders as Conditionally Complete Linear Orders with Bottom

Informal description

Every complete linear order is a conditionally complete linear order with a bottom element.

OrderDual.instConditionallyCompleteLattice instance

(α : Type*) [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice αᵒᵈ

Full source

instance instConditionallyCompleteLattice (α : Type*) [ConditionallyCompleteLattice α] :
    ConditionallyCompleteLattice αᵒᵈ :=
  { OrderDual.instInf α, OrderDual.instSup α, OrderDual.instLattice α with
    le_csSup := ConditionallyCompleteLattice.csInf_le (α := α)
    csSup_le := ConditionallyCompleteLattice.le_csInf (α := α)
    le_csInf := ConditionallyCompleteLattice.csSup_le (α := α)
    csInf_le := ConditionallyCompleteLattice.le_csSup (α := α) }

Conditionally Complete Lattice Structure on Order Duals

Informal description

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

OrderDual.instConditionallyCompleteLinearOrder instance

(α : Type*) [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrder αᵒᵈ

Full source

instance (α : Type*) [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrder αᵒᵈ :=
  { OrderDual.instConditionallyCompleteLattice α, OrderDual.instLinearOrder α with
    csSup_of_not_bddAbove := ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow (α := α)
    csInf_of_not_bddBelow := ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove (α := α) }

Conditionally Complete Linear Order Structure on Order Duals

Informal description

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

le_csSup theorem

(h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s

Full source

theorem le_csSup (h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s :=
  ConditionallyCompleteLattice.le_csSup s a h₁ h₂

Element of Bounded Above Set is Below Supremum

Informal description

Let $s$ be a nonempty subset of a conditionally complete lattice $\alpha$ that is bounded above. For any element $a \in s$, we have $a \leq \sup s$.

csSup_le theorem

(h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) : sSup s ≤ a

Full source

theorem csSup_le (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) : sSup s ≤ a :=
  ConditionallyCompleteLattice.csSup_le s a h₁ h₂

Supremum of Bounded Above Set is Below Any Upper Bound

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$. If $a$ is an upper bound for $s$ (i.e., $b \leq a$ for all $b \in s$), then $\sup s \leq a$.

csInf_le theorem

(h₁ : BddBelow s) (h₂ : a ∈ s) : sInf s ≤ a

Full source

theorem csInf_le (h₁ : BddBelow s) (h₂ : a ∈ s) : sInf s ≤ a :=
  ConditionallyCompleteLattice.csInf_le s a h₁ h₂

Infimum of Bounded Below Set is Below Any Element

Informal description

Let $s$ be a nonempty subset of a conditionally complete lattice $\alpha$ that is bounded below. For any element $a \in s$, we have $\inf s \leq a$.

le_csInf theorem

(h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) : a ≤ sInf s

Full source

theorem le_csInf (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) : a ≤ sInf s :=
  ConditionallyCompleteLattice.le_csInf s a h₁ h₂

Lower Bound Property for Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$. If $a$ is a lower bound for $s$ (i.e., $a \leq b$ for all $b \in s$), then $a \leq \inf s$.

le_csSup_of_le theorem

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

Full source

theorem le_csSup_of_le (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
  le_trans h (le_csSup hs hb)

Comparison of Element with Supremum via Intermediate Element in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$ that is bounded above. If $b \in s$ and $a \leq b$ for some $a \in \alpha$, then $a \leq \sup s$.

csInf_le_of_le theorem

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

Full source

theorem csInf_le_of_le (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) : sInf s ≤ a :=
  le_trans (csInf_le hs hb) h

Infimum Comparison under Element Inequality in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. If $b \in s$ and $b \leq a$ for some $a \in \alpha$, then the infimum of $s$ satisfies $\inf s \leq a$.

csSup_le_csSup theorem

(ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) : sSup s ≤ sSup t

Full source

theorem csSup_le_csSup (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) : sSup s ≤ sSup t :=
  csSup_le hs fun _ ha => le_csSup ht (h ha)

Monotonicity of Supremum under Inclusion in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ and $t$ be subsets of $\alpha$ such that $s$ is nonempty, $t$ is bounded above, and $s \subseteq t$. Then the supremum of $s$ is less than or equal to the supremum of $t$, i.e., $\sup s \leq \sup t$.

csInf_le_csInf theorem

(ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s

Full source

theorem csInf_le_csInf (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s :=
  le_csInf hs fun _ ha => csInf_le ht (h ha)

Monotonicity of Infimum under Inclusion in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ and $t$ be nonempty subsets of $\alpha$ such that $s \subseteq t$ and $t$ is bounded below. Then the infimum of $t$ is less than or equal to the infimum of $s$, i.e., $\inf t \leq \inf s$.

le_csSup_iff theorem

(h : BddAbove s) (hs : s.Nonempty) : a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b

Full source

theorem le_csSup_iff (h : BddAbove s) (hs : s.Nonempty) :
    a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b :=
  ⟨fun h _ hb => le_trans h (csSup_le hs hb), fun hb => hb _ fun _ => le_csSup h⟩

Characterization of Supremum via Upper Bounds in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded above. For any element $a \in \alpha$, we have $a \leq \sup s$ if and only if $a$ is a lower bound for the set of all upper bounds of $s$ (i.e., $a \leq b$ for every upper bound $b$ of $s$).

csInf_le_iff theorem

(h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a

Full source

theorem csInf_le_iff (h : BddBelow s) (hs : s.Nonempty) : sInfsInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a :=
  ⟨fun h _ hb => le_trans (le_csInf hs hb) h, fun hb => hb _ fun _ => csInf_le h⟩

Characterization of Infimum via Lower Bounds in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. For any element $a \in \alpha$, the infimum of $s$ satisfies $\inf s \leq a$ if and only if $a$ is an upper bound for all lower bounds of $s$ (i.e., for every $b$ that is a lower bound of $s$, we have $b \leq a$).

isLUB_csSup theorem

(ne : s.Nonempty) (H : BddAbove s) : IsLUB s (sSup s)

Full source

theorem isLUB_csSup (ne : s.Nonempty) (H : BddAbove s) : IsLUB s (sSup s) :=
  ⟨fun _ => le_csSup H, fun _ => csSup_le ne⟩

Supremum is Least Upper Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded above. Then the supremum $\sup s$ is the least upper bound of $s$, meaning: 1. $\sup s$ is an upper bound of $s$ (i.e., $b \leq \sup s$ for all $b \in s$), and 2. $\sup s$ is less than or equal to any other upper bound of $s$.

isGLB_csInf theorem

(ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s)

Full source

theorem isGLB_csInf (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s) :=
  ⟨fun _ => csInf_le H, fun _ => le_csInf ne⟩

Infimum is Greatest Lower Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. Then the infimum $\inf s$ is the greatest lower bound of $s$, meaning: 1. $\inf s$ is a lower bound of $s$ (i.e., $\inf s \leq b$ for all $b \in s$), and 2. $\inf s$ is greater than or equal to any other lower bound of $s$.

IsLUB.csSup_eq theorem

(H : IsLUB s a) (ne : s.Nonempty) : sSup s = a

Full source

theorem IsLUB.csSup_eq (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a :=
  (isLUB_csSup ne ⟨a, H.1⟩).unique H

Supremum Equals Least Upper Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ be a nonempty subset of $\alpha$. If $a$ is the least upper bound of $s$, then the supremum of $s$ is equal to $a$, i.e., $\sup s = a$.

IsGreatest.csSup_eq theorem

(H : IsGreatest s a) : sSup s = a

Full source

/-- A greatest element of a set is the supremum of this set. -/
theorem IsGreatest.csSup_eq (H : IsGreatest s a) : sSup s = a :=
  H.isLUB.csSup_eq H.nonempty

Supremum of a Set Equals its Greatest Element

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$. If $a$ is the greatest element of $s$ (i.e., $a \in s$ and $a \geq b$ for all $b \in s$), then the supremum of $s$ equals $a$, i.e., $\sup s = a$.

IsGreatest.csSup_mem theorem

(H : IsGreatest s a) : sSup s ∈ s

Full source

theorem IsGreatest.csSup_mem (H : IsGreatest s a) : sSupsSup s ∈ s :=
  H.csSup_eq.symm ▸ H.1

Supremum of a Set with Greatest Element Belongs to the Set

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$. If $a$ is the greatest element of $s$ (i.e., $a \in s$ and $a \geq b$ for all $b \in s$), then the supremum of $s$ is an element of $s$, i.e., $\sup s \in s$.

IsGLB.csInf_eq theorem

(H : IsGLB s a) (ne : s.Nonempty) : sInf s = a

Full source

theorem IsGLB.csInf_eq (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a :=
  (isGLB_csInf ne ⟨a, H.1⟩).unique H

Infimum Equals Greatest Lower Bound in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $s$ a nonempty subset of $\alpha$, and $a \in \alpha$. If $a$ is the greatest lower bound of $s$ (i.e., $a$ is a lower bound of $s$ and any other lower bound $b$ satisfies $b \leq a$), then the infimum of $s$ equals $a$, i.e., $\inf s = a$.

IsLeast.csInf_eq theorem

(H : IsLeast s a) : sInf s = a

Full source

/-- A least element of a set is the infimum of this set. -/
theorem IsLeast.csInf_eq (H : IsLeast s a) : sInf s = a :=
  H.isGLB.csInf_eq H.nonempty

Infimum of a Set Equals its Least Element

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$. If $a$ is the least element of $s$ (i.e., $a \in s$ and $a \leq b$ for all $b \in s$), then the infimum of $s$ equals $a$, i.e., $\inf s = a$.

IsLeast.csInf_mem theorem

(H : IsLeast s a) : sInf s ∈ s

Full source

theorem IsLeast.csInf_mem (H : IsLeast s a) : sInfsInf s ∈ s :=
  H.csInf_eq.symm ▸ H.1

Infimum of a Set with Least Element Belongs to the Set

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$. If $a$ is the least element of $s$ (i.e., $a \in s$ and $a \leq b$ for all $b \in s$), then the infimum of $s$ is an element of $s$.

subset_Icc_csInf_csSup theorem

(hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s)

Full source

theorem subset_Icc_csInf_csSup (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s) :=
  fun _ hx => ⟨csInf_le hb hx, le_csSup ha hx⟩

Subset Contained in Interval of Infimum and Supremum

Informal description

For any nonempty subset $s$ of a conditionally complete lattice that is both bounded below and bounded above, $s$ is contained in the closed interval between its infimum and supremum, i.e., $s \subseteq [\inf s, \sup s]$.

csSup_le_iff theorem

(hb : BddAbove s) (hs : s.Nonempty) : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

Full source

theorem csSup_le_iff (hb : BddAbove s) (hs : s.Nonempty) : sSupsSup s ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  isLUB_le_iff (isLUB_csSup hs hb)

Supremum Bound Characterization in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $s$ a nonempty subset of $\alpha$ that is bounded above, and $a$ an element of $\alpha$. Then the supremum of $s$ is less than or equal to $a$ if and only if every element of $s$ is less than or equal to $a$. In other words: \[ \sup s \leq a \leftrightarrow (\forall b \in s, b \leq a). \]

le_csInf_iff theorem

(hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

Full source

theorem le_csInf_iff (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b :=
  le_isGLB_iff (isGLB_csInf hs hb)

Characterization of Lower Bounds via Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. For any element $a \in \alpha$, we have $a \leq \inf s$ if and only if $a$ is a lower bound for $s$ (i.e., $a \leq b$ for all $b \in s$).

csSup_lowerBounds_eq_csInf theorem

{s : Set α} (h : BddBelow s) (hs : s.Nonempty) : sSup (lowerBounds s) = sInf s

Full source

theorem csSup_lowerBounds_eq_csInf {s : Set α} (h : BddBelow s) (hs : s.Nonempty) :
    sSup (lowerBounds s) = sInf s :=
  (isLUB_csSup h <| hs.mono fun _ hx _ hy => hy hx).unique (isGLB_csInf hs h).isLUB

Supremum of Lower Bounds Equals Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded below. Then the supremum of the set of lower bounds of $s$ equals the infimum of $s$, i.e., $$\sup \{x \in \alpha \mid \forall y \in s, x \leq y\} = \inf s.$$

csInf_upperBounds_eq_csSup theorem

{s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s

Full source

theorem csInf_upperBounds_eq_csSup {s : Set α} (h : BddAbove s) (hs : s.Nonempty) :
    sInf (upperBounds s) = sSup s :=
  (isGLB_csInf h <| hs.mono fun _ hx _ hy => hy hx).unique (isLUB_csSup hs h).isGLB

Infimum of Upper Bounds Equals Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded above. Then the infimum of the set of upper bounds of $s$ equals the supremum of $s$, i.e., \[ \inf (\text{upperBounds } s) = \sup s. \]

csSup_lowerBounds_range theorem

[Nonempty β] {f : β → α} (hf : BddBelow (range f)) : sSup (lowerBounds (range f)) = ⨅ i, f i

Full source

theorem csSup_lowerBounds_range [Nonempty β] {f : β → α} (hf : BddBelow (range f)) :
    sSup (lowerBounds (range f)) = ⨅ i, f i :=
  csSup_lowerBounds_eq_csInf hf <| range_nonempty _

Supremum of Lower Bounds Equals Infimum for Bounded Below Functions

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a nonempty type, and $f : \beta \to \alpha$ a function whose range is bounded below. Then the supremum of the set of lower bounds of the range of $f$ equals the infimum of $f$ over all inputs, i.e., $$\sup \{x \in \alpha \mid \forall y \in \text{range } f, x \leq y\} = \inf_{i \in \beta} f(i).$$

csInf_upperBounds_range theorem

[Nonempty β] {f : β → α} (hf : BddAbove (range f)) : sInf (upperBounds (range f)) = ⨆ i, f i

Full source

theorem csInf_upperBounds_range [Nonempty β] {f : β → α} (hf : BddAbove (range f)) :
    sInf (upperBounds (range f)) = ⨆ i, f i :=
  csInf_upperBounds_eq_csSup hf <| range_nonempty _

Infimum of Upper Bounds of Range Equals Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, $\beta$ a nonempty type, and $f : \beta \to \alpha$ a function whose range is bounded above. Then the infimum of the set of upper bounds of the range of $f$ equals the supremum of $f$, i.e., \[ \inf (\text{upperBounds } (\text{range } f)) = \sup_{i} f(i). \]

not_mem_of_lt_csInf theorem

{x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) : x ∉ s

Full source

theorem not_mem_of_lt_csInf {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) : x ∉ s :=
  fun hx => lt_irrefl _ (h.trans_le (csInf_le hs hx))

Elements Below Infimum Are Not in the Set

Informal description

Let $s$ be a nonempty subset of a conditionally complete lattice $\alpha$ that is bounded below. If an element $x \in \alpha$ satisfies $x < \inf s$, then $x$ does not belong to $s$.

not_mem_of_csSup_lt theorem

{x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) : x ∉ s

Full source

theorem not_mem_of_csSup_lt {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) : x ∉ s :=
  not_mem_of_lt_csInf (α := αᵒᵈ) h hs

Elements Above Supremum Are Not in the Set

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is bounded above. If an element $x \in \alpha$ satisfies $\sup s < x$, then $x$ does not belong to $s$.

csSup_eq_of_forall_le_of_forall_lt_exists_gt theorem

(hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b) (H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b

Full source

/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that `b`
is larger than all elements of `s`, and that this is not the case of any `w<b`.
See `sSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/
theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b)
    (H' : ∀ w, w < b → ∃ a ∈ s, w < a) : sSup s = b :=
  (eq_of_le_of_not_lt (csSup_le hs H)) fun hb =>
    let ⟨_, ha, ha'⟩ := H' _ hb
    lt_irrefl _ <| ha'.trans_le <| le_csSup ⟨b, H⟩ ha

Characterization of Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$. Suppose that: 1. $b$ is an upper bound for $s$ (i.e., $a \leq b$ for all $a \in s$), and 2. For any $w < b$, there exists $a \in s$ such that $w < a$. Then the supremum of $s$ equals $b$, i.e., $\sup s = b$.

csInf_eq_of_forall_ge_of_forall_gt_exists_lt theorem

: s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b

Full source

/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w>b`.
See `sInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in complete lattices. -/
theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt :
    s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ w, b < w → ∃ a ∈ s, a < w) → sInf s = b :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt (α := αᵒᵈ)

Characterization of Infimum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$. Suppose that: 1. $b$ is a lower bound for $s$ (i.e., $b \leq a$ for all $a \in s$), and 2. For any $w > b$, there exists $a \in s$ such that $a < w$. Then the infimum of $s$ equals $b$, i.e., $\inf s = b$.

lt_csSup_of_lt theorem

(hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s

Full source

/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness above for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem lt_csSup_of_lt (hs : BddAbove s) (ha : a ∈ s) (h : b < a) : b < sSup s :=
  lt_of_lt_of_le h (le_csSup hs ha)

Strict Inequality Preserved by Supremum in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ be a subset of $\alpha$ that is bounded above. If there exists an element $a \in s$ such that $b < a$ for some $b \in \alpha$, then $b$ is strictly less than the supremum of $s$, i.e., $b < \sup s$.

csInf_lt_of_lt theorem

: BddBelow s → a ∈ s → a < b → sInf s < b

Full source

/-- `sInf s < b` when there is an element `a` in `s` with `a < b`, when `s` is bounded below.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness below for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case. -/
theorem csInf_lt_of_lt : BddBelow s → a ∈ s → a < b → sInf s < b :=
  lt_csSup_of_lt (α := αᵒᵈ)

Infimum Strictly Less Than Element in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ be a subset of $\alpha$ that is bounded below. If there exists an element $a \in s$ such that $a < b$ for some $b \in \alpha$, then the infimum of $s$ is strictly less than $b$, i.e., $\inf s < b$.

exists_between_of_forall_le theorem

 (sne : s.Nonempty) (tne : t.Nonempty) (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : (upperBounds s ∩ lowerBounds t).Nonempty

Full source

/-- If all elements of a nonempty set `s` are less than or equal to all elements
of a nonempty set `t`, then there exists an element between these sets. -/
theorem exists_between_of_forall_le (sne : s.Nonempty) (tne : t.Nonempty)
    (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : (upperBoundsupperBounds s ∩ lowerBounds t).Nonempty :=
  ⟨sInf t, fun x hx => le_csInf tne <| hst x hx, fun _ hy => csInf_le (sne.mono hst) hy⟩

Existence of Intermediate Element Between Nonempty Sets in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ and $t$ be nonempty subsets of $\alpha$ such that every element of $s$ is less than or equal to every element of $t$. Then there exists an element $z \in \alpha$ that is an upper bound for $s$ and a lower bound for $t$, i.e., $x \leq z \leq y$ for all $x \in s$ and $y \in t$.

csSup_singleton theorem

(a : α) : sSup { a } = a

Full source

/-- The supremum of a singleton is the element of the singleton -/
@[simp]
theorem csSup_singleton (a : α) : sSup {a} = a :=
  isGreatest_singleton.csSup_eq

Supremum of a Singleton Set Equals its Element

Informal description

In a conditionally complete lattice $\alpha$, the supremum of a singleton set $\{a\}$ is equal to its single element $a$, i.e., $\sup \{a\} = a$.

csInf_singleton theorem

(a : α) : sInf { a } = a

Full source

/-- The infimum of a singleton is the element of the singleton -/
@[simp]
theorem csInf_singleton (a : α) : sInf {a} = a :=
  isLeast_singleton.csInf_eq

Infimum of a Singleton Equals Its Element

Informal description

Let $\alpha$ be a conditionally complete lattice. For any element $a \in \alpha$, the infimum of the singleton set $\{a\}$ is equal to $a$, i.e., $\inf \{a\} = a$.

csSup_pair theorem

(a b : α) : sSup { a, b } = a ⊔ b

Full source

theorem csSup_pair (a b : α) : sSup {a, b} = a ⊔ b :=
  (@isLUB_pair _ _ a b).csSup_eq (insert_nonempty _ _)

Supremum of a Pair Equals Join in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice. For any two elements $a, b \in \alpha$, the supremum of the set $\{a, b\}$ is equal to the join of $a$ and $b$, i.e., $\sup \{a, b\} = a \sqcup b$.

csInf_pair theorem

(a b : α) : sInf { a, b } = a ⊓ b

Full source

theorem csInf_pair (a b : α) : sInf {a, b} = a ⊓ b :=
  (@isGLB_pair _ _ a b).csInf_eq (insert_nonempty _ _)

Infimum of a Pair Equals Their Meet

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$. The infimum of the two-element set $\{a, b\}$ is equal to the meet of $a$ and $b$, i.e., $\inf \{a, b\} = a \sqcap b$.

csInf_le_csSup theorem

(hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) : sInf s ≤ sSup s

Full source

/-- If a set is bounded below and above, and nonempty, its infimum is less than or equal to
its supremum. -/
theorem csInf_le_csSup (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) : sInf s ≤ sSup s :=
  isGLB_le_isLUB (isGLB_csInf ne hb) (isLUB_csSup ne ha) ne

Infimum is less than or equal to supremum in conditionally complete lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$ that is both bounded below and bounded above. Then the infimum of $s$ is less than or equal to its supremum, i.e., $\inf s \leq \sup s$.

csSup_union theorem

(hs : BddAbove s) (sne : s.Nonempty) (ht : BddAbove t) (tne : t.Nonempty) : sSup (s ∪ t) = sSup s ⊔ sSup t

Full source

/-- The `sSup` of a union of two sets is the max of the suprema of each subset, under the
assumptions that all sets are bounded above and nonempty. -/
theorem csSup_union (hs : BddAbove s) (sne : s.Nonempty) (ht : BddAbove t) (tne : t.Nonempty) :
    sSup (s ∪ t) = sSupsSup s ⊔ sSup t :=
  ((isLUB_csSup sne hs).union (isLUB_csSup tne ht)).csSup_eq sne.inl

Supremum of Union Equals Join of Suprema in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s, t \subseteq \alpha$ be two nonempty subsets that are both bounded above. Then the supremum of their union satisfies $\sup(s \cup t) = \sup s \sqcup \sup t$.

csInf_union theorem

(hs : BddBelow s) (sne : s.Nonempty) (ht : BddBelow t) (tne : t.Nonempty) : sInf (s ∪ t) = sInf s ⊓ sInf t

Full source

/-- The `sInf` of a union of two sets is the min of the infima of each subset, under the assumptions
that all sets are bounded below and nonempty. -/
theorem csInf_union (hs : BddBelow s) (sne : s.Nonempty) (ht : BddBelow t) (tne : t.Nonempty) :
    sInf (s ∪ t) = sInfsInf s ⊓ sInf t :=
  csSup_union (α := αᵒᵈ) hs sne ht tne

Infimum of Union Equals Meet of Infima in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s, t \subseteq \alpha$ be two nonempty subsets that are both bounded below. Then the infimum of their union satisfies $\inf(s \cup t) = \inf s \sqcap \inf t$.

csSup_inter_le theorem

(hs : BddAbove s) (ht : BddAbove t) (hst : (s ∩ t).Nonempty) : sSup (s ∩ t) ≤ sSup s ⊓ sSup t

Full source

/-- The supremum of an intersection of two sets is bounded by the minimum of the suprema of each
set, if all sets are bounded above and nonempty. -/
theorem csSup_inter_le (hs : BddAbove s) (ht : BddAbove t) (hst : (s ∩ t).Nonempty) :
    sSup (s ∩ t) ≤ sSupsSup s ⊓ sSup t :=
  (csSup_le hst) fun _ hx => le_inf (le_csSup hs hx.1) (le_csSup ht hx.2)

Supremum of Intersection is Bounded by Infimum of Suprema

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s, t \subseteq \alpha$ be two subsets that are both bounded above and whose intersection $s \cap t$ is nonempty. Then the supremum of the intersection satisfies $\sup(s \cap t) \leq \sup s \sqcap \sup t$.

le_csInf_inter theorem

: BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)

Full source

/-- The infimum of an intersection of two sets is bounded below by the maximum of the
infima of each set, if all sets are bounded below and nonempty. -/
theorem le_csInf_inter :
    BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInfsInf s ⊔ sInf t ≤ sInf (s ∩ t) :=
  csSup_inter_le (α := αᵒᵈ)

Infimum of Intersection Bounds Supremum of Infima

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s, t \subseteq \alpha$ be two subsets that are both bounded below and whose intersection $s \cap t$ is nonempty. Then the infimum of the intersection satisfies $\inf s \sqcup \inf t \leq \inf(s \cap t)$.

csSup_insert theorem

(hs : BddAbove s) (sne : s.Nonempty) : sSup (insert a s) = a ⊔ sSup s

Full source

/-- The supremum of `insert a s` is the maximum of `a` and the supremum of `s`, if `s` is
nonempty and bounded above. -/
@[simp]
theorem csSup_insert (hs : BddAbove s) (sne : s.Nonempty) : sSup (insert a s) = a ⊔ sSup s :=
  ((isLUB_csSup sne hs).insert a).csSup_eq (insert_nonempty a s)

Supremum of Inserted Element in Conditionally Complete Lattice: $\sup(\{a\} \cup s) = a \sqcup \sup s$

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s \subseteq \alpha$ be a nonempty subset that is bounded above. For any element $a \in \alpha$, the supremum of the set $\{a\} \cup s$ is equal to the join of $a$ and the supremum of $s$, i.e., \[ \sup(\{a\} \cup s) = a \sqcup \sup s. \]

csInf_insert theorem

(hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s

Full source

/-- The infimum of `insert a s` is the minimum of `a` and the infimum of `s`, if `s` is
nonempty and bounded below. -/
@[simp]
theorem csInf_insert (hs : BddBelow s) (sne : s.Nonempty) : sInf (insert a s) = a ⊓ sInf s :=
  csSup_insert (α := αᵒᵈ) hs sne

Infimum of Inserted Element in Conditionally Complete Lattice: $\inf(\{a\} \cup s) = a \sqcap \inf s$

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s \subseteq \alpha$ be a nonempty subset that is bounded below. For any element $a \in \alpha$, the infimum of the set $\{a\} \cup s$ is equal to the meet of $a$ and the infimum of $s$, i.e., \[ \inf(\{a\} \cup s) = a \sqcap \inf s. \]

csInf_Icc theorem

(h : a ≤ b) : sInf (Icc a b) = a

Full source

@[simp]
theorem csInf_Icc (h : a ≤ b) : sInf (Icc a b) = a :=
  (isGLB_Icc h).csInf_eq (nonempty_Icc.2 h)

Infimum of Closed Interval in Conditionally Complete Lattice

Informal description

For any elements $a$ and $b$ in a conditionally complete lattice with $a \leq b$, the infimum of the closed interval $[a, b]$ is equal to $a$, i.e., $\inf [a, b] = a$.

csInf_Ici theorem

: sInf (Ici a) = a

Full source

@[simp]
theorem csInf_Ici : sInf (Ici a) = a :=
  isLeast_Ici.csInf_eq

Infimum of Closed-Infinite Interval Equals Left Endpoint

Informal description

In a conditionally complete lattice $\alpha$, for any element $a \in \alpha$, the infimum of the closed-infinite interval $[a, \infty)$ is equal to $a$, i.e., $\inf [a, \infty) = a$.

csInf_Ico theorem

(h : a < b) : sInf (Ico a b) = a

Full source

@[simp]
theorem csInf_Ico (h : a < b) : sInf (Ico a b) = a :=
  (isGLB_Ico h).csInf_eq (nonempty_Ico.2 h)

Infimum of Half-Open Interval Equals Left Endpoint

Informal description

For any elements $a$ and $b$ in a conditionally complete lattice $\alpha$ with $a < b$, the infimum of the half-open interval $[a, b)$ is equal to $a$, i.e., $\inf [a, b) = a$.

csInf_Ioc theorem

[DenselyOrdered α] (h : a < b) : sInf (Ioc a b) = a

Full source

@[simp]
theorem csInf_Ioc [DenselyOrdered α] (h : a < b) : sInf (Ioc a b) = a :=
  (isGLB_Ioc h).csInf_eq (nonempty_Ioc.2 h)

Infimum of Half-Open Interval in Densely Ordered Lattices

Informal description

Let $\alpha$ be a densely ordered conditionally complete lattice, and let $a, b \in \alpha$ with $a < b$. Then the infimum of the half-open interval $(a, b]$ is equal to $a$, i.e., $\inf (a, b] = a$.

csInf_Ioi theorem

[NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a

Full source

@[simp]
theorem csInf_Ioi [NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a :=
  csInf_eq_of_forall_ge_of_forall_gt_exists_lt nonempty_Ioi (fun _ => le_of_lt) fun w hw => by
    simpa using exists_between hw

Infimum of Open Right Interval in Densely Ordered Lattice Without Maximal Elements

Informal description

Let $\alpha$ be a conditionally complete lattice with no maximal elements and a dense order. Then for any element $a \in \alpha$, the infimum of the open interval $(a, \infty)$ is equal to $a$, i.e., $\inf \{x \mid a < x\} = a$.

csInf_Ioo theorem

[DenselyOrdered α] (h : a < b) : sInf (Ioo a b) = a

Full source

@[simp]
theorem csInf_Ioo [DenselyOrdered α] (h : a < b) : sInf (Ioo a b) = a :=
  (isGLB_Ioo h).csInf_eq (nonempty_Ioo.2 h)

Infimum of Open Interval in Densely Ordered Lattice: $\inf (a, b) = a$

Informal description

Let $\alpha$ be a densely ordered conditionally complete lattice, and let $a, b \in \alpha$ with $a < b$. Then the infimum of the open interval $(a, b)$ is equal to $a$, i.e., $\inf (a, b) = a$.

csSup_Icc theorem

(h : a ≤ b) : sSup (Icc a b) = b

Full source

@[simp]
theorem csSup_Icc (h : a ≤ b) : sSup (Icc a b) = b :=
  (isLUB_Icc h).csSup_eq (nonempty_Icc.2 h)

Supremum of Closed Interval in Conditionally Complete Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a \leq b$. The supremum of the closed interval $[a, b]$ is equal to $b$, i.e., $\sup([a, b]) = b$.

csSup_Ico theorem

[DenselyOrdered α] (h : a < b) : sSup (Ico a b) = b

Full source

@[simp]
theorem csSup_Ico [DenselyOrdered α] (h : a < b) : sSup (Ico a b) = b :=
  (isLUB_Ico h).csSup_eq (nonempty_Ico.2 h)

Supremum of Half-Open Interval in Densely Ordered Lattice

Informal description

Let $\alpha$ be a densely ordered conditionally complete lattice. For any elements $a, b \in \alpha$ with $a < b$, the supremum of the half-open interval $[a, b)$ is equal to $b$, i.e., $\sup [a, b) = b$.

csSup_Iic theorem

: sSup (Iic a) = a

Full source

@[simp]
theorem csSup_Iic : sSup (Iic a) = a :=
  isGreatest_Iic.csSup_eq

Supremum of Lower Set Equals Endpoint

Informal description

For any element $a$ in a conditionally complete lattice $\alpha$, the supremum of the closed interval $(-\infty, a]$ is equal to $a$, i.e., $\sup(-\infty, a] = a$.

csSup_Iio theorem

[NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a

Full source

@[simp]
theorem csSup_Iio [NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt nonempty_Iio (fun _ => le_of_lt) fun w hw => by
    simpa [and_comm] using exists_between hw

Supremum of Open Left Interval in Densely Ordered Lattice Without Minimal Element

Informal description

Let $\alpha$ be a conditionally complete lattice with no minimal element and densely ordered. Then the supremum of the open interval $(-\infty, a)$ is equal to $a$, i.e., $\sup (-\infty, a) = a$.

csSup_Ioc theorem

(h : a < b) : sSup (Ioc a b) = b

Full source

@[simp]
theorem csSup_Ioc (h : a < b) : sSup (Ioc a b) = b :=
  (isLUB_Ioc h).csSup_eq (nonempty_Ioc.2 h)

Supremum of Half-Open Interval in Conditionally Complete Lattice

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $a, b \in \alpha$ with $a < b$. Then the supremum of the half-open interval $(a, b]$ is equal to $b$, i.e., $\sup (a, b] = b$.

csSup_Ioo theorem

[DenselyOrdered α] (h : a < b) : sSup (Ioo a b) = b

Full source

@[simp]
theorem csSup_Ioo [DenselyOrdered α] (h : a < b) : sSup (Ioo a b) = b :=
  (isLUB_Ioo h).csSup_eq (nonempty_Ioo.2 h)

Supremum of Open Interval in Densely Ordered Lattice

Informal description

Let $\alpha$ be a densely ordered conditionally complete lattice. For any elements $a, b \in \alpha$ with $a < b$, the supremum of the open interval $(a, b)$ is equal to $b$, i.e., $\sup (a, b) = b$.

csSup_eq_of_is_forall_le_of_forall_le_imp_ge theorem

 (hs : s.Nonempty) (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ ub, (∀ a ∈ s, a ≤ ub) → b ≤ ub) : sSup s = b

Full source

/-- Introduction rule to prove that `b` is the supremum of `s`: it suffices to check that
1) `b` is an upper bound
2) every other upper bound `b'` satisfies `b ≤ b'`. -/
theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge (hs : s.Nonempty) (h_is_ub : ∀ a ∈ s, a ≤ b)
    (h_b_le_ub : ∀ ub, (∀ a ∈ s, a ≤ ub) → b ≤ ub) : sSup s = b :=
  (csSup_le hs h_is_ub).antisymm ((h_b_le_ub _) fun _ => le_csSup ⟨b, h_is_ub⟩)

Characterization of Supremum via Upper Bounds

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a nonempty subset of $\alpha$. If $b$ is an upper bound for $s$ (i.e., $a \leq b$ for all $a \in s$) and for any other upper bound $ub$ of $s$ we have $b \leq ub$, then the supremum of $s$ equals $b$, i.e., $\sup s = b$.

sup_eq_top_of_top_mem theorem

[OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤

Full source

lemma sup_eq_top_of_top_mem [OrderTop α] (h : ⊤⊤ ∈ s) : sSup s = ⊤ :=
  top_unique <| le_csSup (OrderTop.bddAbove s) h

Supremum of Set Containing Top is Top

Informal description

Let $\alpha$ be a conditionally complete lattice with a top element $\top$. For any subset $s \subseteq \alpha$ containing $\top$, the supremum of $s$ is equal to $\top$, i.e., $\sup s = \top$.

inf_eq_bot_of_bot_mem theorem

[OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥

Full source

lemma inf_eq_bot_of_bot_mem [OrderBot α] (h : ⊥⊥ ∈ s) : sInf s = ⊥ :=
  bot_unique <| csInf_le (OrderBot.bddBelow s) h

Infimum of Set Containing Bottom is Bottom

Informal description

Let $\alpha$ be a conditionally complete lattice with a bottom element $\bot$. For any subset $s \subseteq \alpha$ containing $\bot$, the infimum of $s$ is equal to $\bot$.

Pi.conditionallyCompleteLattice instance

 {ι : Type*} {α : ι → Type*} [∀ i, ConditionallyCompleteLattice (α i)] : ConditionallyCompleteLattice (∀ i, α i)

Full source

instance Pi.conditionallyCompleteLattice {ι : Type*} {α : ι → Type*}
    [∀ i, ConditionallyCompleteLattice (α i)] : ConditionallyCompleteLattice (∀ i, α i) :=
  { Pi.instLattice, Pi.supSet, Pi.infSet with
    le_csSup := fun _ f ⟨g, hg⟩ hf i =>
      le_csSup ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
    csSup_le := fun s _ hs hf i =>
      (csSup_le (by haveI := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ =>
        hb ▸ hf hg i
    csInf_le := fun _ f ⟨g, hg⟩ hf i =>
      csInf_le ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
    le_csInf := fun s _ hs hf i =>
      (le_csInf (by haveI := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ =>
        hb ▸ hf hg i }

Pointwise Conditionally Complete Lattice Structure on Product Types

Informal description

For any family of types $\alpha_i$ indexed by $i \in \iota$, where each $\alpha_i$ is a conditionally complete lattice, the product type $\prod_{i \in \iota} \alpha_i$ is also a conditionally complete lattice. The supremum and infimum operations are defined pointwise: for a nonempty and bounded subset $S \subseteq \prod_{i \in \iota} \alpha_i$, we have $(\sup S)(i) = \sup \{f(i) \mid f \in S\}$ and $(\inf S)(i) = \inf \{f(i) \mid f \in S\}$ for each $i \in \iota$.

exists_lt_of_lt_csSup theorem

(hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a

Full source

/-- When `b < sSup s`, there is an element `a` in `s` with `b < a`, if `s` is nonempty and the order
is a linear order. -/
theorem exists_lt_of_lt_csSup (hs : s.Nonempty) (hb : b < sSup s) : ∃ a ∈ s, b < a := by
  contrapose! hb
  exact csSup_le hs hb

Existence of Element Above Given Bound in Nonempty Bounded Set

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$. If $b$ is an element such that $b < \sup s$, then there exists an element $a \in s$ with $b < a$.

exists_lt_of_csInf_lt theorem

(hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b

Full source

/-- When `sInf s < b`, there is an element `a` in `s` with `a < b`, if `s` is nonempty and the order
is a linear order. -/
theorem exists_lt_of_csInf_lt (hs : s.Nonempty) (hb : sInf s < b) : ∃ a ∈ s, a < b :=
  exists_lt_of_lt_csSup (α := αᵒᵈ) hs hb

Existence of Element Below Given Bound in Nonempty Set: $\inf s < b \rightarrow \exists a \in s, a < b$

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$. If the infimum of $s$ is less than an element $b \in \alpha$, then there exists an element $a \in s$ such that $a < b$.

lt_csSup_iff theorem

(hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b

Full source

theorem lt_csSup_iff (hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b :=
  lt_isLUB_iff <| isLUB_csSup hs hb

Characterization of Elements Below Supremum in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order, $s$ a nonempty subset of $\alpha$ that is bounded above, and $a$ an element of $\alpha$. Then $a$ is less than the supremum of $s$ if and only if there exists an element $b \in s$ such that $a < b$. In other words: $$a < \sup s \leftrightarrow \exists b \in s, a < b.$$

csInf_lt_iff theorem

(hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b ∈ s, b < a

Full source

theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInfsInf s < a ↔ ∃ b ∈ s, b < a :=
  isGLB_lt_iff <| isGLB_csInf hs hb

Characterization of Infimum Being Less Than an Element in Conditionally Complete Linear Orders

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$ that is bounded below. Then the infimum $\inf s$ is less than an element $a \in \alpha$ if and only if there exists some element $b \in s$ such that $b < a$.

csSup_of_not_bddAbove theorem

(hs : ¬BddAbove s) : sSup s = sSup ∅

Full source

@[simp] lemma csSup_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup ∅ :=
  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs

Supremum of Unbounded Set Equals Supremum of Empty Set

Informal description

For any subset $s$ of a conditionally complete linear order $\alpha$ that is not bounded above, the supremum of $s$ equals the supremum of the empty set.

ciSup_of_not_bddAbove theorem

(hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅

Full source

@[simp] lemma ciSup_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup ∅ :=
  csSup_of_not_bddAbove hf

Supremum of Unbounded Function Equals Supremum of Empty Set

Informal description

For a function $f$ whose range is not bounded above in a conditionally complete linear order, the supremum of $f$ over its domain equals the supremum of the empty set, i.e., $\bigsqcup_i f(i) = \text{sSup} \emptyset$.

csSup_eq_univ_of_not_bddAbove theorem

(hs : ¬BddAbove s) : sSup s = sSup univ

Full source

lemma csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ := by
  rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)]
  contrapose! hs
  exact hs.mono (subset_univ _)

Supremum of Unbounded Set Equals Supremum of Universe

Informal description

For any subset $s$ of a conditionally complete linear order $\alpha$ that is not bounded above, the supremum of $s$ equals the supremum of the entire space $\alpha$, i.e., $\sup s = \sup \alpha$.

ciSup_eq_univ_of_not_bddAbove theorem

(hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ

Full source

lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ :=
  csSup_eq_univ_of_not_bddAbove hf

Supremum of Unbounded Function Equals Supremum of Universe

Informal description

For a function $f : \iota \to \alpha$ whose range is not bounded above in a conditionally complete linear order $\alpha$, the supremum of $f$ over its domain equals the supremum of the entire space $\alpha$, i.e., $\bigsqcup_{i} f(i) = \sup \alpha$.

csInf_of_not_bddBelow theorem

(hs : ¬BddBelow s) : sInf s = sInf ∅

Full source

@[simp] lemma csInf_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf ∅ :=
  ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow s hs

Infimum of Unbounded Below Set Equals Infimum of Empty Set

Informal description

For a conditionally complete linear order $\alpha$ and a subset $s \subseteq \alpha$ that is not bounded below, the infimum of $s$ equals the infimum of the empty set, i.e., $\inf s = \inf \emptyset$.

ciInf_of_not_bddBelow theorem

(hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf ∅

Full source

@[simp] lemma ciInf_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf ∅ :=
  csInf_of_not_bddBelow hf

Infimum of Unbounded Below Function Equals Infimum of Empty Set

Informal description

For a conditionally complete linear order $\alpha$ and a function $f : \iota \to \alpha$ whose range is not bounded below, the infimum of $f$ over all indices equals the infimum of the empty set, i.e., $\inf_{i} f(i) = \inf \emptyset$.

csInf_eq_univ_of_not_bddBelow theorem

(hs : ¬BddBelow s) : sInf s = sInf univ

Full source

lemma csInf_eq_univ_of_not_bddBelow (hs : ¬BddBelow s) : sInf s = sInf univ :=
  csSup_eq_univ_of_not_bddAbove (α := αᵒᵈ) hs

Infimum of Unbounded Below Set Equals Infimum of Universe

Informal description

For any subset $s$ of a conditionally complete linear order $\alpha$ that is not bounded below, the infimum of $s$ equals the infimum of the entire space $\alpha$, i.e., $\inf s = \inf \alpha$.

ciInf_eq_univ_of_not_bddBelow theorem

(hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf univ

Full source

lemma ciInf_eq_univ_of_not_bddBelow (hf : ¬BddBelow (range f)) : ⨅ i, f i = sInf univ :=
  csInf_eq_univ_of_not_bddBelow hf

Infimum of Unbounded Below Function Equals Infimum of Universe

Informal description

For a conditionally complete linear order $\alpha$ and a function $f : \iota \to \alpha$ whose range is not bounded below, the infimum of $f$ over all indices equals the infimum of the entire space $\alpha$, i.e., $\inf_{i} f(i) = \inf \alpha$.

csSup_eq_csSup_of_forall_exists_le theorem

{s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) : sSup s = sSup t

Full source

/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
    (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
    sSup s = sSup t := by
  rcases eq_empty_or_nonempty s with rfl|s_ne
  · have : t = ∅ := eq_empty_of_forall_not_mem (fun y yt ↦ by simpa using ht y yt)
    rw [this]
  rcases eq_empty_or_nonempty t with rfl|t_ne
  · have : s = ∅ := eq_empty_of_forall_not_mem (fun x xs ↦ by simpa using hs x xs)
    rw [this]
  by_cases B : BddAbove s ∨ BddAbove t
  · have Bs : BddAbove s := by
      rcases B with hB|⟨b, hb⟩
      · exact hB
      · refine ⟨b, fun x hx ↦ ?_⟩
        rcases hs x hx with ⟨y, hy, hxy⟩
        exact hxy.trans (hb hy)
    have Bt : BddAbove t := by
      rcases B with ⟨b, hb⟩|hB
      · refine ⟨b, fun y hy ↦ ?_⟩
        rcases ht y hy with ⟨x, hx, hyx⟩
        exact hyx.trans (hb hx)
      · exact hB
    apply le_antisymm
    · apply csSup_le s_ne (fun x hx ↦ ?_)
      rcases hs x hx with ⟨y, yt, hxy⟩
      exact hxy.trans (le_csSup Bt yt)
    · apply csSup_le t_ne (fun y hy ↦ ?_)
      rcases ht y hy with ⟨x, xs, hyx⟩
      exact hyx.trans (le_csSup Bs xs)
  · simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]

Suprema Equality under Mutual Bounding Condition

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $s$ and $t$ be subsets of $\alpha$. If for every $x \in s$ there exists $y \in t$ such that $x \leq y$, and conversely for every $y \in t$ there exists $x \in s$ such that $y \leq x$, then the suprema of $s$ and $t$ are equal, i.e., $\sup s = \sup t$.

csInf_eq_csInf_of_forall_exists_le theorem

{s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) : sInf s = sInf t

Full source

/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
`s` and `t` have the same infimum. This holds even when the sets may be empty or unbounded. -/
theorem csInf_eq_csInf_of_forall_exists_le {s t : Set α}
    (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
    sInf s = sInf t :=
  csSup_eq_csSup_of_forall_exists_le (α := αᵒᵈ) hs ht

Infima Equality under Mutual Bounding Condition

Informal description

Let $\alpha$ be a conditionally complete linear order, and let $s$ and $t$ be subsets of $\alpha$. If for every $x \in s$ there exists $y \in t$ such that $y \leq x$, and conversely for every $y \in t$ there exists $x \in s$ such that $x \leq y$, then the infima of $s$ and $t$ are equal, i.e., $\inf s = \inf t$.

sSup_iUnion_Iic theorem

(f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i, f i

Full source

lemma sSup_iUnion_Iic (f : ι → α) : sSup (⋃ (i : ι), Iic (f i)) = ⨆ i, f i := by
  apply csSup_eq_csSup_of_forall_exists_le
  · rintro x ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨f i, mem_range_self _, hi⟩
  · rintro x ⟨i, rfl⟩
    exact ⟨f i, mem_iUnion_of_mem i le_rfl, le_rfl⟩

Supremum of Union of Lower Sets Equals Supremum of Function Range

Informal description

Let $\alpha$ be a conditionally complete linear order and let $f : \iota \to \alpha$ be a function. The supremum of the union of all lower sets $\{x \in \alpha \mid x \leq f(i)\}$ for $i \in \iota$ equals the supremum of the range of $f$, i.e., \[ \sup \left( \bigcup_{i \in \iota} \{x \in \alpha \mid x \leq f(i)\} \right) = \sup_{i \in \iota} f(i). \]

sInf_iUnion_Ici theorem

(f : ι → α) : sInf (⋃ (i : ι), Ici (f i)) = ⨅ i, f i

Full source

lemma sInf_iUnion_Ici (f : ι → α) : sInf (⋃ (i : ι), Ici (f i)) = ⨅ i, f i :=
  sSup_iUnion_Iic (α := αᵒᵈ) f

Infimum of Union of Upper Sets Equals Infimum of Function Range

Informal description

Let $\alpha$ be a conditionally complete linear order and let $f : \iota \to \alpha$ be a function. The infimum of the union of all upper sets $\{x \in \alpha \mid x \geq f(i)\}$ for $i \in \iota$ equals the infimum of the range of $f$, i.e., \[ \inf \left( \bigcup_{i \in \iota} \{x \in \alpha \mid x \geq f(i)\} \right) = \inf_{i \in \iota} f(i). \]

csInf_eq_bot_of_bot_mem theorem

[OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥

Full source

theorem csInf_eq_bot_of_bot_mem [OrderBot α] {s : Set α} (hs : ⊥⊥ ∈ s) : sInf s = ⊥ :=
  eq_bot_iff.2 <| csInf_le (OrderBot.bddBelow s) hs

Infimum of Set Containing Bottom is Bottom

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element $\bot$, and let $s$ be a subset of $\alpha$ containing $\bot$. Then the infimum of $s$ is equal to $\bot$.

csSup_eq_top_of_top_mem theorem

[OrderTop α] {s : Set α} (hs : ⊤ ∈ s) : sSup s = ⊤

Full source

theorem csSup_eq_top_of_top_mem [OrderTop α] {s : Set α} (hs : ⊤⊤ ∈ s) : sSup s = ⊤ :=
  csInf_eq_bot_of_bot_mem (α := αᵒᵈ) hs

Supremum of Set Containing Top is Top

Informal description

Let $\alpha$ be a conditionally complete linear order with a top element $\top$, and let $s$ be a subset of $\alpha$ containing $\top$. Then the supremum of $s$ is equal to $\top$.

sInf_eq_argmin_on theorem

(hs : s.Nonempty) : sInf s = argminOn id s hs

Full source

theorem sInf_eq_argmin_on (hs : s.Nonempty) : sInf s = argminOn id s hs :=
  IsLeast.csInf_eq ⟨argminOn_mem _ _ _, fun _ ha => argminOn_le id _ ha⟩

Infimum as Argument of Minimum Identity Function

Informal description

Let $\alpha$ be a conditionally complete linear order and $s$ a nonempty subset of $\alpha$. Then the infimum of $s$ is equal to the argument of the minimum of the identity function on $s$, i.e., $\inf s = \text{argmin}_{x \in s} \, x$.

isLeast_csInf theorem

(hs : s.Nonempty) : IsLeast s (sInf s)

Full source

theorem isLeast_csInf (hs : s.Nonempty) : IsLeast s (sInf s) := by
  rw [sInf_eq_argmin_on hs]
  exact ⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩

Infimum is the Least Element in Nonempty Sets

Informal description

For any nonempty subset $s$ of a conditionally complete linear order $\alpha$, the infimum $\inf s$ is the least element of $s$, i.e., $\inf s \in s$ and $\inf s \leq x$ for all $x \in s$.

le_csInf_iff' theorem

(hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s

Full source

theorem le_csInf_iff' (hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s :=
  le_isGLB_iff (isLeast_csInf hs).isGLB

Characterization of Infimum via Lower Bounds in Conditionally Complete Linear Orders

Informal description

For any nonempty subset $s$ of a conditionally complete linear order $\alpha$, an element $b \in \alpha$ satisfies $b \leq \inf s$ if and only if $b$ is a lower bound of $s$, i.e., $b \leq x$ for all $x \in s$.

csInf_mem theorem

(hs : s.Nonempty) : sInf s ∈ s

Full source

theorem csInf_mem (hs : s.Nonempty) : sInfsInf s ∈ s :=
  (isLeast_csInf hs).1

Infimum Belongs to Nonempty Set in Conditionally Complete Linear Order

Informal description

For any nonempty subset $s$ of a conditionally complete linear order $\alpha$, the infimum $\inf s$ is an element of $s$.

MonotoneOn.map_csInf theorem

 {β : Type*} [ConditionallyCompleteLattice β] {f : α → β} (hf : MonotoneOn f s) (hs : s.Nonempty) :
  f (sInf s) = sInf (f '' s)

Full source

theorem MonotoneOn.map_csInf {β : Type*} [ConditionallyCompleteLattice β] {f : α → β}
    (hf : MonotoneOn f s) (hs : s.Nonempty) : f (sInf s) = sInf (f '' s) :=
  (hf.map_isLeast (isLeast_csInf hs)).csInf_eq.symm

Monotonicity Preserves Infima: $f(\inf s) = \inf (f '' s)$

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a function that is monotone on a nonempty subset $s \subseteq \alpha$. Then the image of the infimum of $s$ under $f$ equals the infimum of the image of $s$ under $f$, i.e., $f(\inf s) = \inf (f '' s)$.

Monotone.map_csInf theorem

 {β : Type*} [ConditionallyCompleteLattice β] {f : α → β} (hf : Monotone f) (hs : s.Nonempty) :
  f (sInf s) = sInf (f '' s)

Full source

theorem Monotone.map_csInf {β : Type*} [ConditionallyCompleteLattice β] {f : α → β}
    (hf : Monotone f) (hs : s.Nonempty) : f (sInf s) = sInf (f '' s) :=
  (hf.map_isLeast (isLeast_csInf hs)).csInf_eq.symm

Monotonicity Preserves Infima: $f(\inf s) = \inf (f '' s)$

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any nonempty subset $s \subseteq \alpha$, the image of the infimum of $s$ under $f$ equals the infimum of the image of $s$ under $f$, i.e., \[ f(\inf s) = \inf (f '' s). \]

csInf_univ theorem

[ConditionallyCompleteLattice α] [OrderBot α] : sInf (univ : Set α) = ⊥

Full source

@[simp]
theorem csInf_univ [ConditionallyCompleteLattice α] [OrderBot α] : sInf (univ : Set α) = ⊥ :=
  isLeast_univ.csInf_eq

Infimum of Universal Set in Conditionally Complete Lattice with Bottom is Bottom

Informal description

Let $\alpha$ be a conditionally complete lattice with a bottom element $\bot$. Then the infimum of the universal set (i.e., the entire set $\alpha$) is equal to $\bot$, i.e., $\inf \alpha = \bot$.

csSup_empty theorem

: (sSup ∅ : α) = ⊥

Full source

@[simp]
theorem csSup_empty : (sSup ∅ : α) = ⊥ :=
  ConditionallyCompleteLinearOrderBot.csSup_empty

Supremum of Empty Set in Conditionally Complete Linear Order with Bottom Element is Bottom

Informal description

In a conditionally complete linear order with a bottom element $\bot$, the supremum of the empty set is equal to $\bot$, i.e., $\sup(\emptyset) = \bot$.

isLUB_csSup' theorem

{s : Set α} (hs : BddAbove s) : IsLUB s (sSup s)

Full source

theorem isLUB_csSup' {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s) := by
  rcases eq_empty_or_nonempty s with (rfl | hne)
  · simp only [csSup_empty, isLUB_empty]
  · exact isLUB_csSup hne hs

Supremum is Least Upper Bound for Bounded Sets in Conditionally Complete Lattices

Informal description

Let $\alpha$ be a conditionally complete lattice and $s$ a subset of $\alpha$ that is bounded above. Then the supremum $\sup s$ is the least upper bound of $s$, meaning: 1. $\sup s$ is an upper bound of $s$ (i.e., $x \leq \sup s$ for all $x \in s$), and 2. $\sup s$ is less than or equal to any other upper bound of $s$.

csSup_le_iff' theorem

{s : Set α} (hs : BddAbove s) {a : α} : sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a

Full source

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `csSup_le_iff`. -/
theorem csSup_le_iff' {s : Set α} (hs : BddAbove s) {a : α} : sSupsSup s ≤ a ↔ ∀ x ∈ s, x ≤ a :=
  isLUB_le_iff (isLUB_csSup' hs)

Supremum Comparison Criterion in Conditionally Complete Linear Orders with Bottom

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element $\bot$, and let $s$ be a subset of $\alpha$ that is bounded above. For any element $a \in \alpha$, the supremum $\sup s$ is less than or equal to $a$ if and only if every element $x \in s$ satisfies $x \leq a$.

csSup_le' theorem

{s : Set α} {a : α} (h : a ∈ upperBounds s) : sSup s ≤ a

Full source

theorem csSup_le' {s : Set α} {a : α} (h : a ∈ upperBounds s) : sSup s ≤ a :=
  (csSup_le_iff' ⟨a, h⟩).2 h

Supremum is Less Than or Equal to Any Upper Bound

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $s$ be a subset of $\alpha$. If $a$ is an upper bound of $s$, then the supremum of $s$ satisfies $\sup s \leq a$.

lt_csSup_iff' theorem

(hb : BddAbove s) : a < sSup s ↔ ∃ b ∈ s, a < b

Full source

/-- In conditionally complete orders with a bottom element, the nonempty condition can be omitted
from `lt_csSup_iff`. -/
theorem lt_csSup_iff' (hb : BddAbove s) : a < sSup s ↔ ∃ b ∈ s, a < b := by
  simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff' hb).not

Characterization of Strict Upper Bounds via Supremum in Bounded Sets

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element $\bot$, and let $s$ be a subset of $\alpha$ that is bounded above. For any element $a \in \alpha$, we have $a < \sup s$ if and only if there exists an element $b \in s$ such that $a < b$.

le_csSup_iff' theorem

{s : Set α} {a : α} (h : BddAbove s) : a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b

Full source

theorem le_csSup_iff' {s : Set α} {a : α} (h : BddAbove s) :
    a ≤ sSup s ↔ ∀ b, b ∈ upperBounds s → a ≤ b :=
  ⟨fun h _ hb => le_trans h (csSup_le' hb), fun hb => hb _ fun _ => le_csSup h⟩

Characterization of Supremum via Upper Bounds in Bounded Sets

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $s$ be a subset of $\alpha$ that is bounded above. For any element $a \in \alpha$, we have $a \leq \sup s$ if and only if $a$ is a lower bound for the set of upper bounds of $s$ (i.e., $a \leq b$ for every upper bound $b$ of $s$).

le_csInf_iff'' theorem

{s : Set α} {a : α} (ne : s.Nonempty) : a ≤ sInf s ↔ ∀ b : α, b ∈ s → a ≤ b

Full source

theorem le_csInf_iff'' {s : Set α} {a : α} (ne : s.Nonempty) :
    a ≤ sInf s ↔ ∀ b : α, b ∈ s → a ≤ b :=
  le_csInf_iff (OrderBot.bddBelow _) ne

Characterization of Lower Bounds via Infimum in Nonempty Sets

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $s$ be a nonempty subset of $\alpha$. For any element $a \in \alpha$, we have $a \leq \inf s$ if and only if $a$ is a lower bound for $s$ (i.e., $a \leq b$ for all $b \in s$).

csInf_le' theorem

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

Full source

theorem csInf_le' (h : a ∈ s) : sInf s ≤ a := csInf_le (OrderBot.bddBelow _) h

Infimum is Below Any Element in Nonempty Set

Informal description

For any element $a$ in a nonempty subset $s$ of a conditionally complete linear order with a bottom element, the infimum of $s$ is less than or equal to $a$.

exists_lt_of_lt_csSup' theorem

{s : Set α} {a : α} (h : a < sSup s) : ∃ b ∈ s, a < b

Full source

theorem exists_lt_of_lt_csSup' {s : Set α} {a : α} (h : a < sSup s) : ∃ b ∈ s, a < b := by
  contrapose! h
  exact csSup_le' h

Existence of Element Above in Supremum Condition (With Bottom Element)

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element, and let $s$ be a subset of $\alpha$. For any element $a \in \alpha$, if $a$ is strictly less than the supremum of $s$, then there exists an element $b \in s$ such that $a < b$.

not_mem_of_lt_csInf' theorem

{x : α} {s : Set α} (h : x < sInf s) : x ∉ s

Full source

theorem not_mem_of_lt_csInf' {x : α} {s : Set α} (h : x < sInf s) : x ∉ s :=
  not_mem_of_lt_csInf h (OrderBot.bddBelow s)

Elements Below Infimum Are Not in the Set (With Bottom Element)

Informal description

Let $\alpha$ be a conditionally complete linear order with a bottom element $\bot$, and let $s$ be a subset of $\alpha$. If an element $x \in \alpha$ satisfies $x < \inf s$, then $x$ does not belong to $s$.

csInf_le_csInf' theorem

{s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) : sInf s ≤ sInf t

Full source

theorem csInf_le_csInf' {s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) : sInf s ≤ sInf t :=
  csInf_le_csInf (OrderBot.bddBelow s) h₁ h₂

Monotonicity of Infimum under Inclusion in Conditionally Complete Lattices (Nonempty Subset Version)

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ and $t$ be subsets of $\alpha$ such that $t$ is nonempty and $t \subseteq s$. Then the infimum of $s$ is less than or equal to the infimum of $t$, i.e., $\inf s \leq \inf t$.

csSup_le_csSup' theorem

{s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) : sSup s ≤ sSup t

Full source

theorem csSup_le_csSup' {s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) : sSup s ≤ sSup t := by
  rcases eq_empty_or_nonempty s with rfl | h
  · rw [csSup_empty]
    exact bot_le
  · exact csSup_le_csSup h₁ h h₂

Monotonicity of Supremum under Inclusion in Conditionally Complete Lattices (Generalized)

Informal description

Let $\alpha$ be a conditionally complete lattice, and let $s$ and $t$ be subsets of $\alpha$ such that $t$ is bounded above and $s \subseteq t$. Then the supremum of $s$ is less than or equal to the supremum of $t$, i.e., $\sup s \leq \sup t$.

WithTop.isLUB_sSup' theorem

{β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : s.Nonempty) : IsLUB s (sSup s)

Full source

/-- The `sSup` of a non-empty set is its least upper bound for a conditionally
complete lattice with a top. -/
theorem isLUB_sSup' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
    (hs : s.Nonempty) : IsLUB s (sSup s) := by
  classical
  constructor
  · show iteite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · show iteite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)

Supremum is Least Upper Bound in $\text{WithTop}\ \beta$ for Nonempty Sets

Informal description

Let $\beta$ be a conditionally complete lattice and $s$ a nonempty subset of $\text{WithTop}\ \beta$ (the type $\beta$ extended with a top element $\top$). Then the supremum $\sup s$ is the least upper bound of $s$, meaning that $\sup s$ is an upper bound for $s$ and any other upper bound for $s$ is greater than or equal to $\sup s$.

WithTop.isLUB_sSup theorem

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

Full source

theorem isLUB_sSup (s : Set (WithTop α)) : IsLUB s (sSup s) := by
  rcases s.eq_empty_or_nonempty with rfl | hs
  · simp [sSup]
  · exact isLUB_sSup' hs

Supremum is Least Upper Bound in $\text{WithTop}\ \alpha$

Informal description

Let $\alpha$ be a type equipped with a supremum operation. For any subset $s$ of $\text{WithTop}\ \alpha$ (the type $\alpha$ extended with a top element $\top$), the supremum $\sup s$ is the least upper bound of $s$. This means that $\sup s$ is an upper bound for all elements of $s$, and any other upper bound for $s$ is greater than or equal to $\sup s$.

WithTop.isGLB_sInf' theorem

{β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : BddBelow s) : IsGLB s (sInf s)

Full source

/-- The `sInf` of a bounded-below set is its greatest lower bound for a conditionally
complete lattice with a top. -/
theorem isGLB_sInf' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
    (hs : BddBelow s) : IsGLB s (sInf s) := by
  classical
  constructor
  · show iteite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · show iteite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

Infimum is Greatest Lower Bound in $\text{WithTop}\ \beta$ for Bounded Below Sets

Informal description

Let $\beta$ be a conditionally complete lattice and $s$ a subset of $\text{WithTop}\ \beta$ (the type $\beta$ extended with a top element $\top$) that is bounded below. Then the infimum $\inf s$ is the greatest lower bound of $s$, meaning that $\inf s$ is a lower bound for $s$ and any other lower bound for $s$ is less than or equal to $\inf s$.

WithTop.isGLB_sInf theorem

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

Full source

theorem isGLB_sInf (s : Set (WithTop α)) : IsGLB s (sInf s) := by
  by_cases hs : BddBelow s
  · exact isGLB_sInf' hs
  · exfalso
    apply hs
    use ⊥
    intro _ _
    exact bot_le

Greatest Lower Bound Property for Infima in $\text{WithTop}\ \alpha$

Informal description

For any subset $s$ of the type $\text{WithTop}\ \alpha$ (where $\alpha$ is extended with a top element $\top$), the infimum $\inf s$ is the greatest lower bound of $s$. This means that $\inf s$ is a lower bound for all elements in $s$, and any other lower bound of $s$ is less than or equal to $\inf s$.

WithTop.instCompleteLinearOrder instance

: CompleteLinearOrder (WithTop α)

Full source

noncomputable instance : CompleteLinearOrder (WithTop α) where
  __ := linearOrder
  __ := LinearOrder.toBiheytingAlgebra
  le_sSup s := (isLUB_sSup s).1
  sSup_le s := (isLUB_sSup s).2
  le_sInf s := (isGLB_sInf s).2
  sInf_le s := (isGLB_sInf s).1

Complete Linear Order Structure on `WithTop α`

Informal description

The type `WithTop α`, obtained by adding a top element $\top$ to a conditionally complete linear order $\alpha$, forms a complete linear order. In this structure, every subset has both a supremum and an infimum, and the order is total. This extends the conditionally complete lattice structure on $\alpha$ to handle cases involving $\top$ and ensures that all subsets, including those containing $\top$, have well-defined suprema and infima.

WithTop.coe_sSup theorem

{s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, ↑a : WithTop α)

Full source

/-- A version of `WithTop.coe_sSup'` with a more convenient but less general statement. -/
@[norm_cast]
theorem coe_sSup {s : Set α} (hb : BddAbove s) : ↑(sSup s) = (⨆ a ∈ s, ↑a : WithTop α) := by
  rw [coe_sSup' hb, sSup_image]

Supremum Preservation under Canonical Embedding to $\text{WithTop}\ \alpha$ for Bounded Above Sets

Informal description

Let $\alpha$ be a type with a supremum operation, and let $s$ be a subset of $\alpha$ that is bounded above. Then the image of the supremum of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is equal to the supremum of the images of all elements of $s$ under this embedding. In other words, if $s \subseteq \alpha$ is bounded above, then $\uparrow(\sup s) = \sup \{\uparrow a \mid a \in s\}$ in $\text{WithTop}\ \alpha$.

WithTop.coe_sInf theorem

{s : Set α} (hs : s.Nonempty) (h's : BddBelow s) : ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α)

Full source

/-- A version of `WithTop.coe_sInf'` with a more convenient but less general statement. -/
@[norm_cast]
theorem coe_sInf {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
    ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α) := by
  rw [coe_sInf' hs h's, sInf_image]

Infimum Preservation under Canonical Embedding to `WithTop α` (Simplified Version)

Informal description

For a nonempty set $s$ of elements in a type $\alpha$ that is bounded below, the image of the infimum of $s$ under the canonical embedding $\alpha \to \text{WithTop}\ \alpha$ is equal to the infimum of the images of the elements of $s$ in $\text{WithTop}\ \alpha$. In other words, $\uparrow(\inf s) = \inf_{a \in s} \uparrow a$.

Monotone.le_csSup_image theorem

{s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddAbove s) : f c ≤ sSup (f '' s)

Full source

theorem le_csSup_image {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddAbove s) :
    f c ≤ sSup (f '' s) :=
  le_csSup (map_bddAbove h_mono h_bdd) (mem_image_of_mem f hcs)

Monotone Function Preserves Supremum Inequality

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any nonempty subset $s \subseteq \alpha$ that is bounded above and any element $c \in s$, we have $f(c) \leq \sup f(s)$, where $f(s)$ denotes the image of $s$ under $f$.

Monotone.csSup_image_le theorem

{s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ upperBounds s) : sSup (f '' s) ≤ f B

Full source

theorem csSup_image_le {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ upperBounds s) :
    sSup (f '' s) ≤ f B :=
  csSup_le (Nonempty.image f hs) (h_mono.mem_upperBounds_image hB)

Monotonicity Preserves Supremum Inequality for Images

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any nonempty subset $s \subseteq \alpha$ and any upper bound $B$ of $s$, the supremum of the image $f(s)$ satisfies $\sup f(s) \leq f(B)$.

Monotone.csInf_image_le theorem

{s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) : sInf (f '' s) ≤ f c

Full source

theorem csInf_image_le {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) :
    sInf (f '' s) ≤ f c := by
  let f' : αᵒᵈ → βᵒᵈ := f
  exact le_csSup_image (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hcs h_bdd

Monotone Function Preserves Infimum Inequality

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any nonempty subset $s \subseteq \alpha$ that is bounded below and any element $c \in s$, we have $\inf f(s) \leq f(c)$, where $f(s)$ denotes the image of $s$ under $f$.

Monotone.le_csInf_image theorem

{s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) : f B ≤ sInf (f '' s)

Full source

theorem le_csInf_image {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) :
    f B ≤ sInf (f '' s) := by
  let f' : αᵒᵈ → βᵒᵈ := f
  exact csSup_image_le (α := αᵒᵈ) (β := βᵒᵈ)
    (show Monotone f' from fun x y hxy => h_mono hxy) hs hB

Monotonicity Preserves Infimum Inequality for Images

Informal description

Let $\alpha$ and $\beta$ be conditionally complete lattices, and let $f : \alpha \to \beta$ be a monotone function. For any nonempty subset $s \subseteq \alpha$ and any lower bound $B$ of $s$, we have $f(B) \leq \inf f(s)$, where $f(s)$ denotes the image of $s$ under $f$.

MonotoneOn.csInf_eq_of_subset_of_forall_exists_le theorem

 [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α} (ht : BddBelow (f '' t)) (hf : MonotoneOn f t)
  (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) : sInf (f '' s) = sInf (f '' t)

Full source

lemma MonotoneOn.csInf_eq_of_subset_of_forall_exists_le
    [Preorder α] [ConditionallyCompleteLattice β] {f : α → β}
    {s t : Set α} (ht : BddBelow (f '' t)) (hf : MonotoneOn f t)
    (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
    sInf (f '' s) = sInf (f '' t) := by
  obtain rfl | hs := Set.eq_empty_or_nonempty s
  · obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_not_mem] using h
    rfl
  apply le_antisymm _ (csInf_le_csInf ht (hs.image _) (image_subset _ hst))
  refine le_csInf ((hs.mono hst).image f) ?_
  simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a ha
  obtain ⟨x, hxs, hxa⟩ := h a ha
  exact csInf_le_of_le (ht.mono (image_subset _ hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)

Infimum Equality for Monotone Functions on Subsets with Lower Bounds

Informal description

Let $\alpha$ be a preorder and $\beta$ a conditionally complete lattice. Let $f : \alpha \to \beta$ be a function that is monotone on a subset $t \subseteq \alpha$, and let $s \subseteq t$ be a subset such that: 1. The image $f(t)$ is bounded below in $\beta$, 2. For every $y \in t$, there exists $x \in s$ with $x \leq y$. Then the infimum of $f(s)$ equals the infimum of $f(t)$, i.e., $\inf f(s) = \inf f(t)$.

MonotoneOn.csSup_eq_of_subset_of_forall_exists_le theorem

 [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α} (ht : BddAbove (f '' t)) (hf : MonotoneOn f t)
  (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) : sSup (f '' s) = sSup (f '' t)

Full source

lemma MonotoneOn.csSup_eq_of_subset_of_forall_exists_le
    [Preorder α] [ConditionallyCompleteLattice β] {f : α → β}
    {s t : Set α} (ht : BddAbove (f '' t)) (hf : MonotoneOn f t)
    (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
    sSup (f '' s) = sSup (f '' t) :=
  MonotoneOn.csInf_eq_of_subset_of_forall_exists_le (α := αᵒᵈ) (β := βᵒᵈ) ht hf.dual hst h

Supremum Equality for Monotone Functions on Subsets with Upper Bounds

Informal description

Let $\alpha$ be a preorder and $\beta$ a conditionally complete lattice. Let $f : \alpha \to \beta$ be a function that is monotone on a subset $t \subseteq \alpha$, and let $s \subseteq t$ be a subset such that: 1. The image $f(t)$ is bounded above in $\beta$, 2. For every $y \in t$, there exists $x \in s$ with $y \leq x$. Then the supremum of $f(s)$ equals the supremum of $f(t)$, i.e., $\sup f(s) = \sup f(t)$.

csSup_image2_eq_csSup_csSup theorem

 (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b)) (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty)
  (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (image2 l s t) = l (sSup s) (sSup t)

Full source

theorem csSup_image2_eq_csSup_csSup (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty) (hs₁ : BddAbove s)
    (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (image2 l s t) = l (sSup s) (sSup t) := by
  refine eq_of_forall_ge_iff fun c => ?_
  rw [csSup_le_iff (hs₁.image2 (fun _ => (h₁ _).monotone_l) (fun _ => (h₂ _).monotone_l) ht₁)
      (hs₀.image2 ht₀),
    forall_mem_image2, forall₂_swap, (h₂ _).le_iff_le, csSup_le_iff ht₁ ht₀]
  simp_rw [← (h₂ _).le_iff_le, (h₁ _).le_iff_le, csSup_le_iff hs₁ hs₀]

Supremum of Image under Binary Function with Galois Connections: $\sup l(s, t) = l(\sup s, \sup t)$

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $\gamma$ be a conditionally complete lattice. Let $l : \alpha \to \beta \to \gamma$ be a function such that for every $b \in \beta$, the function $\lambda a, l(a, b)$ has a Galois connection with $u_1(b) : \gamma \to \alpha$, and for every $a \in \alpha$, the function $\lambda b, l(a, b)$ has a Galois connection with $u_2(a) : \gamma \to \beta$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets that are bounded above. Then the supremum of the image of $s \times t$ under $l$ is equal to $l$ applied to the suprema of $s$ and $t$, i.e., \[ \sup \{ l(a, b) \mid a \in s, b \in t \} = l(\sup s, \sup t). \]

csSup_image2_eq_csSup_csInf theorem

 (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b)) (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) :
  s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sSup s) (sInf t)

Full source

theorem csSup_image2_eq_csSup_csInf (h₁ : ∀ b, GaloisConnection (swap l b) (u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDualtoDual ∘ u₂ a)) :
    s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sSup s) (sInf t) :=
  csSup_image2_eq_csSup_csSup (β := βᵒᵈ) h₁ h₂

Supremum of Image under Binary Function with Mixed Galois Connections: $\sup l(s, t) = l(\sup s, \inf t)$

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $\gamma$ be a conditionally complete lattice. Let $l : \alpha \to \beta \to \gamma$ be a function such that: 1. For every $b \in \beta$, the function $\lambda a, l(a, b)$ has a Galois connection with $u_1(b) : \gamma \to \alpha$. 2. For every $a \in \alpha$, the function $\lambda b, l(a, b) \circ \text{ofDual}$ has a Galois connection with $\text{toDual} \circ u_2(a) : \gamma \to \beta^\text{op}$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets such that $s$ is bounded above and $t$ is bounded below. Then the supremum of the image of $s \times t$ under $l$ is equal to $l$ applied to the supremum of $s$ and the infimum of $t$, i.e., \[ \sup \{ l(a, b) \mid a \in s, b \in t \} = l(\sup s, \inf t). \]

csSup_image2_eq_csInf_csSup theorem

 (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b)) (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) :
  s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (image2 l s t) = l (sInf s) (sSup t)

Full source

theorem csSup_image2_eq_csInf_csSup (h₁ : ∀ b, GaloisConnection (swapswap l b ∘ ofDual) (toDualtoDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a) (u₂ a)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (image2 l s t) = l (sInf s) (sSup t) :=
  csSup_image2_eq_csSup_csSup (α := αᵒᵈ) h₁ h₂

Supremum of Image under Binary Function with Mixed Galois Connections: $\sup l(s, t) = l(\inf s, \sup t)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders with $\gamma$ a conditionally complete lattice. Let $l : \alpha \to \beta \to \gamma$ be a function such that: 1. For each $b \in \beta$, the function $\lambda a, l(a, b)$ has a Galois connection with $u_1(b) : \gamma \to \alpha^\text{op}$ (where $\alpha^\text{op}$ is the order dual of $\alpha$). 2. For each $a \in \alpha$, the function $\lambda b, l(a, b)$ has a Galois connection with $u_2(a) : \gamma \to \beta$. Let $s \subseteq \alpha$ be nonempty and bounded below, and let $t \subseteq \beta$ be nonempty and bounded above. Then the supremum of the image of $s \times t$ under $l$ satisfies: \[ \sup \{ l(a, b) \mid a \in s, b \in t \} = l(\inf s, \sup t). \]

csSup_image2_eq_csInf_csInf theorem

 (h₁ : ∀ b, GaloisConnection (swap l b ∘ ofDual) (toDual ∘ u₁ b))
  (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDual ∘ u₂ a)) :
  s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sInf s) (sInf t)

Full source

theorem csSup_image2_eq_csInf_csInf (h₁ : ∀ b, GaloisConnection (swapswap l b ∘ ofDual) (toDualtoDual ∘ u₁ b))
    (h₂ : ∀ a, GaloisConnection (l a ∘ ofDual) (toDualtoDual ∘ u₂ a)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (image2 l s t) = l (sInf s) (sInf t) :=
  csSup_image2_eq_csSup_csSup (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂

Supremum of Image under Binary Function with Dual Galois Connections: $\sup l(s, t) = l(\inf s, \inf t)$

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $\gamma$ be a conditionally complete lattice. Let $l : \alpha \to \beta \to \gamma$ be a function such that for every $b \in \beta$, the function $\lambda a, l(a, b)$ has a Galois connection with $u_1(b) : \gamma \to \alpha^\text{op}$, and for every $a \in \alpha$, the function $\lambda b, l(a, b)$ has a Galois connection with $u_2(a) : \gamma \to \beta^\text{op}$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets that are bounded below. Then the supremum of the image of $s \times t$ under $l$ is equal to $l$ applied to the infima of $s$ and $t$, i.e., \[ \sup \{ l(a, b) \mid a \in s, b \in t \} = l(\inf s, \inf t). \]

csInf_image2_eq_csInf_csInf theorem

 (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b)) (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) :
  s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sInf s) (sInf t)

Full source

theorem csInf_image2_eq_csInf_csInf (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sInf s) (sInf t) :=
  csSup_image2_eq_csSup_csSup (α := αᵒᵈ) (β := βᵒᵈ) (γ := γᵒᵈ) (u₁ := l₁) (u₂ := l₂)
    (fun _ => (h₁ _).dual) fun _ => (h₂ _).dual

Infimum of Image under Binary Function with Galois Connections: $\inf u(s, t) = u(\inf s, \inf t)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders with $\gamma$ a conditionally complete lattice. Let $u : \alpha \to \beta \to \gamma$ be a function such that: 1. For each $b \in \beta$, the function $l_1(b) : \gamma \to \alpha$ has a Galois connection with $\lambda a, u(a, b)$. 2. For each $a \in \alpha$, the function $l_2(a) : \gamma \to \beta$ has a Galois connection with $\lambda b, u(a, b)$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets that are bounded below. Then the infimum of the image of $s \times t$ under $u$ satisfies: \[ \inf \{ u(a, b) \mid a \in s, b \in t \} = u(\inf s, \inf t). \]

csInf_image2_eq_csInf_csSup theorem

 (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b)) (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) :
  s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sInf s) (sSup t)

Full source

theorem csInf_image2_eq_csInf_csSup (h₁ : ∀ b, GaloisConnection (l₁ b) (swap u b))
    (h₂ : ∀ a, GaloisConnection (toDualtoDual ∘ l₂ a) (u a ∘ ofDual)) :
    s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sInf s) (sSup t) :=
  csInf_image2_eq_csInf_csInf (β := βᵒᵈ) h₁ h₂

Infimum of Image under Binary Function with Mixed Galois Connections: $\inf u(s, t) = u(\inf s, \sup t)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders with $\gamma$ a conditionally complete lattice. Let $u : \alpha \to \beta \to \gamma$ be a function such that: 1. For each $b \in \beta$, the function $l_1(b) : \gamma \to \alpha$ has a Galois connection with $\lambda a, u(a, b)$. 2. For each $a \in \alpha$, the function $l_2(a) : \gamma \to \beta^\text{op}$ has a Galois connection with $\lambda b, u(a, b)$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets with $s$ bounded below and $t$ bounded above. Then the infimum of the image of $s \times t$ under $u$ satisfies: \[ \inf \{ u(a, b) \mid a \in s, b \in t \} = u(\inf s, \sup t). \]

csInf_image2_eq_csSup_csInf theorem

 (h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual)) (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) :
  s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sSup s) (sInf t)

Full source

theorem csInf_image2_eq_csSup_csInf (h₁ : ∀ b, GaloisConnection (toDualtoDual ∘ l₁ b) (swapswap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (l₂ a) (u a)) :
    s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (image2 u s t) = u (sSup s) (sInf t) :=
  csInf_image2_eq_csInf_csInf (α := αᵒᵈ) h₁ h₂

Infimum of Image under Binary Function with Mixed Galois Connections: $\inf u(s, t) = u(\sup s, \inf t)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders with $\gamma$ a conditionally complete lattice. Let $u : \alpha \to \beta \to \gamma$ be a function such that: 1. For each $b \in \beta$, the function $l_1(b) : \gamma \to \alpha^\text{op}$ has a Galois connection with $\lambda a, u(a, b)$ (where $\alpha^\text{op}$ is the order dual of $\alpha$). 2. For each $a \in \alpha$, the function $l_2(a) : \gamma \to \beta$ has a Galois connection with $\lambda b, u(a, b)$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets with $s$ bounded above and $t$ bounded below. Then the infimum of the image of $s \times t$ under $u$ satisfies: \[ \inf \{ u(a, b) \mid a \in s, b \in t \} = u(\sup s, \inf t). \]

csInf_image2_eq_csSup_csSup theorem

 (h₁ : ∀ b, GaloisConnection (toDual ∘ l₁ b) (swap u b ∘ ofDual))
  (h₂ : ∀ a, GaloisConnection (toDual ∘ l₂ a) (u a ∘ ofDual)) :
  s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sSup s) (sSup t)

Full source

theorem csInf_image2_eq_csSup_csSup (h₁ : ∀ b, GaloisConnection (toDualtoDual ∘ l₁ b) (swapswap u b ∘ ofDual))
    (h₂ : ∀ a, GaloisConnection (toDualtoDual ∘ l₂ a) (u a ∘ ofDual)) :
    s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (image2 u s t) = u (sSup s) (sSup t) :=
  csInf_image2_eq_csInf_csInf (α := αᵒᵈ) (β := βᵒᵈ) h₁ h₂

Infimum of Image under Binary Function with Dual Galois Connections: $\inf u(s, t) = u(\sup s, \sup t)$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders with $\gamma$ a conditionally complete lattice. Let $u : \alpha \to \beta \to \gamma$ be a function such that: 1. For each $b \in \beta$, the function $l_1(b) : \gamma \to \alpha^\text{op}$ has a Galois connection with $\lambda a, u(a, b)$ (where $\alpha^\text{op}$ is the order dual of $\alpha$). 2. For each $a \in \alpha$, the function $l_2(a) : \gamma \to \beta^\text{op}$ has a Galois connection with $\lambda b, u(a, b)$. Let $s \subseteq \alpha$ and $t \subseteq \beta$ be nonempty subsets that are bounded above. Then the infimum of the image of $s \times t$ under $u$ satisfies: \[ \inf \{ u(a, b) \mid a \in s, b \in t \} = u(\sup s, \sup t). \]

WithTop.conditionallyCompleteLattice instance

{α : Type*} [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithTop α)

Full source

/-- Adding a top element to a conditionally complete lattice
gives a conditionally complete lattice -/
noncomputable instance WithTop.conditionallyCompleteLattice {α : Type*}
    [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithTop α) :=
  { lattice, instSupSet, instInfSet with
    le_csSup := fun _ a _ haS => (WithTop.isLUB_sSup' ⟨a, haS⟩).1 haS
    csSup_le := fun _ _ hS haS => (WithTop.isLUB_sSup' hS).2 haS
    csInf_le := fun _ _ hS haS => (WithTop.isGLB_sInf' hS).1 haS
    le_csInf := fun _ a _ haS => (WithTop.isGLB_sInf' ⟨a, haS⟩).2 haS }

Conditionally Complete Lattice Structure on $\text{WithTop}\ \alpha$

Informal description

For any conditionally complete lattice $\alpha$, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) is also a conditionally complete lattice. The supremum and infimum operations on $\text{WithTop}\ \alpha$ extend those of $\alpha$ in a natural way, handling the top element appropriately.

WithBot.conditionallyCompleteLattice instance

{α : Type*} [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithBot α)

Full source

/-- Adding a bottom element to a conditionally complete lattice
gives a conditionally complete lattice -/
noncomputable instance WithBot.conditionallyCompleteLattice {α : Type*}
    [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithBot α) :=
  { WithBot.lattice with
    le_csSup := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csInf_le
    csSup_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csInf
    csInf_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csSup
    le_csInf := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csSup_le }

Conditionally Complete Lattice Structure on $\alpha$ with Bottom Element

Informal description

For any conditionally complete lattice $\alpha$, the type $\alpha$ with a bottom element $\bot$ adjoined (denoted $\text{WithBot}\ \alpha$) is also a conditionally complete lattice. The supremum and infimum operations on $\text{WithBot}\ \alpha$ extend those of $\alpha$, with $\sup \emptyset = \bot$ and $\inf \emptyset = \top$ (the top element of $\alpha$ if it exists, otherwise a new top element).

WithTop.WithBot.completeLattice instance

{α : Type*} [ConditionallyCompleteLattice α] : CompleteLattice (WithTop (WithBot α))

Full source

noncomputable instance WithTop.WithBot.completeLattice {α : Type*}
    [ConditionallyCompleteLattice α] : CompleteLattice (WithTop (WithBot α)) :=
  { instInfSet, instSupSet, boundedOrder, lattice with
    le_sSup := fun _ a haS => (WithTop.isLUB_sSup' ⟨a, haS⟩).1 haS
    sSup_le := fun S a ha => by
      rcases S.eq_empty_or_nonempty with h | h
      · show ite _ _ _ ≤ a
        simp [h]
      · exact (WithTop.isLUB_sSup' h).2 ha
    sInf_le := fun S a haS =>
      show ite _ _ _ ≤ a by
        simp only [OrderBot.bddBelow, not_true_eq_false, or_false]
        split_ifs with h₁
        · cases a
          · exact le_rfl
          cases h₁ haS
        · cases a
          · exact le_top
          · apply WithTop.coe_le_coe.2
            refine csInf_le ?_ haS
            use ⊥
            intro b _
            exact bot_le
    le_sInf := fun _ a haS => (WithTop.isGLB_sInf' ⟨a, haS⟩).2 haS }

Complete Lattice Structure on $\text{WithTop}(\text{WithBot}\ \alpha)$

Informal description

For any conditionally complete lattice $\alpha$, the type $\text{WithTop}(\text{WithBot}\ \alpha)$ (obtained by first adjoining a bottom element $\bot$ to $\alpha$ and then adjoining a top element $\top$ to the result) forms a complete lattice. In this structure, all subsets have suprema and infima, including the empty set and unbounded sets, which are handled by the adjoined top and bottom elements.

WithTop.WithBot.completeLinearOrder instance

{α : Type*} [ConditionallyCompleteLinearOrder α] : CompleteLinearOrder (WithTop (WithBot α))

Full source

noncomputable instance WithTop.WithBot.completeLinearOrder {α : Type*}
    [ConditionallyCompleteLinearOrder α] : CompleteLinearOrder (WithTop (WithBot α)) :=
  -- FIXME: Spread notation doesn't work
  { completeLattice, linearOrder, LinearOrder.toBiheytingAlgebra with }

Complete Linear Order Structure on $\text{WithTop}(\text{WithBot}\ \alpha)$

Informal description

For any conditionally complete linear order $\alpha$, the type $\text{WithTop}(\text{WithBot}\ \alpha)$ (obtained by first adjoining a bottom element $\bot$ to $\alpha$ and then adjoining a top element $\top$ to the result) forms a complete linear order. In this structure, all subsets have suprema and infima, including the empty set and unbounded sets, which are handled by the adjoined top and bottom elements.

WithBot.WithTop.completeLattice instance

{α : Type*} [ConditionallyCompleteLattice α] : CompleteLattice (WithBot (WithTop α))

Full source

noncomputable instance WithBot.WithTop.completeLattice {α : Type*}
    [ConditionallyCompleteLattice α] : CompleteLattice (WithBot (WithTop α)) :=
  { instInfSet, instSupSet, instBoundedOrder, lattice with
    le_sSup := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).sInf_le
    sSup_le := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).le_sInf
    sInf_le := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).le_sSup
    le_sInf := (WithTop.WithBot.completeLattice (α := αᵒᵈ)).sSup_le }

Complete Lattice Structure on $\text{WithBot}(\text{WithTop}\ \alpha)$

Informal description

For any conditionally complete lattice $\alpha$, the type $\text{WithBot}(\text{WithTop}\ \alpha)$ (obtained by first adjoining a top element $\top$ to $\alpha$ and then adjoining a bottom element $\bot$ to the result) forms a complete lattice. In this structure, all subsets have suprema and infima, including the empty set and unbounded sets, which are handled by the adjoined top and bottom elements.

WithBot.WithTop.completeLinearOrder instance

{α : Type*} [ConditionallyCompleteLinearOrder α] : CompleteLinearOrder (WithBot (WithTop α))

Full source

noncomputable instance WithBot.WithTop.completeLinearOrder {α : Type*}
    [ConditionallyCompleteLinearOrder α] : CompleteLinearOrder (WithBot (WithTop α)) :=
  { completeLattice, linearOrder, LinearOrder.toBiheytingAlgebra with }

Complete Linear Order Structure on $\text{WithBot}(\text{WithTop}\ \alpha)$

Informal description

For any conditionally complete linear order $\alpha$, the type $\text{WithBot}(\text{WithTop}\ \alpha)$ (obtained by first adjoining a top element $\top$ to $\alpha$ and then adjoining a bottom element $\bot$ to the result) forms a complete linear order. In this structure, all subsets have suprema and infima, including the empty set and unbounded sets, which are handled by the adjoined top and bottom elements.