Omega Complete Partial Orders

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

The concept of an omega-complete partial order (ωCPO) is useful for the formalization of the semantics of programming languages. Its notion of supremum helps define the meaning of recursive procedures.

Main definitions

• class OmegaCompletePartialOrder
• ite, map, bind, seq as continuous morphisms

Instances of OmegaCompletePartialOrder

• Part
• every CompleteLattice
• pi-types
• product types
• OrderHom
• ContinuousHom (with notation →𝒄)
  • an instance of OmegaCompletePartialOrder (α →𝒄 β)
• ContinuousHom.ofFun
• ContinuousHom.ofMono
• continuous functions:
  • id
  • ite
  • const
  • Part.bind
  • Part.map
  • Part.seq

References

• [Chain-complete posets and directed sets with applications][markowsky1976]
• [Recursive definitions of partial functions and their computations][cadiou1972]
• [Semantics of Programming Languages: Structures and Techniques][gunter1992]

@[simp]

theorem OrderHom.bind_coe {α : Type u_1} [Preorder α] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o β → Part γ) (x : α) : ↑(OrderHom.bind f g) x = ↑f x >>= ↑g x

def OrderHom.bind {α : Type u_1} [Preorder α] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o β → Part γ) : α →o Part γ

Part.bind as a monotone function

Equations

• OrderHom.bind f g = { toFun := fun x => ↑f x >>= ↑g x, monotone' := (_ : ∀ ⦃x y : α⦄, x ≤ y → ∀ (a : γ), a ∈ (fun x => ↑f x >>= ↑g x) x → a ∈ (fun x => ↑f x >>= ↑g x) y) }

def OmegaCompletePartialOrder.Chain (α : Type u) [Preorder α] : Type u

A chain is a monotone sequence.

See the definition on page 114 of [gunter1992].

Equations

• OmegaCompletePartialOrder.Chain α = (ℕ →o α)

instance OmegaCompletePartialOrder.Chain.instOrderHomClassChainNatInstLENatToLE {α : Type u} [Preorder α] : OrderHomClass (OmegaCompletePartialOrder.Chain α) ℕ α

Equations

• OmegaCompletePartialOrder.Chain.instOrderHomClassChainNatInstLENatToLE = inferInstanceAs (OrderHomClass (ℕ →o α) ℕ α)

instance OmegaCompletePartialOrder.Chain.instCoeFunChainForAllNat {α : Type u} [Preorder α] : CoeFun (OmegaCompletePartialOrder.Chain α) fun x => ℕ → α

Equations

• OmegaCompletePartialOrder.Chain.instCoeFunChainForAllNat = { coe := FunLike.coe }

instance OmegaCompletePartialOrder.Chain.instInhabitedChain {α : Type u} [Preorder α] [Inhabited α] : Inhabited (OmegaCompletePartialOrder.Chain α)

Equations

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

instance OmegaCompletePartialOrder.Chain.instMembershipChain {α : Type u} [Preorder α] : Membership α (OmegaCompletePartialOrder.Chain α)

Equations

• OmegaCompletePartialOrder.Chain.instMembershipChain = { mem := fun a c => ∃ i, a = ↑c i }

instance OmegaCompletePartialOrder.Chain.instLEChain {α : Type u} [Preorder α] : LE (OmegaCompletePartialOrder.Chain α)

Equations

• OmegaCompletePartialOrder.Chain.instLEChain = { le := fun x y => ∀ (i : ℕ), ∃ j, ↑x i ≤ ↑y j }

theorem OmegaCompletePartialOrder.Chain.isChain_range {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) : IsChain (fun x x_1 => x ≤ x_1) (Set.range ↑c)

theorem OmegaCompletePartialOrder.Chain.directed {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) : Directed (fun x x_1 => x ≤ x_1) ↑c

def OmegaCompletePartialOrder.Chain.map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) : OmegaCompletePartialOrder.Chain β

map function for Chain

Equations

• OmegaCompletePartialOrder.Chain.map c f = OrderHom.comp f c

@[simp]

theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) : ↑(OmegaCompletePartialOrder.Chain.map c f) = ↑f ∘ ↑c

theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (x : α) : x ∈ c → ↑f x ∈ OmegaCompletePartialOrder.Chain.map c f

theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} : b ∈ OmegaCompletePartialOrder.Chain.map c f → ∃ a, a ∈ c ∧ ↑f a = b

@[simp]

theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} : b ∈ OmegaCompletePartialOrder.Chain.map c f ↔ ∃ a, a ∈ c ∧ ↑f a = b

@[simp]

theorem OmegaCompletePartialOrder.Chain.map_id {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) : OmegaCompletePartialOrder.Chain.map c OrderHom.id = c

theorem OmegaCompletePartialOrder.Chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder α] [Preorder β] [Preorder γ] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ) : OmegaCompletePartialOrder.Chain.map (OmegaCompletePartialOrder.Chain.map c f) g = OmegaCompletePartialOrder.Chain.map c (OrderHom.comp g f)

theorem OmegaCompletePartialOrder.Chain.map_le_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {g : α →o β} (h : f ≤ g) : OmegaCompletePartialOrder.Chain.map c f ≤ OmegaCompletePartialOrder.Chain.map c g

def OmegaCompletePartialOrder.Chain.zip {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) : OmegaCompletePartialOrder.Chain (α × β)

OmegaCompletePartialOrder.Chain.zip pairs up the elements of two chains that have the same index.

Equations

• OmegaCompletePartialOrder.Chain.zip c₀ c₁ = OrderHom.prod c₀ c₁

@[simp]

theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) (n : ℕ) : ↑(OmegaCompletePartialOrder.Chain.zip c₀ c₁) n = (↑c₀ n, ↑c₁ n)

class OmegaCompletePartialOrder (α : Type u_1) extends PartialOrder : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• ωSup : OmegaCompletePartialOrder.Chain α → α

  The supremum of an increasing sequence

• le_ωSup : ∀ (c : OmegaCompletePartialOrder.Chain α) (i : ℕ), ↑c i ≤ OmegaCompletePartialOrder.ωSup c

  ωSup is an upper bound of the increasing sequence

• ωSup_le : ∀ (c : OmegaCompletePartialOrder.Chain α) (x : α), (∀ (i : ℕ), ↑c i ≤ x) → OmegaCompletePartialOrder.ωSup c ≤ x

  ωSup is a lower bound of the set of upper bounds of the increasing sequence

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

See the definition on page 114 of [gunter1992].

@[reducible]

def OmegaCompletePartialOrder.lift {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [PartialOrder β] (f : β →o α) (ωSup₀ : OmegaCompletePartialOrder.Chain β → β) (h : ∀ (x y : β), ↑f x ≤ ↑f y → x ≤ y) (h' : ∀ (c : OmegaCompletePartialOrder.Chain β), ↑f (ωSup₀ c) = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c f)) : OmegaCompletePartialOrder β

Transfer an OmegaCompletePartialOrder on β to an OmegaCompletePartialOrder on α using a strictly monotone function f : β →o α, a definition of ωSup and a proof that f is continuous with regard to the provided ωSup and the ωCPO on α.

Equations

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

theorem OmegaCompletePartialOrder.le_ωSup_of_le {α : Type u} [OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} (i : ℕ) (h : x ≤ ↑c i) : x ≤ OmegaCompletePartialOrder.ωSup c

theorem OmegaCompletePartialOrder.ωSup_total {α : Type u} [OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {x : α} (h : ∀ (i : ℕ), ↑c i ≤ x ∨ x ≤ ↑c i) : OmegaCompletePartialOrder.ωSup c ≤ x ∨ x ≤ OmegaCompletePartialOrder.ωSup c

theorem OmegaCompletePartialOrder.ωSup_le_ωSup_of_le {α : Type u} [OmegaCompletePartialOrder α] {c₀ : OmegaCompletePartialOrder.Chain α} {c₁ : OmegaCompletePartialOrder.Chain α} (h : c₀ ≤ c₁) : OmegaCompletePartialOrder.ωSup c₀ ≤ OmegaCompletePartialOrder.ωSup c₁

theorem OmegaCompletePartialOrder.ωSup_le_iff {α : Type u} [OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) (x : α) : OmegaCompletePartialOrder.ωSup c ≤ x ↔ ∀ (i : ℕ), ↑c i ≤ x

theorem OmegaCompletePartialOrder.isLUB_range_ωSup {α : Type u} [OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α) : IsLUB (Set.range ↑c) (OmegaCompletePartialOrder.ωSup c)

theorem OmegaCompletePartialOrder.ωSup_eq_of_isLUB {α : Type u} [OmegaCompletePartialOrder α] {c : OmegaCompletePartialOrder.Chain α} {a : α} (h : IsLUB (Set.range ↑c) a) : a = OmegaCompletePartialOrder.ωSup c

def OmegaCompletePartialOrder.subtype {α : Type u_2} [OmegaCompletePartialOrder α] (p : α → Prop) (hp : (c : OmegaCompletePartialOrder.Chain α) → ((i : α) → i ∈ c → p i) → p (OmegaCompletePartialOrder.ωSup c)) : OmegaCompletePartialOrder (Subtype p)

A subset p : α → Prop of the type closed under ωSup induces an OmegaCompletePartialOrder on the subtype {a : α // p a}.

Equations

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

def OmegaCompletePartialOrder.Continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) : Prop

A monotone function f : α →o β is continuous if it distributes over ωSup.

In order to distinguish it from the (more commonly used) continuity from topology (see Mathlib/Topology/Basic.lean), the present definition is often referred to as "Scott-continuity" (referring to Dana Scott). It corresponds to continuity in Scott topological spaces (not defined here).

Equations

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

def OmegaCompletePartialOrder.Continuous' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) : Prop

Continuous' f asserts that f is both monotone and continuous.

Equations

• OmegaCompletePartialOrder.Continuous' f = ∃ hf, OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }

theorem OmegaCompletePartialOrder.isLUB_of_scottContinuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {c : OmegaCompletePartialOrder.Chain α} {f : α → β} (hf : ScottContinuous f) : IsLUB (Set.range ↑(OmegaCompletePartialOrder.Chain.map c { toFun := f, monotone' := (_ : Monotone f) })) (f (OmegaCompletePartialOrder.ωSup c))

theorem OmegaCompletePartialOrder.ScottContinuous.continuous' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} (hf : ScottContinuous f) : OmegaCompletePartialOrder.Continuous' f

theorem OmegaCompletePartialOrder.Continuous'.to_monotone {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} (hf : OmegaCompletePartialOrder.Continuous' f) : Monotone f

theorem OmegaCompletePartialOrder.Continuous.of_bundled {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) (hf : Monotone f) (hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }) : OmegaCompletePartialOrder.Continuous' f

theorem OmegaCompletePartialOrder.Continuous.of_bundled' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf' : OmegaCompletePartialOrder.Continuous f) : OmegaCompletePartialOrder.Continuous' ↑f

theorem OmegaCompletePartialOrder.Continuous'.to_bundled {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) (hf : OmegaCompletePartialOrder.Continuous' f) : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := (_ : Monotone f) }

@[simp]

theorem OmegaCompletePartialOrder.continuous'_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →o β} : OmegaCompletePartialOrder.Continuous' ↑f ↔ OmegaCompletePartialOrder.Continuous f

theorem OmegaCompletePartialOrder.continuous_id {α : Type u} [OmegaCompletePartialOrder α] : OmegaCompletePartialOrder.Continuous OrderHom.id

theorem OmegaCompletePartialOrder.continuous_comp {α : Type u} {β : Type v} {γ : Type u_1} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : α →o β) (g : β →o γ) (hfc : OmegaCompletePartialOrder.Continuous f) (hgc : OmegaCompletePartialOrder.Continuous g) : OmegaCompletePartialOrder.Continuous (OrderHom.comp g f)

theorem OmegaCompletePartialOrder.id_continuous' {α : Type u} [OmegaCompletePartialOrder α] : OmegaCompletePartialOrder.Continuous' id

theorem OmegaCompletePartialOrder.continuous_const {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) : OmegaCompletePartialOrder.Continuous (↑(OrderHom.const α) x)

theorem OmegaCompletePartialOrder.const_continuous' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) : OmegaCompletePartialOrder.Continuous' (Function.const α x)

theorem Part.eq_of_chain {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} {b : α} (ha : Part.some a ∈ c) (hb : Part.some b ∈ c) : a = b

noncomputable def Part.ωSup {α : Type u} (c : OmegaCompletePartialOrder.Chain (Part α)) : Part α

The (noncomputable) ωSup definition for the ω-CPO structure on Part α.

Equations

• Part.ωSup c = if h : ∃ a, Part.some a ∈ c then Part.some (Classical.choose h) else Part.none

theorem Part.ωSup_eq_some {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} (h : Part.some a ∈ c) : Part.ωSup c = Part.some a

theorem Part.ωSup_eq_none {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬∃ a, Part.some a ∈ c) : Part.ωSup c = Part.none

theorem Part.mem_chain_of_mem_ωSup {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} (h : a ∈ Part.ωSup c) : Part.some a ∈ c

noncomputable instance Part.omegaCompletePartialOrder {α : Type u} : OmegaCompletePartialOrder (Part α)

Equations

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

theorem Part.mem_ωSup {α : Type u} (x : α) (c : OmegaCompletePartialOrder.Chain (Part α)) : x ∈ OmegaCompletePartialOrder.ωSup c ↔ Part.some x ∈ c

instance Pi.instOmegaCompletePartialOrderForAll {α : Type u_1} {β : α → Type u_2} [(a : α) → OmegaCompletePartialOrder (β a)] : OmegaCompletePartialOrder ((a : α) → β a)

Equations

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

theorem Pi.OmegaCompletePartialOrder.flip₁_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] (f : (x : α) → γ → β x) (a : α) (hf : OmegaCompletePartialOrder.Continuous' fun x y => f y x) : OmegaCompletePartialOrder.Continuous' (f a)

theorem Pi.OmegaCompletePartialOrder.flip₂_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] (f : γ → (x : α) → β x) (hf : ∀ (x : α), OmegaCompletePartialOrder.Continuous' fun g => f g x) : OmegaCompletePartialOrder.Continuous' f

@[simp]

theorem Prod.ωSup_fst {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).fst = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.fst)

@[simp]

theorem Prod.ωSup_snd {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).snd = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.snd)

def Prod.ωSup {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : α × β

The supremum of a chain in the product ω-CPO.

Equations

• Prod.ωSup c = (OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.fst), OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.snd))

@[simp]

theorem Prod.instOmegaCompletePartialOrderProd_ωSup_snd {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).snd = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.snd)

@[simp]

theorem Prod.instOmegaCompletePartialOrderProd_ωSup_fst {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).fst = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c OrderHom.fst)

instance Prod.instOmegaCompletePartialOrderProd {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α × β)

Equations

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

theorem Prod.ωSup_zip {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) : OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.zip c₀ c₁) = (OmegaCompletePartialOrder.ωSup c₀, OmegaCompletePartialOrder.ωSup c₁)

instance CompleteLattice.instOmegaCompletePartialOrder (α : Type u) [CompleteLattice α] : OmegaCompletePartialOrder α

Any complete lattice has an ω-CPO structure where the countable supremum is a special case of arbitrary suprema.

Equations

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

theorem CompleteLattice.sSup_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] (s : Set (α →o β)) (hs : ∀ (f : α →o β), f ∈ s → OmegaCompletePartialOrder.Continuous f) : OmegaCompletePartialOrder.Continuous (sSup s)

theorem CompleteLattice.iSup_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] {ι : Sort u_1} {f : ι → α →o β} (h : ∀ (i : ι), OmegaCompletePartialOrder.Continuous (f i)) : OmegaCompletePartialOrder.Continuous (⨆ (i : ι), f i)

theorem CompleteLattice.sSup_continuous' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] (s : Set (α → β)) (hc : ∀ (f : α → β), f ∈ s → OmegaCompletePartialOrder.Continuous' f) : OmegaCompletePartialOrder.Continuous' (sSup s)

theorem CompleteLattice.sup_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] {f : α →o β} {g : α →o β} (hf : OmegaCompletePartialOrder.Continuous f) (hg : OmegaCompletePartialOrder.Continuous g) : OmegaCompletePartialOrder.Continuous (f ⊔ g)

theorem CompleteLattice.top_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] : OmegaCompletePartialOrder.Continuous ⊤

theorem CompleteLattice.bot_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] : OmegaCompletePartialOrder.Continuous ⊥

theorem CompleteLattice.inf_continuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [CompleteLinearOrder β] (f : α →o β) (g : α →o β) (hf : OmegaCompletePartialOrder.Continuous f) (hg : OmegaCompletePartialOrder.Continuous g) : OmegaCompletePartialOrder.Continuous (f ⊓ g)

theorem CompleteLattice.inf_continuous' {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [CompleteLinearOrder β] {f : α → β} {g : α → β} (hf : OmegaCompletePartialOrder.Continuous' f) (hg : OmegaCompletePartialOrder.Continuous' g) : OmegaCompletePartialOrder.Continuous' (f ⊓ g)

@[simp]

theorem OmegaCompletePartialOrder.OrderHom.ωSup_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α) : ↑(OmegaCompletePartialOrder.OrderHom.ωSup c) a = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c (OrderHom.apply a))

def OmegaCompletePartialOrder.OrderHom.ωSup {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →o β)) : α →o β

The ωSup operator for monotone functions.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →o β)) (a : α) : ↑(OmegaCompletePartialOrder.ωSup c) a = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c (OrderHom.apply a))

instance OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α →o β)

Equations

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

structure OmegaCompletePartialOrder.ContinuousHom (α : Type u) (β : Type v) [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] extends OrderHom : Type (max u v)

• toFun : α → β
• monotone' : Monotone s.toFun
• cont : OmegaCompletePartialOrder.Continuous s.toOrderHom

  The underlying function of a ContinuousHom is continuous, i.e. it preserves ωSup

A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of OrderHom.continuous.

def OmegaCompletePartialOrder.«term_→𝒄_» : Lean.TrailingParserDescr

A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of OrderHom.continuous.

Equations

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

instance OmegaCompletePartialOrder.instOrderHomClassContinuousHomToLEToPreorderToPartialOrderToLEToPreorderToPartialOrder (α : Type u) (β : Type v) [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OrderHomClass (α →𝒄 β) α β

Equations

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

instance OmegaCompletePartialOrder.instPartialOrderContinuousHom (α : Type u) (β : Type v) [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : PartialOrder (α →𝒄 β)

Equations

• OmegaCompletePartialOrder.instPartialOrderContinuousHom α β = PartialOrder.lift (fun f => f.toFun) (_ : ∀ ⦃a₁ a₂ : α →𝒄 β⦄, (fun f => f.toFun) a₁ = (fun f => f.toFun) a₂ → a₁ = a₂)

theorem OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : f.toOrderHom = ↑f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf : OmegaCompletePartialOrder.Continuous f) : ↑{ toOrderHom := f, cont := hf } = ↑f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : ↑f.toOrderHom = ↑f

def OmegaCompletePartialOrder.ContinuousHom.Simps.apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (h : α →𝒄 β) : α → β

See Note [custom simps projection]. We specify this explicitly because we don't have a FunLike instance.

Equations

• OmegaCompletePartialOrder.ContinuousHom.Simps.apply h = ↑h

theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} (h : f = g) (x : α) : ↑f x = ↑g x

theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) {x : α} {y : α} (h : x = y) : ↑f x = ↑f y

theorem OmegaCompletePartialOrder.ContinuousHom.monotone {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : Monotone ↑f

theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} {x : α} {y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : ↑f x ≤ ↑g y

theorem OmegaCompletePartialOrder.ContinuousHom.ite_continuous' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {p : Prop} [hp : Decidable p] (f : α → β) (g : α → β) (hf : OmegaCompletePartialOrder.Continuous' f) (hg : OmegaCompletePartialOrder.Continuous' g) : OmegaCompletePartialOrder.Continuous' fun x => if p then f x else g x

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_bind {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (c : OmegaCompletePartialOrder.Chain α) (f : α →o Part β) (g : α →o β → Part γ) : OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c (OrderHom.bind f g)) = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c f) >>= OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c g)

theorem OmegaCompletePartialOrder.ContinuousHom.bind_continuous' {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α → Part β) (g : α → β → Part γ) : OmegaCompletePartialOrder.Continuous' f → OmegaCompletePartialOrder.Continuous' g → OmegaCompletePartialOrder.Continuous' fun x => f x >>= g x

theorem OmegaCompletePartialOrder.ContinuousHom.map_continuous' {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : β → γ) (g : α → Part β) (hg : OmegaCompletePartialOrder.Continuous' g) : OmegaCompletePartialOrder.Continuous' fun x => f <$> g x

theorem OmegaCompletePartialOrder.ContinuousHom.seq_continuous' {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α → Part (β → γ)) (g : α → Part β) (hf : OmegaCompletePartialOrder.Continuous' f) (hg : OmegaCompletePartialOrder.Continuous' g) : OmegaCompletePartialOrder.Continuous' fun x => Seq.seq (f x) fun x_1 => g x

theorem OmegaCompletePartialOrder.ContinuousHom.continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (F : α →𝒄 β) (C : OmegaCompletePartialOrder.Chain α) : ↑F (OmegaCompletePartialOrder.ωSup C) = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map C ↑F)

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.copy_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) (g : α →𝒄 β) (h : f = ↑g) : ∀ (a : α), ↑(OmegaCompletePartialOrder.ContinuousHom.copy f g h) a = f a

def OmegaCompletePartialOrder.ContinuousHom.copy {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) (g : α →𝒄 β) (h : f = ↑g) : α →𝒄 β

Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.

Equations

• OmegaCompletePartialOrder.ContinuousHom.copy f g h = { toOrderHom := OrderHom.copy g.toOrderHom f h, cont := (_ : OmegaCompletePartialOrder.Continuous (OrderHom.copy g.toOrderHom f h)) }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.id_apply {α : Type u} [OmegaCompletePartialOrder α] (a : α) : ↑OmegaCompletePartialOrder.ContinuousHom.id a = a

def OmegaCompletePartialOrder.ContinuousHom.id {α : Type u} [OmegaCompletePartialOrder α] : α →𝒄 α

The identity as a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.id = { toOrderHom := OrderHom.id, cont := (_ : OmegaCompletePartialOrder.Continuous OrderHom.id) }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) : ∀ (a : α), ↑(OmegaCompletePartialOrder.ContinuousHom.comp f g) a = ↑f (↑g a)

def OmegaCompletePartialOrder.ContinuousHom.comp {α : Type u} {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) : α →𝒄 γ

The composition of continuous functions.

Equations

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

theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : ∀ (x : α), ↑f x = ↑g x) : f = g

theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : ↑f = ↑g) : f = g

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.comp_id {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) : OmegaCompletePartialOrder.ContinuousHom.comp f OmegaCompletePartialOrder.ContinuousHom.id = f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) : OmegaCompletePartialOrder.ContinuousHom.comp OmegaCompletePartialOrder.ContinuousHom.id f = f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] [OmegaCompletePartialOrder φ] (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) : OmegaCompletePartialOrder.ContinuousHom.comp f (OmegaCompletePartialOrder.ContinuousHom.comp g h) = OmegaCompletePartialOrder.ContinuousHom.comp (OmegaCompletePartialOrder.ContinuousHom.comp f g) h

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a : α) (f : α →𝒄 β) : ↑↑f a = ↑f a

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.const_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) : ∀ (a : α), ↑(OmegaCompletePartialOrder.ContinuousHom.const x) a = x

def OmegaCompletePartialOrder.ContinuousHom.const {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) : α →𝒄 β

Function.const is a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.const x = { toOrderHom := ↑(OrderHom.const α) x, cont := (_ : OmegaCompletePartialOrder.Continuous (↑(OrderHom.const α) x)) }

instance OmegaCompletePartialOrder.ContinuousHom.instInhabitedContinuousHom {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [Inhabited β] : Inhabited (α →𝒄 β)

Equations

• OmegaCompletePartialOrder.ContinuousHom.instInhabitedContinuousHom = { default := OmegaCompletePartialOrder.ContinuousHom.const default }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.toMono_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : ↑OmegaCompletePartialOrder.ContinuousHom.toMono f = ↑f

def OmegaCompletePartialOrder.ContinuousHom.toMono {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : (α →𝒄 β) →o α →o β

The map from continuous functions to monotone functions is itself a monotone function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.toMono = { toFun := fun f => ↑f, monotone' := (_ : ∀ (x x_1 : α →𝒄 β), x ≤ x_1 → x ≤ x_1) }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) : (∀ (i j : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z) ↔ ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z

When proving that a chain of applications is below a bound z, it suffices to consider the functions and values being selected from the same index in the chains.

This lemma is more specific than necessary, i.e. c₀ only needs to be a chain of monotone functions, but it is only used with continuous functions.

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) : (∀ (j i : ℕ), ↑(↑c₀ i) (↑c₁ j) ≤ z) ↔ ∀ (i : ℕ), ↑(↑c₀ i) (↑c₁ i) ≤ z

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (a : α) : ↑(OmegaCompletePartialOrder.ContinuousHom.ωSup c) a = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map (OmegaCompletePartialOrder.Chain.map c OmegaCompletePartialOrder.ContinuousHom.toMono) (OrderHom.apply a))

def OmegaCompletePartialOrder.ContinuousHom.ωSup {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) : α →𝒄 β

The ωSup operator for continuous functions, which takes the pointwise countable supremum of the functions in the ω-chain.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.instOmegaCompletePartialOrderContinuousHom_ωSup {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) : OmegaCompletePartialOrder.ωSup c = OmegaCompletePartialOrder.ContinuousHom.ωSup c

instance OmegaCompletePartialOrder.ContinuousHom.instOmegaCompletePartialOrderContinuousHom {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α →𝒄 β)

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : (α →𝒄 β) × α) : ↑OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = ↑f.fst f.snd

def OmegaCompletePartialOrder.ContinuousHom.Prod.apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : (α →𝒄 β) × α →𝒄 β

The application of continuous functions as a continuous function.

Equations

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

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_def {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (x : α) : ↑(OmegaCompletePartialOrder.ωSup c) x = ↑(OmegaCompletePartialOrder.ContinuousHom.ωSup c) x

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) : ↑(OmegaCompletePartialOrder.ωSup c₀) (OmegaCompletePartialOrder.ωSup c₁) = ↑OmegaCompletePartialOrder.ContinuousHom.Prod.apply (OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.zip c₀ c₁))

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_5} (f : α → β →𝒄 γ) (x : β) (y : α) : ↑(OmegaCompletePartialOrder.ContinuousHom.flip f) x y = ↑(f y) x

def OmegaCompletePartialOrder.ContinuousHom.flip {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_5} (f : α → β →𝒄 γ) : β →𝒄 α → γ

A family of continuous functions yields a continuous family of functions.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ) (x : α) : ↑(OmegaCompletePartialOrder.ContinuousHom.bind f g) x = ↑f x >>= ↑g x

noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ) : α →𝒄 Part γ

Part.bind as a continuous function.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : β → γ) (g : α →𝒄 Part β) (x : α) : ↑(OmegaCompletePartialOrder.ContinuousHom.map f g) x = f <$> ↑g x

noncomputable def OmegaCompletePartialOrder.ContinuousHom.map {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : β → γ) (g : α →𝒄 Part β) : α →𝒄 Part γ

Part.map as a continuous function.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (β → γ)) (g : α →𝒄 Part β) (x : α) : ↑(OmegaCompletePartialOrder.ContinuousHom.seq f g) x = Seq.seq (↑f x) fun x => ↑g x

noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (β → γ)) (g : α →𝒄 Part β) : α →𝒄 Part γ

Part.seq as a continuous function.

Equations

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