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 α

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 ⊤ }

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)) }

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

Equations

• WithBot.instSupSet = { sSup := sInf }

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

Equations

• WithBot.instInfSet = { sInf := sSup }

theorem WithTop.sSup_eq {α : Type u_1} [Preorder α] [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s) (hs' : BddAbove (WithTop.some ⁻¹' s)) : sSup s = ↑(sSup (WithTop.some ⁻¹' s))

theorem WithTop.sInf_eq {α : Type u_1} [Preorder α] [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) : sInf s = ↑(sInf (WithTop.some ⁻¹' s))

theorem WithBot.sInf_eq {α : Type u_1} [Preorder α] [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) (hs' : BddBelow (WithBot.some ⁻¹' s)) : sInf s = ↑(sInf (WithBot.some ⁻¹' s))

theorem WithBot.sSup_eq {α : Type u_1} [Preorder α] [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) : sSup s = ↑(sSup (WithBot.some ⁻¹' s))

@[simp]

theorem WithTop.sInf_empty {α : Type u_1} [Preorder α] [InfSet α] : sInf ∅ = ⊤

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)

theorem WithTop.coe_sSup' {α : Type u_1} [Preorder α] [SupSet α] {s : Set α} (hs : BddAbove s) : ↑(sSup s) = sSup ((fun (a : α) => ↑a) '' s)

@[simp]

theorem WithBot.sSup_empty {α : Type u_1} [Preorder α] [SupSet α] : sSup ∅ = ⊥

@[deprecated WithBot.sSup_empty]

theorem WithBot.csSup_empty {α : Type u_1} [Preorder α] [SupSet α] : sSup ∅ = ⊥

Alias of WithBot.sSup_empty.

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)

theorem WithBot.coe_sInf' {α : Type u_1} [Preorder α] [InfSet α] {s : Set α} (hs : BddBelow s) : ↑(sInf s) = sInf ((fun (a : α) => ↑a) '' s)

instance ConditionallyCompleteLinearOrder.toLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrder α] : LinearOrder α

Equations

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

@[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

• CompleteLattice.toConditionallyCompleteLattice = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

@[instance 100]

instance CompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α : Type u_5} [h : CompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot α

Equations

• CompleteLinearOrder.toConditionallyCompleteLinearOrderBot = ConditionallyCompleteLinearOrderBot.mk ⋯

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

Equations

• OrderDual.instConditionallyCompleteLattice α = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• OrderDual.instConditionallyCompleteLinearOrder α = ConditionallyCompleteLinearOrder.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯

theorem le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s

theorem csSup_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) : sSup s ≤ a

theorem csInf_le {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : BddBelow s) (h₂ : a ∈ s) : sInf s ≤ a

theorem le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) : a ≤ sInf s

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

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

theorem csSup_le_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (ht : BddAbove t) (hs : s.Nonempty) (h : s ⊆ t) : sSup s ≤ sSup t

theorem csInf_le_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s t : Set α} (ht : BddBelow t) (hs : s.Nonempty) (h : s ⊆ t) : sInf t ≤ sInf s

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

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

theorem isLUB_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : s.Nonempty) (H : BddAbove s) : IsLUB s (sSup s)

theorem isGLB_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s)

theorem IsLUB.csSup_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a

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.

theorem IsGreatest.csSup_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGreatest s a) : sSup s ∈ s

theorem IsGLB.csInf_eq {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a

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.

theorem IsLeast.csInf_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (H : IsLeast s a) : sInf s ∈ s

theorem subset_Icc_csInf_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Set.Icc (sInf s) (sSup s)

theorem csSup_le_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddAbove s) (hs : s.Nonempty) : sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

theorem le_csInf_iff {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} {a : α} (hb : BddBelow s) (hs : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

theorem csSup_lowerBounds_eq_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) : sSup (lowerBounds s) = sInf s

theorem csInf_upperBounds_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s

@[deprecated csSup_lowerBounds_eq_csInf]

theorem csSup_lower_bounds_eq_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddBelow s) (hs : s.Nonempty) : sSup (lowerBounds s) = sInf s

Alias of csSup_lowerBounds_eq_csInf.

@[deprecated csInf_upperBounds_eq_csSup]

theorem csInf_upper_bounds_eq_csSup {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} (h : BddAbove s) (hs : s.Nonempty) : sInf (upperBounds s) = sSup s

Alias of csInf_upperBounds_eq_csSup.

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

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

theorem not_mem_of_lt_csInf {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : x < sInf s) (hs : BddBelow s) : x ∉ s

theorem not_mem_of_csSup_lt {α : Type u_1} [ConditionallyCompleteLattice α] {x : α} {s : Set α} (h : sSup s < x) (hs : BddAbove s) : x ∉ s

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.

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.

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.

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.

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.

@[simp]

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

The supremum of a singleton is the element of the singleton

@[simp]

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

The infimum of a singleton is the element of the singleton

@[simp]

theorem csSup_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a b : α) : sSup {a, b} = a ⊔ b

@[simp]

theorem csInf_pair {α : Type u_1} [ConditionallyCompleteLattice α] (a b : α) : sInf {a, b} = a ⊓ b

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.

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.

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.

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.

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.

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.

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.

@[simp]

theorem csInf_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) : sInf (Set.Icc a b) = a

@[simp]

theorem csInf_Ici {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} : sInf (Set.Ici a) = a

@[simp]

theorem csInf_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a < b) : sInf (Set.Ico a b) = a

@[simp]

theorem csInf_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) : sInf (Set.Ioc a b) = a

@[simp]

theorem csInf_Ioi {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMaxOrder α] [DenselyOrdered α] : sInf (Set.Ioi a) = a

@[simp]

theorem csInf_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) : sInf (Set.Ioo a b) = a

@[simp]

theorem csSup_Icc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a ≤ b) : sSup (Set.Icc a b) = b

@[simp]

theorem csSup_Ico {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) : sSup (Set.Ico a b) = b

@[simp]

theorem csSup_Iic {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} : sSup (Set.Iic a) = a

@[simp]

theorem csSup_Iio {α : Type u_1} [ConditionallyCompleteLattice α] {a : α} [NoMinOrder α] [DenselyOrdered α] : sSup (Set.Iio a) = a

@[simp]

theorem csSup_Ioc {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} (h : a < b) : sSup (Set.Ioc a b) = b

@[simp]

theorem csSup_Ioo {α : Type u_1} [ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α] (h : a < b) : sSup (Set.Ioo a b) = b

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

theorem sup_eq_top_of_top_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} [OrderTop α] (h : ⊤ ∈ s) : sSup s = ⊤

theorem inf_eq_bot_of_bot_mem {α : Type u_1} [ConditionallyCompleteLattice α] {s : Set α} [OrderBot α] (h : ⊥ ∈ s) : sInf s = ⊥

instance Pi.conditionallyCompleteLattice {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → ConditionallyCompleteLattice (α i)] : ConditionallyCompleteLattice ((i : ι) → α i)

Equations

• Pi.conditionallyCompleteLattice = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

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.

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.

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

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

theorem csSup_of_not_bddAbove {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddAbove s) : sSup s = sSup ∅

theorem csSup_eq_univ_of_not_bddAbove {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddAbove s) : sSup s = sSup Set.univ

theorem csInf_of_not_bddBelow {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) : sInf s = sInf ∅

theorem csInf_eq_univ_of_not_bddBelow {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} (hs : ¬BddBelow s) : sInf s = sInf Set.univ

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.

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.

theorem sSup_iUnion_Iic {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) : sSup (⋃ (i : ι), Set.Iic (f i)) = ⨆ (i : ι), f i

theorem sInf_iUnion_Ici {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) : sInf (⋃ (i : ι), Set.Ici (f i)) = ⨅ (i : ι), f i

theorem csInf_eq_bot_of_bot_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderBot α] {s : Set α} (hs : ⊥ ∈ s) : sInf s = ⊥

theorem csSup_eq_top_of_top_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderTop α] {s : Set α} (hs : ⊤ ∈ s) : sSup s = ⊤

theorem sInf_eq_argmin_on {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : sInf s = Function.argminOn id ⋯ s hs

theorem isLeast_csInf {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : IsLeast s (sInf s)

theorem le_csInf_iff' {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} {b : α} [WellFoundedLT α] (hs : s.Nonempty) : b ≤ sInf s ↔ b ∈ lowerBounds s

theorem csInf_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] (hs : s.Nonempty) : sInf s ∈ s

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)

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.

@[simp]

theorem csInf_univ {α : Type u_1} [ConditionallyCompleteLinearOrder α] [OrderBot α] : sInf Set.univ = ⊥

@[simp]

theorem csSup_empty {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] : sSup ∅ = ⊥

theorem isLUB_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} (hs : BddAbove s) : IsLUB s (sSup s)

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.

theorem csSup_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ upperBounds s) : sSup s ≤ a

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.

theorem le_csSup_iff' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : BddAbove s) : a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

theorem le_csInf_iff'' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (ne : s.Nonempty) : a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b

theorem csInf_le' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a ∈ s) : sInf s ≤ a

theorem exists_lt_of_lt_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s : Set α} {a : α} (h : a < sSup s) : ∃ b ∈ s, a < b

theorem not_mem_of_lt_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {x : α} {s : Set α} (h : x < sInf s) : x ∉ s

theorem csInf_le_csInf' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s t : Set α} (h₁ : t.Nonempty) (h₂ : t ⊆ s) : sInf s ≤ sInf t

theorem csSup_le_csSup' {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] {s t : Set α} (h₁ : BddAbove t) (h₂ : s ⊆ t) : sSup s ≤ sSup t

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.

theorem WithTop.isLUB_sSup {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) : IsLUB s (sSup s)

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.

theorem WithTop.isGLB_sInf {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] (s : Set (WithTop α)) : IsGLB s (sInf s)

noncomputable instance WithTop.instCompleteLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrderBot α] : CompleteLinearOrder (WithTop α)

Equations

• WithTop.instCompleteLinearOrder = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

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.

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.

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)

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

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

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)

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.

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)

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)

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)

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)

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)

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)

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)

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.

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

• WithTop.conditionallyCompleteLattice = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

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

• WithBot.conditionallyCompleteLattice = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯

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

Equations

• WithTop.WithBot.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• WithTop.WithBot.completeLinearOrder = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT

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

Equations

• WithBot.WithTop.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• WithBot.WithTop.completeLinearOrder = CompleteLinearOrder.mk ⋯ ⋯ ⋯ ⋯ ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT