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
omega_complete_partial_order ite,map,bind,seqas continuous morphisms
Instances of omega_complete_partial_order
roption- every
complete_lattice - pi-types
- product types
monotone_homcontinuous_hom(with notation →𝒄)- an instance of
omega_complete_partial_order (α →𝒄 β)
- an instance of
continuous_hom.of_funcontinuous_hom.of_mono- continuous functions:
iditeconstroption.bindroption.maproption.seq
References
- [G. Markowsky, Chain-complete posets and directed sets with applications, https://doi.org/10.1007/BF02485815][markowsky]
- [J. M. Cadiou and Zohar Manna, Recursive definitions of partial functions and their computations., https://doi.org/10.1145/942580.807072][cadiou]
- [Carl A. Gunter, Semantics of Programming Languages: Structures and Techniques, ISBN: 0262570955][gunter]
@[simp]
theorem
preorder_hom.const_to_fun
(α : Type u_1)
{β : Type u_2}
[preorder α]
[preorder β]
(f : β)
(a : α) :
⇑(preorder_hom.const α f) a = function.const α f a
The constant function, as a monotone function.
Equations
- preorder_hom.const α f = {to_fun := function.const α f, monotone' := _}
The diagonal function, as a monotone function.
Equations
- preorder_hom.prod.diag = {to_fun := λ (x : α), (x, x), monotone' := _}
@[simp]
theorem
preorder_hom.prod.diag_to_fun
{α : Type u_1}
[preorder α]
(x : α) :
⇑preorder_hom.prod.diag x = (x, x)
@[simp]
theorem
preorder_hom.prod.fst_to_fun
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(c : α × β) :
@[simp]
theorem
preorder_hom.prod.snd_to_fun
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
(c : α × β) :
@[simp]
theorem
preorder_hom.prod.zip_to_fun
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[preorder α]
[preorder β]
[preorder γ]
(f : α →ₘ β)
(g : α →ₘ γ)
(a : α) :
⇑(preorder_hom.prod.zip f g) a = (⇑(preorder_hom.prod.map f g) ∘ ⇑preorder_hom.prod.diag) a
A chain is a monotonically increasing sequence.
See the definition on page 114 of [gunter].
Equations
@[instance]
@[instance]
@[instance]
@[instance]
Equations
- omega_complete_partial_order.chain.has_le = {le := λ (x y : omega_complete_partial_order.chain α), ∀ (i : ℕ), ∃ (j : ℕ), ⇑x i ≤ ⇑y j}
def
omega_complete_partial_order.chain.map
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c : omega_complete_partial_order.chain α)
(f : α →ₘ β) :
map function for chain
theorem
omega_complete_partial_order.chain.mem_map
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c : omega_complete_partial_order.chain α)
{f : α →ₘ β}
(x : α)
(a : x ∈ c) :
@[simp]
theorem
omega_complete_partial_order.chain.map_id
{α : Type u}
[preorder α]
(c : omega_complete_partial_order.chain α) :
c.map preorder_hom.id = c
theorem
omega_complete_partial_order.chain.map_le_map
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c : omega_complete_partial_order.chain α)
{f g : α →ₘ β}
(h : f ≤ g) :
def
omega_complete_partial_order.chain.zip
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c₀ : omega_complete_partial_order.chain α)
(c₁ : omega_complete_partial_order.chain β) :
chain.zip pairs up the elements of two chains that have the same index
Equations
- c₀.zip c₁ = preorder_hom.prod.zip c₀ c₁
@[simp]
theorem
omega_complete_partial_order.chain.zip_to_fun
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c₀ : omega_complete_partial_order.chain α)
(c₁ : omega_complete_partial_order.chain β)
(a : ℕ) :
⇑(c₀.zip c₁) a = (⇑(preorder_hom.prod.map c₀ c₁) ∘ ⇑preorder_hom.prod.diag) a
@[class]
- to_partial_order : partial_order α
- ωSup : omega_complete_partial_order.chain α → α
- le_ωSup : ∀ (c_1 : omega_complete_partial_order.chain α) (i : ℕ), ⇑c_1 i ≤ omega_complete_partial_order.ωSup c_1
- ωSup_le : ∀ (c_1 : omega_complete_partial_order.chain α) (x : α), (∀ (i : ℕ), ⇑c_1 i ≤ x) → omega_complete_partial_order.ωSup c_1 ≤ x
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 [gunter].
Instances
- complete_lattice.omega_complete_partial_order
- roption.omega_complete_partial_order
- pi.omega_complete_partial_order
- prod.omega_complete_partial_order
- omega_complete_partial_order.preorder_hom.omega_complete_partial_order
- omega_complete_partial_order.continuous_hom.omega_complete_partial_order
- ωCPO.omega_complete_partial_order
def
omega_complete_partial_order.lift
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[partial_order β]
(f : β →ₘ α)
(ωSup₀ : omega_complete_partial_order.chain β → β)
(h : ∀ (x y : β), ⇑f x ≤ ⇑f y → x ≤ y)
(h' : ∀ (c : omega_complete_partial_order.chain β), ⇑f (ωSup₀ c) = omega_complete_partial_order.ωSup (c.map f)) :
Transfer a omega_complete_partial_order on β to a omega_complete_partial_order on α using
a strictly monotone function f : β →ₘ α, a definition of ωSup and a proof that f is continuous
with regard to the provided ωSup and the ωCPO on α.
Equations
- omega_complete_partial_order.lift f ωSup₀ h h' = {to_partial_order := _inst_2, ωSup := ωSup₀, le_ωSup := _, ωSup_le := _}
theorem
omega_complete_partial_order.le_ωSup_of_le
{α : Type u}
[omega_complete_partial_order α]
{c : omega_complete_partial_order.chain α}
{x : α}
(i : ℕ)
(h : x ≤ ⇑c i) :
theorem
omega_complete_partial_order.ωSup_total
{α : Type u}
[omega_complete_partial_order α]
{c : omega_complete_partial_order.chain α}
{x : α}
(h : ∀ (i : ℕ), ⇑c i ≤ x ∨ x ≤ ⇑c i) :
theorem
omega_complete_partial_order.ωSup_le_ωSup_of_le
{α : Type u}
[omega_complete_partial_order α]
{c₀ c₁ : omega_complete_partial_order.chain α}
(h : c₀ ≤ c₁) :
theorem
omega_complete_partial_order.ωSup_le_iff
{α : Type u}
[omega_complete_partial_order α]
(c : omega_complete_partial_order.chain α)
(x : α) :
def
omega_complete_partial_order.continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →ₘ β) :
Prop
A monotone function f : α →ₘ β is continuous if it distributes over ωSup.
In order to distinguish it from the (more commonly used) continuity from topology (see 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
def
omega_complete_partial_order.continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β) :
Prop
continuous' f asserts that f is both monotone and continuous.
Equations
- omega_complete_partial_order.continuous' f = ∃ (hf : monotone f), omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}
theorem
omega_complete_partial_order.continuous.to_monotone
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
{f : α → β}
(hf : omega_complete_partial_order.continuous' f) :
monotone f
theorem
omega_complete_partial_order.continuous.of_bundled
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β)
(hf : monotone f)
(hf' : omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}) :
theorem
omega_complete_partial_order.continuous.of_bundled'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →ₘ β)
(hf' : omega_complete_partial_order.continuous f) :
theorem
omega_complete_partial_order.continuous.to_bundled
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β)
(hf : omega_complete_partial_order.continuous' f) :
omega_complete_partial_order.continuous {to_fun := f, monotone' := _}
theorem
omega_complete_partial_order.continuous_comp
{α : Type u}
{β : Type v}
{γ : Type u_1}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : α →ₘ β)
(g : β →ₘ γ)
(hfc : omega_complete_partial_order.continuous f)
(hgc : omega_complete_partial_order.continuous g) :
theorem
omega_complete_partial_order.const_continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(x : β) :
theorem
roption.eq_of_chain
{α : Type u}
{c : omega_complete_partial_order.chain (roption α)}
{a b : α}
(ha : roption.some a ∈ c)
(hb : roption.some b ∈ c) :
a = b
The (noncomputable) ωSup definition for the ω-CPO structure on roption α.
Equations
- roption.ωSup c = dite (∃ (a : α), roption.some a ∈ c) (λ (h : ∃ (a : α), roption.some a ∈ c), roption.some (classical.some h)) (λ (h : ¬∃ (a : α), roption.some a ∈ c), roption.none)
theorem
roption.ωSup_eq_some
{α : Type u}
{c : omega_complete_partial_order.chain (roption α)}
{a : α}
(h : roption.some a ∈ c) :
theorem
roption.ωSup_eq_none
{α : Type u}
{c : omega_complete_partial_order.chain (roption α)}
(h : ¬∃ (a : α), roption.some a ∈ c) :
theorem
roption.mem_chain_of_mem_ωSup
{α : Type u}
{c : omega_complete_partial_order.chain (roption α)}
{a : α}
(h : a ∈ roption.ωSup c) :
roption.some a ∈ c
@[instance]
Equations
- roption.omega_complete_partial_order = {to_partial_order := order_bot.to_partial_order (roption α) roption.order_bot, ωSup := roption.ωSup α, le_ωSup := _, ωSup_le := _}
theorem
roption.mem_ωSup
{α : Type u}
(x : α)
(c : omega_complete_partial_order.chain (roption α)) :
x ∈ omega_complete_partial_order.ωSup c ↔ roption.some x ∈ c
@[simp]
theorem
pi.monotone_apply_to_fun
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), partial_order (β a)]
(a : α)
(f : Π (a : α), β a) :
⇑(pi.monotone_apply a) f = f a
def
pi.monotone_apply
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), partial_order (β a)]
(a : α) :
(Π (a : α), β a) →ₘ β a
Function application λ f, f a is monotone with respect to f for fixed a.
Equations
- pi.monotone_apply a = {to_fun := λ (f : Π (a : α), β a), f a, monotone' := _}
@[instance]
def
pi.omega_complete_partial_order
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), omega_complete_partial_order (β a)] :
omega_complete_partial_order (Π (a : α), β a)
Equations
- pi.omega_complete_partial_order = {to_partial_order := pi.partial_order (λ (i : α), omega_complete_partial_order.to_partial_order), ωSup := λ (c : omega_complete_partial_order.chain (Π (a : α), β a)) (a : α), omega_complete_partial_order.ωSup (c.map (pi.monotone_apply a)), le_ωSup := _, ωSup_le := _}
theorem
pi.omega_complete_partial_order.flip₁_continuous'
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (x : α), omega_complete_partial_order (β x)]
[omega_complete_partial_order γ]
(f : Π (x : α), γ → β x)
(a : α)
(hf : omega_complete_partial_order.continuous' (λ (x : γ) (y : α), f y x)) :
theorem
pi.omega_complete_partial_order.flip₂_continuous'
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (x : α), omega_complete_partial_order (β x)]
[omega_complete_partial_order γ]
(f : γ → Π (x : α), β x)
(hf : ∀ (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :
@[simp]
theorem
prod.ωSup_snd
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α × β)) :
@[simp]
theorem
prod.ωSup_fst
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α × β)) :
def
prod.ωSup
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α × β)) :
α × β
The supremum of a chain in the product ω-CPO.
@[simp]
theorem
prod.omega_complete_partial_order_ωSup_fst
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α × β)) :
@[simp]
theorem
prod.omega_complete_partial_order_ωSup_snd
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α × β)) :
@[instance]
def
prod.omega_complete_partial_order
{α : Type u_1}
{β : Type u_2}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
- prod.omega_complete_partial_order = {to_partial_order := prod.partial_order α β omega_complete_partial_order.to_partial_order, ωSup := prod.ωSup _inst_2, le_ωSup := _, ωSup_le := _}
@[instance]
Any complete lattice has an ω-CPO structure where the countable supremum is a special case
of arbitrary suprema.
Equations
- complete_lattice.omega_complete_partial_order α = {to_partial_order := order_bot.to_partial_order α (bounded_lattice.to_order_bot α), ωSup := λ (c : omega_complete_partial_order.chain α), ⨆ (i : ℕ), ⇑c i, le_ωSup := _, ωSup_le := _}
theorem
complete_lattice.inf_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
[is_total β has_le.le]
(f g : α →ₘ β)
(hf : omega_complete_partial_order.continuous f)
(hg : omega_complete_partial_order.continuous g) :
theorem
complete_lattice.Sup_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
(s : set (α →ₘ β))
(hs : ∀ (f : α →ₘ β), f ∈ s → omega_complete_partial_order.continuous f) :
theorem
complete_lattice.Sup_continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
(s : set (α → β))
(a : ∀ (t : α → β), t ∈ s → omega_complete_partial_order.continuous' t) :
theorem
complete_lattice.sup_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
{f g : α →ₘ β}
(hf : omega_complete_partial_order.continuous f)
(hg : omega_complete_partial_order.continuous g) :
theorem
complete_lattice.top_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β] :
theorem
complete_lattice.bot_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β] :
def
omega_complete_partial_order.preorder_hom.monotone_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(a : α) :
Function application λ f, f a (for fixed a) is a monotone function from the
monotone function space α →ₘ β to β.
@[simp]
theorem
omega_complete_partial_order.preorder_hom.monotone_apply_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(a : α)
(f : α →ₘ β) :
def
omega_complete_partial_order.preorder_hom.to_fun_hom
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
The "forgetful functor" from α →ₘ β to α → β that takes the underlying function,
is monotone.
def
omega_complete_partial_order.preorder_hom.ωSup
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →ₘ β)) :
α →ₘ β
The ωSup operator for monotone functions.
Equations
@[simp]
theorem
omega_complete_partial_order.preorder_hom.ωSup_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →ₘ β))
(a : α) :
@[simp]
theorem
omega_complete_partial_order.preorder_hom.omega_complete_partial_order_ωSup_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →ₘ β))
(a : α) :
@[instance]
def
omega_complete_partial_order.preorder_hom.omega_complete_partial_order
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
- omega_complete_partial_order.preorder_hom.omega_complete_partial_order = omega_complete_partial_order.lift omega_complete_partial_order.preorder_hom.to_fun_hom omega_complete_partial_order.preorder_hom.ωSup omega_complete_partial_order.preorder_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.preorder_hom.omega_complete_partial_order._proof_2
@[nolint]
def
omega_complete_partial_order.continuous_hom.to_preorder_hom
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(s : α →𝒄 β) :
α →ₘ β
structure
omega_complete_partial_order.continuous_hom
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Type (max u v)
- to_fun : α → β
- monotone' : monotone c.to_fun
- cont : omega_complete_partial_order.continuous {to_fun := c.to_fun, monotone' := _}
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 preorder_hom.continuous.
@[instance]
def
omega_complete_partial_order.has_coe_to_fun
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
has_coe_to_fun (α →𝒄 β)
Equations
- omega_complete_partial_order.has_coe_to_fun α β = {F := λ (_x : α →𝒄 β), α → β, coe := omega_complete_partial_order.continuous_hom.to_fun _inst_2}
@[instance]
def
omega_complete_partial_order.has_coe
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
@[instance]
def
omega_complete_partial_order.partial_order
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
partial_order (α →𝒄 β)
theorem
omega_complete_partial_order.continuous_hom.monotone
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →𝒄 β) :
theorem
omega_complete_partial_order.continuous_hom.ite_continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
{p : Prop}
[hp : decidable p]
(f g : α → β)
(hf : omega_complete_partial_order.continuous' f)
(hg : omega_complete_partial_order.continuous' g) :
omega_complete_partial_order.continuous' (λ (x : α), ite p (f x) (g x))
theorem
omega_complete_partial_order.continuous_hom.ωSup_bind
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(c : omega_complete_partial_order.chain α)
(f : α →ₘ roption β)
(g : α →ₘ β → roption γ) :
omega_complete_partial_order.ωSup (c.map (f.bind g)) = omega_complete_partial_order.ωSup (c.map f) >>= omega_complete_partial_order.ωSup (c.map g)
theorem
omega_complete_partial_order.continuous_hom.bind_continuous'
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α → roption β)
(g : α → β → roption γ)
(a : omega_complete_partial_order.continuous' f)
(a_1 : omega_complete_partial_order.continuous' g) :
omega_complete_partial_order.continuous' (λ (x : α), f x >>= g x)
theorem
omega_complete_partial_order.continuous_hom.map_continuous'
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : β → γ)
(g : α → roption β)
(hg : omega_complete_partial_order.continuous' g) :
omega_complete_partial_order.continuous' (λ (x : α), f <$> g x)
theorem
omega_complete_partial_order.continuous_hom.seq_continuous'
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α → roption (β → γ))
(g : α → roption β)
(hf : omega_complete_partial_order.continuous' f)
(hg : omega_complete_partial_order.continuous' g) :
omega_complete_partial_order.continuous' (λ (x : α), f x <*> g x)
theorem
omega_complete_partial_order.continuous_hom.continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(F : α →𝒄 β)
(C : omega_complete_partial_order.chain α) :
def
omega_complete_partial_order.continuous_hom.of_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β)
(g : α →𝒄 β)
(h : f = ⇑g) :
α →𝒄 β
Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.of_fun_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β)
(g : α →𝒄 β)
(h : f = ⇑g)
(a : α) :
⇑(omega_complete_partial_order.continuous_hom.of_fun f g h) a = f a
@[simp]
theorem
omega_complete_partial_order.continuous_hom.of_mono_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →ₘ β)
(h : ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f))
(a : α) :
def
omega_complete_partial_order.continuous_hom.of_mono
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →ₘ β)
(h : ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f)) :
α →𝒄 β
Construct a continuous function from a monotone function with a proof of continuity.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.id_to_fun
{α : Type u}
[omega_complete_partial_order α]
(a : α) :
def
omega_complete_partial_order.continuous_hom.id
{α : Type u}
[omega_complete_partial_order α] :
α →𝒄 α
The identity as a continuous function.
Equations
- omega_complete_partial_order.continuous_hom.id = omega_complete_partial_order.continuous_hom.of_mono preorder_hom.id omega_complete_partial_order.continuous_hom.id._proof_1
def
omega_complete_partial_order.continuous_hom.comp
{α : Type u}
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : β →𝒄 γ)
(g : α →𝒄 β) :
α →𝒄 γ
The composition of continuous functions.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.comp_to_fun
{α : Type u}
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : β →𝒄 γ)
(g : α →𝒄 β)
(a : α) :
@[ext]
theorem
omega_complete_partial_order.continuous_hom.ext
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f g : α →𝒄 β)
(h : ∀ (x : α), ⇑f x = ⇑g x) :
f = g
theorem
omega_complete_partial_order.continuous_hom.coe_inj
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f g : α →𝒄 β)
(h : ⇑f = ⇑g) :
f = g
@[simp]
theorem
omega_complete_partial_order.continuous_hom.comp_id
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : β →𝒄 γ) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.id_comp
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : β →𝒄 γ) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.comp_assoc
{α : Type u}
{β : Type v}
{γ : Type u_3}
{φ : Type u_4}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
[omega_complete_partial_order φ]
(f : γ →𝒄 φ)
(g : β →𝒄 γ)
(h : α →𝒄 β) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.coe_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(a : α)
(f : α →𝒄 β) :
def
omega_complete_partial_order.continuous_hom.const
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : β) :
α →𝒄 β
function.const is a continuous function.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.const_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : β)
(a : α) :
@[instance]
def
omega_complete_partial_order.continuous_hom.inhabited
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[inhabited β] :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.prod.apply_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : (α →𝒄 β) × α) :
def
omega_complete_partial_order.continuous_hom.prod.apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
The application of continuous functions as a monotone function.
(It would make sense to make it a continuous function, but we are currently constructing a
omega_complete_partial_order instance for α →𝒄 β, and we cannot use it as the domain or image
of a continuous function before we do.)
def
omega_complete_partial_order.continuous_hom.to_mono
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
The map from continuous functions to monotone functions is itself a monotone function.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.to_mono_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →𝒄 β) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.forall_forall_merge
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c₀ : omega_complete_partial_order.chain (α →𝒄 β))
(c₁ : omega_complete_partial_order.chain α)
(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
omega_complete_partial_order.continuous_hom.forall_forall_merge'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c₀ : omega_complete_partial_order.chain (α →𝒄 β))
(c₁ : omega_complete_partial_order.chain α)
(z : β) :
def
omega_complete_partial_order.continuous_hom.ωSup
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →𝒄 β)) :
α →𝒄 β
The ωSup operator for continuous functions, which takes the pointwise countable supremum
of the functions in the ω-chain.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.ωSup_to_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →𝒄 β))
(a : α) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.omega_complete_partial_order_ωSup
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →𝒄 β)) :
@[instance]
def
omega_complete_partial_order.continuous_hom.omega_complete_partial_order
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
- omega_complete_partial_order.continuous_hom.omega_complete_partial_order = omega_complete_partial_order.lift omega_complete_partial_order.continuous_hom.to_mono omega_complete_partial_order.continuous_hom.ωSup omega_complete_partial_order.continuous_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.continuous_hom.omega_complete_partial_order._proof_2
theorem
omega_complete_partial_order.continuous_hom.ωSup_def
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →𝒄 β))
(x : α) :
theorem
omega_complete_partial_order.continuous_hom.ωSup_ωSup
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c₀ : omega_complete_partial_order.chain (α →𝒄 β))
(c₁ : omega_complete_partial_order.chain α) :
def
omega_complete_partial_order.continuous_hom.flip
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
{α : Type u_1}
(f : α → β →𝒄 γ) :
β →𝒄 α → γ
A family of continuous functions yields a continuous family of functions.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.flip_to_fun
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
{α : Type u_1}
(f : α → β →𝒄 γ)
(x : β)
(y : α) :
⇑(omega_complete_partial_order.continuous_hom.flip f) x y = ⇑(f y) x
def
omega_complete_partial_order.continuous_hom.bind
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α →𝒄 roption β)
(g : α →𝒄 β → roption γ) :
roption.bind as a continuous function.
def
omega_complete_partial_order.continuous_hom.map
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 roption β) :
roption.map as a continuous function.
Equations
- omega_complete_partial_order.continuous_hom.map f g = omega_complete_partial_order.continuous_hom.of_fun (λ (x : α), f <$> ⇑g x) (g.bind (omega_complete_partial_order.continuous_hom.const (pure ∘ f))) _
@[simp]
theorem
omega_complete_partial_order.continuous_hom.map_to_fun
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 roption β)
(x : α) :
⇑(omega_complete_partial_order.continuous_hom.map f g) x = f <$> ⇑g x
def
omega_complete_partial_order.continuous_hom.seq
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α →𝒄 roption (β → γ))
(g : α →𝒄 roption β) :
roption.seq as a continuous function.
Equations
- f.seq g = omega_complete_partial_order.continuous_hom.of_fun (λ (x : α), ⇑f x <*> ⇑g x) (f.bind (omega_complete_partial_order.continuous_hom.flip (flip omega_complete_partial_order.continuous_hom.map g))) _