Order-theoretic preliminaries

This module collects order-theoretic lemmas about infima and suprema in conditionally complete lattices, in particular closure under bounded infima and suprema.

def sInfClosed {α : Type u_1} [ConditionallyCompleteLattice α] (S : Set α) : Prop

The sInfClosed declaration.

Equations

• sInfClosed S = ∀ s ⊆ S, s.Nonempty → BddBelow s → sInf s ∈ S

def sSupClosed {α : Type u_1} [ConditionallyCompleteLattice α] (S : Set α) : Prop

The sSupClosed declaration.

Equations

• sSupClosed S = ∀ s ⊆ S, s.Nonempty → BddAbove s → sSup s ∈ S

theorem sInfClosed_top {α : Type u_1} [ConditionallyCompleteLattice α] : sInfClosed ⊤

theorem sInfClosed_Ici {α : Type u_1} [ConditionallyCompleteLattice α] (x : α) : sInfClosed (Set.Ici x)

theorem sInfClosed_bot {α : Type u_1} [ConditionallyCompleteLattice α] : sInfClosed ⊥

theorem sSupClosed_top {α : Type u_1} [ConditionallyCompleteLattice α] : sSupClosed ⊤

theorem sSupClosed_Iic {α : Type u_1} [ConditionallyCompleteLattice α] (x : α) : sSupClosed (Set.Iic x)

theorem sSupClosed_bot {α : Type u_1} [ConditionallyCompleteLattice α] : sSupClosed ⊥

class ContinuousOrderMap {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) : Prop

The ContinuousOrderMap type.

• monotone : Monotone f
• preimage_Ici_closed (x : β) : sInfClosed (f ⁻¹' Set.Ici x)
• preimage_Iic_closed (x : β) : sSupClosed (f ⁻¹' Set.Iic x)

class ContinuousOrderMapBounded {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) extends ContinuousOrderMap f : Prop

The ContinuousOrderMapBounded type.

• monotone : Monotone f
• preimage_Ici_closed (x : β) : sInfClosed (f ⁻¹' Set.Ici x)
• preimage_Iic_closed (x : β) : sSupClosed (f ⁻¹' Set.Iic x)
• bounded_preimage_Ici (y : β) : BddBelow (f ⁻¹' Set.Ici y)
• bounded_preimage_Iic (y : β) : BddAbove (f ⁻¹' Set.Iic y)

instance ContinuousOrderMap.instOrderDualCompCoeEquivToDualOfDual {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] : ContinuousOrderMap (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

theorem ContinuousOrderMap.map_sInf' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : f (sInf s) = sInf (f '' s)

theorem ContinuousOrderMap.map_sInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : f (sInf s) = ⨅ (x : ↑s), f ↑x

theorem ContinuousOrderMap.map_sSup' {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : f (sSup s) = sSup (f '' s)

theorem ContinuousOrderMap.map_sSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : f (sSup s) = ⨆ (x : ↑s), f ↑x

theorem ContinuousOrderMap.map_iInf {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {ι : Sort u_3} [Nonempty ι] {g : ι → α} (hbdd : BddBelow (Set.range g)) : f (⨅ (i : ι), g i) = ⨅ (i : ι), f (g i)

theorem ContinuousOrderMap.map_iSup {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMap f] {ι : Sort u_3} [Nonempty ι] {g : ι → α} (hbdd : BddAbove (Set.range g)) : f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

instance ContinuousOrderMapBounded.instOrderDualCompCoeEquivToDualOfDual {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) [ContinuousOrderMapBounded f] : ContinuousOrderMapBounded (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)

theorem ContinuousOrderMapBounded.bddBelow_iff {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) {s : Set α} [ContinuousOrderMapBounded f] : BddBelow (f '' s) ↔ BddBelow s

theorem ContinuousOrderMapBounded.bddAbove_iff {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] (f : α → β) {s : Set α} [ContinuousOrderMapBounded f] : BddAbove (f '' s) ↔ BddAbove s