# Theory of conditionally complete lattices #

A conditionally complete lattice is a lattice in which every non-empty bounded subset `s` has a least upper bound and a greatest lower bound, denoted below by `sSup s` and `sInf s`. Typical examples are `ℝ`, `ℕ`, and `ℤ` with their usual orders.

The theory is very comparable to the theory of complete lattices, except that suitable boundedness and nonemptiness assumptions have to be added to most statements. We express these using the `BddAbove` and `BddBelow` predicates, which we use to prove most useful properties of `sSup` and `sInf` in conditionally complete lattices.

To differentiate the statements between complete lattices and conditionally complete lattices, we prefix `sInf` and `sSup` in the statements by `c`, giving `csInf` and `csSup`. For instance, `sInf_le` is a statement in complete lattices ensuring `sInf s ≤ x`, while `csInf_le` is the same statement in conditionally complete lattices with an additional assumption that `s` is bounded below.

Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`

source
noncomputable instance WithTop.instSupSet {α : Type u_1} [Preorder α] [SupSet α] :
SupSet (WithTop α)
Equations

- WithTop.instSupSet = { sSup := fun (S : Set (WithTop α)) => if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) => ↑a) ⁻¹' S) then ↑(sSup ((fun (a : α) => ↑a) ⁻¹' S)) else ⊤ }

source
noncomputable instance WithTop.instInfSet {α : Type u_1} [Preorder α] [InfSet α] :
InfSet (WithTop α)
Equations

- WithTop.instInfSet = { sInf := fun (S : Set (WithTop α)) => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) => ↑a) ⁻¹' S)) }

source
noncomputable instance WithBot.instSupSet {α : Type u_1} [Preorder α] [SupSet α] :
SupSet (WithBot α)
Equations

- WithBot.instSupSet = { sSup := sInf }

source
noncomputable instance WithBot.instInfSet {α : Type u_1} [Preorder α] [InfSet α] :
InfSet (WithBot α)
Equations

- WithBot.instInfSet = { sInf := sSup }

source
theorem WithTop.sSup_eq {α : Type u_1} [Preorder α] [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) (hs' : BddAbove (some ⁻¹' s)) :
sSup s = ↑(sSup (some ⁻¹' s))
source
theorem WithTop.sInf_eq {α : Type u_1} [Preorder α] [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
sInf s = ↑(sInf (some ⁻¹' s))
source
theorem WithBot.sInf_eq {α : Type u_1} [Preorder α] [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) (hs' : BddBelow (some ⁻¹' s)) :
sInf s = ↑(sInf (some ⁻¹' s))
source
theorem WithBot.sSup_eq {α : Type u_1} [Preorder α] [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
sSup s = ↑(sSup (some ⁻¹' s))
source
@[simp]
theorem WithTop.sInf_empty {α : Type u_1} [Preorder α] [InfSet α] :
sInf ∅ = ⊤
source
theorem WithTop.coe_sInf' {α : Type u_1} [Preorder α] [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
↑(sInf s) = sInf ((fun (a : α) => ↑a) '' s)
source
theorem WithTop.coe_sSup' {α : Type u_1} [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove s) :
↑(sSup s) = sSup ((fun (a : α) => ↑a) '' s)
source
@[simp]
theorem WithBot.sSup_empty {α : Type u_1} [Preorder α] [SupSet α] :
sSup ∅ = ⊥
source
theorem WithBot.coe_sSup' {α : Type u_1} [Preorder α] [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
↑(sSup s) = sSup ((fun (a : α) => ↑a) '' s)
source
theorem WithBot.coe_sInf' {α : Type u_1} [Preorder α] [InfSet α] {s : Set α} (hs : BddBelow s) :
↑(sInf s) = sInf ((fun (a : α) => ↑a) '' s)
source
instance ConditionallyCompleteLinearOrder.toLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrder α] :
LinearOrder α
Equations

- One or more equations did not get rendered due to their size.

source
@[instance 100]
instance CompleteLattice.toConditionallyCompleteLattice {α : Type u_1} [CompleteLattice α] :
ConditionallyCompleteLattice α

A complete lattice is a conditionally complete lattice, as there are no restrictions on the properties of sInf and sSup in a complete lattice.

Equations

- One or more equations did not get rendered due to their size.

source
@[instance 100]
instance CompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α : Type u_5} [h : CompleteLinearOrder α] :
ConditionallyCompleteLinearOrderBot α
Equations

- One or more equations did not get rendered due to their size.

source
instance OrderDual.instConditionallyCompleteLattice (α : Type u_5) [ConditionallyCompleteLattice α] :
ConditionallyCompleteLattice α ᵒᵈ
Equations

- One or more equations did not get rendered due to their size.

source
instance OrderDual.instConditionallyCompleteLinearOrder (α : Type u_5) [ConditionallyCompleteLinearOrder α] :
ConditionallyCompleteLinearOrder α ᵒᵈ
Equations

- One or more equations did not get rendered due to their size.

source
theorem le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddAbove s) (h₂ : a ∈ s) :
a ≤ sSup s
source
theorem csSup_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) :
sSup s ≤ a
source
theorem csInf_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddBelow s) (h₂ : a ∈ s) :
sInf s ≤ a
source
theorem le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) :
a ≤ sInf s
source
theorem le_csSup_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) :
a ≤ sSup s
source
theorem csInf_le_of_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} (hs : BddBelow s) (hb : b ∈ s) (h : b ≤ a) :
sInf s ≤ a
source
theorem csSup_le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) :
sSup s ≤ sSup t
source
theorem csInf_le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) :
sInf t ≤ sInf s
source
theorem le_csSup_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddAbove s) (hs : s.Nonempty) :
a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
source
theorem csInf_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h : BddBelow s) (hs : s.Nonempty) :
sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a
source
theorem isLUB_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : s.Nonempty) (H : BddAbove s) :
IsLUB s (sSup s)
source
theorem isGLB_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : s.Nonempty) (H : BddBelow s) :
IsGLB s (sInf s)
source
theorem IsLUB.csSup_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLUB s a) (ne : s.Nonempty) :
sSup s = a
source
theorem IsGreatest.csSup_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
sSup s = a

A greatest element of a set is the supremum of this set.

source
theorem IsGreatest.csSup_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) :
sSup s ∈ s
source
theorem IsGLB.csInf_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGLB s a) (ne : s.Nonempty) :
sInf s = a
source
theorem IsLeast.csInf_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
sInf s = a

A least element of a set is the infimum of this set.

source
theorem IsLeast.csInf_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) :
sInf s ∈ s
source
theorem subset_Icc_csInf_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) :
s ⊆ Set.Icc (sInf s) (sSup s)
source
theorem csSup_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddAbove s) (hs : s.Nonempty) :
sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a
source
theorem le_csInf_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddBelow s) (hs : s.Nonempty) :
a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
source
theorem csSup_lowerBounds_eq_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) :
sSup (lowerBounds s) = sInf s
source
theorem csInf_upperBounds_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) :
sInf (upperBounds s) = sSup s
source
theorem csSup_lowerBounds_range {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [Nonempty β] {f : β → α} (hf : BddBelow (Set.range f)) :
sSup (lowerBounds (Set.range f)) = ⨅ (i : β), f i
source
theorem csInf_upperBounds_range {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [Nonempty β] {f : β → α} (hf : BddAbove (Set.range f)) :
sInf (upperBounds (Set.range f)) = ⨆ (i : β), f i
source
theorem notMem_of_lt_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) :
x ∉ s
source
@[deprecated notMem_of_lt_csInf (since := "2025-05-23")]
theorem not_mem_of_lt_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) :
x ∉ s

Alias of `notMem_of_lt_csInf`.

source
theorem notMem_of_csSup_lt {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) :
x ∉ s
source
@[deprecated notMem_of_csSup_lt (since := "2025-05-23")]
theorem not_mem_of_csSup_lt {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) :
x ∉ s

Alias of `notMem_of_csSup_lt`.

source
theorem csSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} (hs : s.Nonempty) (H : ∀ a ∈ s, a ≤ b) (H' : ∀ w < b, ∃ a ∈ s, w < a) :
sSup s = b

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.

source
theorem csInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} :
s.Nonempty → (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b

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.

source
theorem lt_csSup_of_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} (hs : BddAbove s) (ha : a ∈ s) (h : b < a) :
b < sSup s

`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.

source
theorem csInf_lt_of_lt {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a b : α} :
BddBelow s → a ∈ s → a < b → sInf s < b

`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.

source
theorem exists_between_of_forall_le {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (sne : s.Nonempty) (tne : t.Nonempty) (hst : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) :
(upperBounds s ∩ lowerBounds t).Nonempty

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.

source
@[simp]
theorem csSup_singleton {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) :
sSup {a} = a

The supremum of a singleton is the element of the singleton

source
@[simp]
theorem csInf_singleton {α : Type u_1} [ConditionallyCompleteLattice α] (a : α) :
sInf {a} = a

The infimum of a singleton is the element of the singleton

source
theorem csSup_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a b : α) :
sSup {a, b} = a ⊔ b
source
theorem csInf_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a b : α) :
sInf {a, b} = a ⊓ b
source
theorem csInf_le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) (ne : s.Nonempty) :
sInf s ≤ sSup s

If a set is bounded below and above, and nonempty, its infimum is less than or equal to its supremum.

source
theorem csSup_union {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (hs : BddAbove s) (sne : s.Nonempty) (ht : BddAbove t) (tne : t.Nonempty) :
sSup (s ∪ t) = sSup s ⊔ sSup t

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.

source
theorem csInf_union {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (hs : BddBelow s) (sne : s.Nonempty) (ht : BddBelow t) (tne : t.Nonempty) :
sInf (s ∪ t) = sInf s ⊓ sInf t

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.

source
theorem csSup_inter_le {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (hs : BddAbove s) (ht : BddAbove t) (hst : (s ∩ t).Nonempty) :
sSup (s ∩ t) ≤ sSup s ⊓ sSup t

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.

source
theorem le_csInf_inter {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} :
BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)

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.

source
@[simp]
theorem csSup_insert {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddAbove s) (sne : s.Nonempty) :
sSup (insert a s) = a ⊔ sSup s

The supremum of `insert a s` is the maximum of `a` and the supremum of `s`, if `s` is nonempty and bounded above.

source
@[simp]
theorem csInf_insert {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hs : BddBelow s) (sne : s.Nonempty) :
sInf (insert a s) = a ⊓ sInf s

The infimum of `insert a s` is the minimum of `a` and the infimum of `s`, if `s` is nonempty and bounded below.

source
@[simp]
theorem csInf_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) :
sInf (Set.Icc a b) = a
source
@[simp]
theorem csInf_Ici {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} :
sInf (Set.Ici a) = a
source
@[simp]
theorem csInf_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a < b) :
sInf (Set.Ico a b) = a
source
@[simp]
theorem csInf_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) :
sInf (Set.Ioc a b) = a
source
@[simp]
theorem csInf_Ioi {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMaxOrder α] [DenselyOrdered α] :
sInf (Set.Ioi a) = a
source
@[simp]
theorem csInf_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) :
sInf (Set.Ioo a b) = a
source
@[simp]
theorem csSup_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) :
sSup (Set.Icc a b) = b
source
@[simp]
theorem csSup_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) :
sSup (Set.Ico a b) = b
source
@[simp]
theorem csSup_Iic {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} :
sSup (Set.Iic a) = a
source
@[simp]
theorem csSup_Iio {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMinOrder α] [DenselyOrdered α] :
sSup (Set.Iio a) = a
source
@[simp]
theorem csSup_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a < b) :
sSup (Set.Ioc a b) = b
source
@[simp]
theorem csSup_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) :
sSup (Set.Ioo a b) = b
source
theorem csSup_eq_of_is_forall_le_of_forall_le_imp_ge {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {b : α} (hs : s.Nonempty) (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ (ub : α), (∀ a ∈ s, a ≤ ub) → b ≤ ub) :
sSup s = b

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'`.

source
theorem sup_eq_top_of_top_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} [OrderTop α] (h : ⊤ ∈ s) :
sSup s = ⊤
source
theorem inf_eq_bot_of_bot_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} [OrderBot α] (h : ⊥ ∈ s) :
sInf s = ⊥
source
instance Pi.conditionallyCompleteLattice {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → ConditionallyCompleteLattice (α i)] :
ConditionallyCompleteLattice ((i : ι) → α i)
Equations

- Pi.conditionallyCompleteLattice = { toLattice := Pi.instLattice, toSupSet := Pi.supSet, toInfSet := Pi.infSet, le_csSup := ⋯, csSup_le := ⋯, csInf_le := ⋯, le_csInf := ⋯ }

source
theorem exists_lt_of_lt_csSup {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : s.Nonempty) (hb : b < sSup s) :
∃ a ∈ s, b < a

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.

source
theorem exists_lt_of_csInf_lt {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} (hs : s.Nonempty) (hb : sInf s < b) :
∃ a ∈ s, a < b

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.

source
theorem lt_csSup_iff {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {a : α} (hb : BddAbove s) (hs : s.Nonempty) :
a < sSup s ↔ ∃ b ∈ s, a < b
source
theorem csInf_lt_iff {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {a : α} (hb : BddBelow s) (hs : s.Nonempty) :
sInf s < a ↔ ∃ b ∈ s, b < a
source
@[simp]
theorem csSup_of_not_bddAbove {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddAbove s) :
sSup s = sSup ∅
source
@[simp]
theorem ciSup_of_not_bddAbove {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddAbove (Set.range f)) :
⨆ (i : ι), f i = sSup ∅
source
theorem csSup_eq_univ_of_not_bddAbove {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddAbove s) :
sSup s = sSup Set.univ
source
theorem ciSup_eq_univ_of_not_bddAbove {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddAbove (Set.range f)) :
⨆ (i : ι), f i = sSup Set.univ
source
@[simp]
theorem csInf_of_not_bddBelow {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) :
sInf s = sInf ∅
source
@[simp]
theorem ciInf_of_not_bddBelow {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) :
⨅ (i : ι), f i = sInf ∅
source
theorem csInf_eq_univ_of_not_bddBelow {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) :
sInf s = sInf Set.univ
source
theorem ciInf_eq_univ_of_not_bddBelow {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] {f : ι → α} (hf : ¬BddBelow (Set.range f)) :
⨅ (i : ι), f i = sInf Set.univ
source
theorem csSup_eq_csSup_of_forall_exists_le {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
sSup s = sSup t

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.

source
theorem csInf_eq_csInf_of_forall_exists_le {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s t : Set α} (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
sInf s = sInf t

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.

source
theorem sSup_iUnion_Iic {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) :
sSup (⋃ (i : ι), Set.Iic (f i)) = ⨆ (i : ι), f i
source
theorem sInf_iUnion_Ici {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) :
sInf (⋃ (i : ι), Set.Ici (f i)) = ⨅ (i : ι), f i
source
theorem csInf_eq_bot_of_bot_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) :
sInf s = ⊥
source
theorem csSup_eq_top_of_top_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderTop α] {s : Set α} (hs : ⊤ ∈ s) :
sSup s = ⊤
source
theorem sInf_eq_argmin_on {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) :
sInf s = Function.argminOn id s hs
source
theorem isLeast_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) :
IsLeast s (sInf s)
source
theorem le_csInf_iff' {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedLT α] (hs : s.Nonempty) :
b ≤ sInf s ↔ b ∈ lowerBounds s
source
theorem csInf_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) :
sInf s ∈ s
source
theorem MonotoneOn.map_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5} [ConditionallyCompleteLattice β] {f : α → β} (hf : MonotoneOn f s) (hs : s.Nonempty) :
f (sInf s) = sInf (f '' s)
source
theorem Monotone.map_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5} [ConditionallyCompleteLattice β] {f : α → β} (hf : Monotone f) (hs : s.Nonempty) :
f (sInf s) = sInf (f '' s)

### Lemmas about a conditionally complete linear order with bottom element #

In this case we have `Sup ∅ = ⊥`, so we can drop some `Nonempty`/`Set.Nonempty` assumptions.

source
@[simp]
theorem csInf_univ {α : Type u_1} [ConditionallyCompleteLattice α] [OrderBot α] :
sInf Set.univ = ⊥
source
@[simp]
theorem csSup_empty {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] :
sSup ∅ = ⊥
source
theorem isLUB_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) :
IsLUB s (sSup s)
source
theorem csSup_le_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) {a : α} :
sSup s ≤ a ↔ ∀ x ∈ s, x ≤ a

In conditionally complete orders with a bottom element, the nonempty condition can be omitted from `csSup_le_iff`.

source
theorem csSup_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ upperBounds s) :
sSup s ≤ a
source
theorem lt_csSup_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (hb : BddAbove s) :
a < sSup s ↔ ∃ b ∈ s, a < b

In conditionally complete orders with a bottom element, the nonempty condition can be omitted from `lt_csSup_iff`.

source
theorem le_csSup_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : BddAbove s) :
a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b
source
theorem le_csInf_iff'' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : s.Nonempty) :
a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
source
theorem csInf_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ s) :
sInf s ≤ a
source
theorem exists_lt_of_lt_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a < sSup s) :
∃ b ∈ s, a < b
source
theorem notMem_of_lt_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {x : α} {s : Set α} (h : x < sInf s) :
x ∉ s
source
@[deprecated notMem_of_lt_csInf' (since := "2025-05-23")]
theorem not_mem_of_lt_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {x : α} {s : Set α} (h : x < sInf s) :
x ∉ s

Alias of `notMem_of_lt_csInf'`.

source
theorem csInf_le_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) :
sInf s ≤ sInf t
source
theorem csSup_le_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) :
sSup s ≤ sSup t
source
theorem WithTop.isLUB_sSup' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : s.Nonempty) :
IsLUB s (sSup s)

The `sSup` of a non-empty set is its least upper bound for a conditionally complete lattice with a top.

source
theorem WithTop.isLUB_sSup {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) :
IsLUB s (sSup s)
source
theorem WithTop.isGLB_sInf' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithTop β)} (hs : BddBelow s) :
IsGLB s (sInf s)

The `sInf` of a bounded-below set is its greatest lower bound for a conditionally complete lattice with a top.

source
theorem WithTop.isGLB_sInf {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) :
IsGLB s (sInf s)
source
noncomputable instance WithTop.instCompleteLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] :
CompleteLinearOrder (WithTop α)
Equations

- One or more equations did not get rendered due to their size.

source
theorem WithTop.coe_sSup {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hb : BddAbove s) :
↑(sSup s) = ⨆ a ∈ s, ↑a

A version of `WithTop.coe_sSup'` with a more convenient but less general statement.

source
theorem WithTop.coe_sInf {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
↑(sInf s) = ⨅ a ∈ s, ↑a

A version of `WithTop.coe_sInf'` with a more convenient but less general statement.

A monotone function into a conditionally complete lattice preserves the ordering properties of `sSup` and `sInf`.

source
theorem Monotone.le_csSup_image {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddAbove s) :
f c ≤ sSup (f '' s)
source
theorem Monotone.csSup_image_le {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} (h_mono : Monotone f) {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ upperBounds s) :
sSup (f '' s) ≤ f B
source
theorem Monotone.csInf_image_le {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} (h_mono : Monotone f) {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) :
sInf (f '' s) ≤ f c
source
theorem Monotone.le_csInf_image {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} (h_mono : Monotone f) {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) :
f B ≤ sInf (f '' s)
source
theorem MonotoneOn.csInf_eq_of_subset_of_forall_exists_le {α : Type u_1} {β : Type u_2} [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)
source
theorem MonotoneOn.csSup_eq_of_subset_of_forall_exists_le {α : Type u_1} {β : Type u_2} [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)
source
theorem MonotoneOn.sInf_image_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : MonotoneOn f (Set.Icc a b)) :
sInf (f '' Set.Icc a b) = f a
source
theorem MonotoneOn.sSup_image_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : MonotoneOn f (Set.Icc a b)) :
sSup (f '' Set.Icc a b) = f b
source
theorem AntitoneOn.sInf_image_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : AntitoneOn f (Set.Icc a b)) :
sInf (f '' Set.Icc a b) = f b
source
theorem AntitoneOn.sSup_image_Icc {α : Type u_1} {β : Type u_2} [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b) (h' : AntitoneOn f (Set.Icc a b)) :
sSup (f '' Set.Icc a b) = f a

### Supremum/infimum of `Set.image2` #

A collection of lemmas showing what happens to the suprema/infima of `s` and `t` when mapped under a binary function whose partial evaluations are lower/upper adjoints of Galois connections.

source
theorem csSup_image2_eq_csSup_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.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 (Set.image2 l s t) = l (sSup s) (sSup t)
source
theorem csSup_image2_eq_csSup_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) :
s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sSup s) (sInf t)
source
theorem csSup_image2_eq_csInf_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) :
s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
source
theorem csSup_image2_eq_csInf_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) :
s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sInf s) (sInf t)
source
theorem csInf_image2_eq_csInf_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) :
s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sInf s) (sInf t)
source
theorem csInf_image2_eq_csInf_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) :
s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sInf s) (sSup t)
source
theorem csInf_image2_eq_csSup_csInf {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) :
s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
source
theorem csInf_image2_eq_csSup_csSup {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) :
s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sSup s) (sSup t)

### Complete lattice structure on `WithTop (WithBot α)` #

If `α` is a `ConditionallyCompleteLattice`, then we show that `WithTop α` and `WithBot α` also inherit the structure of conditionally complete lattices. Furthermore, we show that `WithTop (WithBot α)` and `WithBot (WithTop α)` naturally inherit the structure of a complete lattice. Note that for `α` a conditionally complete lattice, `sSup` and `sInf` both return junk values for sets which are empty or unbounded. The extension of `sSup` to `WithTop α` fixes the unboundedness problem and the extension to `WithBot α` fixes the problem with the empty set.

This result can be used to show that the extended reals `[-∞, ∞]` are a complete linear order.

source
noncomputable instance WithTop.conditionallyCompleteLattice {α : Type u_5} [ConditionallyCompleteLattice α] :
ConditionallyCompleteLattice (WithTop α)

Adding a top element to a conditionally complete lattice gives a conditionally complete lattice

Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance WithBot.conditionallyCompleteLattice {α : Type u_5} [ConditionallyCompleteLattice α] :
ConditionallyCompleteLattice (WithBot α)

Adding a bottom element to a conditionally complete lattice gives a conditionally complete lattice

Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance WithTop.WithBot.completeLattice {α : Type u_5} [ConditionallyCompleteLattice α] :
CompleteLattice (WithTop (WithBot α))
Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance WithTop.WithBot.completeLinearOrder {α : Type u_5} [ConditionallyCompleteLinearOrder α] :
CompleteLinearOrder (WithTop (WithBot α))
Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance WithBot.WithTop.completeLattice {α : Type u_5} [ConditionallyCompleteLattice α] :
CompleteLattice (WithBot (WithTop α))
Equations

- One or more equations did not get rendered due to their size.

source
noncomputable instance WithBot.WithTop.completeLinearOrder {α : Type u_5} [ConditionallyCompleteLinearOrder α] :
CompleteLinearOrder (WithBot (WithTop α))
Equations

- One or more equations did not get rendered due to their size.