Conditionally complete lattice structure on WithTop and WithBot

This file extends sSup and sInf from α to WithTop α and WithBot α, and shows that they are conditionally complete lattices when α is. We also show that WithTop (WithBot α) and WithBot (WithTop α) are complete lattices.

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

@[instance_reducible]

noncomputable instance WithTop.instSupSet {α : Type u_1} [LE α] [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 ⊤ }

@[instance_reducible]

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

Equations

• WithBot.instInfSet = { sInf := fun (S : Set (WithBot α)) => if ⊥ ∈ S then ⊥ else if BddBelow ((fun (a : α) => ↑a) ⁻¹' S) then ↑(sInf ((fun (a : α) => ↑a) ⁻¹' S)) else ⊥ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• WithBot.instSupSet = { sSup := fun (S : Set (WithBot α)) => if S ⊆ {⊥} ∨ ¬BddAbove S then ⊥ else ↑(sSup ((fun (a : α) => ↑a) ⁻¹' S)) }

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem WithTop.sInf_singleton_top {α : Type u_1} [LE α] [InfSet α] : sInf {⊤} = ⊤

@[simp]

theorem WithBot.sSup_singleton_bot {α : Type u_1} [LE α] [SupSet α] : sSup {⊥} = ⊥

@[simp]

theorem WithTop.sSup_of_top_mem {α : Type u_1} [LE α] [SupSet α] {s : Set (WithTop α)} (h : ⊤ ∈ s) : sSup s = ⊤

@[simp]

theorem WithBot.sInf_of_bot_mem {α : Type u_1} [LE α] [InfSet α] {s : Set (WithBot α)} (h : ⊥ ∈ s) : sInf s = ⊥

theorem WithTop.sSup_singleton_top {α : Type u_1} [LE α] [SupSet α] : sSup {⊤} = ⊤

theorem WithBot.sInf_singleton_bot {α : Type u_1} [LE α] [InfSet α] : sInf {⊥} = ⊥

theorem WithTop.sSup_of_not_bddAbove {α : Type u_1} [LE α] [SupSet α] {s : Set (WithTop α)} (h : ¬BddAbove (some ⁻¹' s)) : sSup s = ⊤

theorem WithBot.sInf_of_not_bddBelow {α : Type u_1} [LE α] [InfSet α] {s : Set (WithBot α)} (h : ¬BddBelow (some ⁻¹' s)) : sInf s = ⊥

@[simp]

theorem WithTop.sInf_of_not_bddBelow {α : Type u_1} [LE α] [InfSet α] {s : Set (WithTop α)} (h : ¬BddBelow s) : sInf s = ⊤

@[simp]

theorem WithBot.sSup_of_not_bddAbove {α : Type u_1} [LE α] [SupSet α] {s : Set (WithBot α)} (h : ¬BddAbove s) : sSup s = ⊥

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

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

theorem WithTop.sSup_empty (α : Type u_5) [CompleteLattice α] : sSup ∅ = ⊥

theorem WithBot.sInf_empty (α : Type u_5) [CompleteLattice α] : 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 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 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 WithBot.isGLB_sInf' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithBot β)} (hs : s.Nonempty) : IsGLB s (sInf s)

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 WithBot.isLUB_sSup' {β : Type u_5} [ConditionallyCompleteLattice β] {s : Set (WithBot β)} (hs : BddAbove s) : IsLUB s (sSup s)

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

@[instance_reducible]

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

Equations

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

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.

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.

@[instance_reducible]

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 = { toLattice := WithTop.lattice, toSupSet := WithTop.instSupSet, toInfSet := WithTop.instInfSet, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }

@[instance_reducible]

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 = { toLattice := WithBot.lattice, toSupSet := WithBot.instSupSet, toInfSet := WithBot.instInfSet, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }

@[instance_reducible]

noncomputable instance instCompleteLatticeWithTop {α : Type u_1} [CompleteLattice α] : CompleteLattice (WithTop α)

Equations

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

@[instance_reducible]

noncomputable instance instCompleteLatticeWithBot {α : Type u_1} [CompleteLattice α] : CompleteLattice (WithBot α)

Equations

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

@[instance_reducible]

noncomputable instance instCompleteLinearOrderWithBot {α : Type u_1} [CompleteLinearOrder α] : CompleteLinearOrder (WithBot α)

Equations

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

@[instance_reducible]

noncomputable instance instConditionallyCompleteLinearOrderWithTop {α : Type u_1} [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrder (WithTop α)

Equations

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

@[instance_reducible]

noncomputable instance instConditionallyCompleteLinearOrderBotWithBotOfConditionallyCompleteLinearOrder {α : Type u_1} [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot (WithBot α)

Equations

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

@[instance_reducible]

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.

@[instance_reducible]

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.

@[instance_reducible]

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.

Extension of iSup and iInf from a preorder α to WithTop α and WithBot α

theorem WithTop.iInf_empty {α : Type u_1} {ι : Sort u_4} [Preorder α] [IsEmpty ι] [InfSet α] (f : ι → WithTop α) : ⨅ (i : ι), f i = ⊤

theorem WithBot.iSup_empty {α : Type u_1} {ι : Sort u_4} [Preorder α] [IsEmpty ι] [SupSet α] (f : ι → WithBot α) : ⨆ (i : ι), f i = ⊥

theorem WithTop.coe_iInf {α : Type u_1} {ι : Sort u_4} [Preorder α] [Nonempty ι] [InfSet α] {f : ι → α} (hf : BddBelow (Set.range f)) : ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

theorem WithBot.coe_iSup {α : Type u_1} {ι : Sort u_4} [Preorder α] [Nonempty ι] [SupSet α] {f : ι → α} (hf : BddAbove (Set.range f)) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

theorem WithTop.coe_iSup {α : Type u_1} {ι : Sort u_4} [Preorder α] [SupSet α] (f : ι → α) (h : BddAbove (Set.range f)) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

theorem WithBot.coe_iInf {α : Type u_1} {ι : Sort u_4} [Preorder α] [InfSet α] (f : ι → α) (h : BddBelow (Set.range f)) : ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

@[deprecated WithBot.iSup_empty (since := "2026-05-04")]

theorem WithBot.ciSup_empty {α : Type u_1} {ι : Sort u_4} [Preorder α] [IsEmpty ι] [SupSet α] (f : ι → WithBot α) : ⨆ (i : ι), f i = ⊥

Alias of WithBot.iSup_empty.

theorem WithBot.coe_biSup {ι : Type u_5} {s : Set ι} (hs : s.Nonempty) {α : Type u_6} [CompleteLattice α] (f : ι → α) : ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

theorem WithTop.coe_biInf {ι : Type u_5} {s : Set ι} (hs : s.Nonempty) {α : Type u_6} [CompleteLattice α] (f : ι → α) : ↑(⨅ i ∈ s, f i) = ⨅ i ∈ s, ↑(f i)

theorem WithBot.coe_biInf {ι : Type u_5} {s : Set ι} {α : Type u_6} [CompleteLattice α] (f : ι → α) : ↑(⨅ i ∈ s, f i) = ⨅ i ∈ s, ↑(f i)

theorem WithTop.coe_biSup {ι : Type u_5} {s : Set ι} {α : Type u_6} [CompleteLattice α] (f : ι → α) : ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

theorem WithTop.iSup_coe_eq_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} : ⨆ (x : ι), ↑(f x) = ⊤ ↔ ¬BddAbove (Set.range f)

theorem WithTop.iSup_coe_lt_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} : ⨆ (x : ι), ↑(f x) < ⊤ ↔ BddAbove (Set.range f)

theorem WithTop.iInf_coe_eq_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} : ⨅ (x : ι), ↑(f x) = ⊤ ↔ IsEmpty ι

theorem WithTop.iInf_coe_lt_top {α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrderBot α] {f : ι → α} : ⨅ (i : ι), ↑(f i) < ⊤ ↔ Nonempty ι