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 #
part- 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:
References #
@[protected, instance]
def
omega_complete_partial_order.chain.has_coe_to_fun
{α : Type u}
[preorder α] :
has_coe_to_fun (omega_complete_partial_order.chain α) (λ (_x : omega_complete_partial_order.chain α), ℕ → α)
@[protected, instance]
@[protected, instance]
@[protected, 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 : α →o β) :
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 : α →o β}
(x : α) :
@[simp]
theorem
omega_complete_partial_order.chain.map_id
{α : Type u}
[preorder α]
(c : omega_complete_partial_order.chain α) :
c.map order_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 : α →o β}
(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₁ = order_hom.prod c₀ c₁
@[simp]
theorem
omega_complete_partial_order.chain.zip_coe
{α : Type u}
{β : Type v}
[preorder α]
[preorder β]
(c₀ : omega_complete_partial_order.chain α)
(c₁ : omega_complete_partial_order.chain β)
(x : ℕ) :
@[class]
- to_partial_order : partial_order α
- ωSup : omega_complete_partial_order.chain α → α
- le_ωSup : ∀ (c : omega_complete_partial_order.chain α) (i : ℕ), ⇑c i ≤ omega_complete_partial_order.ωSup c
- ωSup_le : ∀ (c : omega_complete_partial_order.chain α) (x : α), (∀ (i : ℕ), ⇑c i ≤ x) → omega_complete_partial_order.ωSup c ≤ 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 [Gun92].
@[protected]
def
omega_complete_partial_order.lift
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[partial_order β]
(f : β →o α)
(ω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 : β →o α, 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.subtype
{α : Type u_1}
[omega_complete_partial_order α]
(p : α → Prop)
(hp : ∀ (c : omega_complete_partial_order.chain α), (∀ (i : α), i ∈ c → p i) → p (omega_complete_partial_order.ωSup c)) :
A subset p : α → Prop of the type closed under ωSup induces an
omega_complete_partial_order on the subtype {a : α // p a}.
Equations
- omega_complete_partial_order.subtype p hp = omega_complete_partial_order.lift (order_hom.subtype.val p) (λ (c : omega_complete_partial_order.chain (subtype p)), ⟨omega_complete_partial_order.ωSup (c.map (order_hom.subtype.val p)), _⟩) _ _
def
omega_complete_partial_order.continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(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 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 : α →o β)
(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' := _}
@[simp, norm_cast]
theorem
omega_complete_partial_order.continuous'_coe
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
{f : α →o β} :
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 : α →o β)
(g : β →o γ)
(hfc : omega_complete_partial_order.continuous f)
(hgc : omega_complete_partial_order.continuous g) :
theorem
omega_complete_partial_order.continuous_const
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(x : β) :
theorem
omega_complete_partial_order.const_continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(x : β) :
theorem
part.eq_of_chain
{α : Type u}
{c : omega_complete_partial_order.chain (part α)}
{a b : α}
(ha : part.some a ∈ c)
(hb : part.some b ∈ c) :
a = b
@[protected]
The (noncomputable) ωSup definition for the ω-CPO structure on part α.
theorem
part.ωSup_eq_some
{α : Type u}
{c : omega_complete_partial_order.chain (part α)}
{a : α}
(h : part.some a ∈ c) :
theorem
part.ωSup_eq_none
{α : Type u}
{c : omega_complete_partial_order.chain (part α)}
(h : ¬∃ (a : α), part.some a ∈ c) :
theorem
part.mem_chain_of_mem_ωSup
{α : Type u}
{c : omega_complete_partial_order.chain (part α)}
{a : α}
(h : a ∈ part.ωSup c) :
@[protected, instance]
Equations
- part.omega_complete_partial_order = {to_partial_order := part.partial_order α, ωSup := part.ωSup α, le_ωSup := _, ωSup_le := _}
theorem
part.mem_ωSup
{α : Type u}
(x : α)
(c : omega_complete_partial_order.chain (part α)) :
x ∈ omega_complete_partial_order.ωSup c ↔ part.some x ∈ c
@[protected, 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.eval_order_hom 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 (α × β)) :
@[protected]
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.
Equations
@[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 (α × β)) :
@[protected, 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 := _}
@[protected, 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 := complete_semilattice_Inf.to_partial_order α (complete_lattice.to_complete_semilattice_Inf α), ω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 : α →o β)
(hf : omega_complete_partial_order.continuous f)
(hg : omega_complete_partial_order.continuous g) :
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 (α →o β))
(hs : ∀ (f : α →o β), f ∈ s → omega_complete_partial_order.continuous f) :
theorem
complete_lattice.supr_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
{ι : Sort u_1}
{f : ι → α →o β}
(h : ∀ (i : ι), omega_complete_partial_order.continuous (f i)) :
omega_complete_partial_order.continuous (⨆ (i : ι), f i)
theorem
complete_lattice.Sup_continuous'
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
(s : set (α → β))
(hc : ∀ (f : α → β), f ∈ s → omega_complete_partial_order.continuous' f) :
theorem
complete_lattice.sup_continuous
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[complete_lattice β]
{f g : α →o β}
(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 β] :
@[protected]
def
omega_complete_partial_order.order_hom.ωSup
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →o β)) :
α →o β
The ωSup operator for monotone functions.
Equations
- omega_complete_partial_order.order_hom.ωSup c = {to_fun := λ (a : α), omega_complete_partial_order.ωSup (c.map (order_hom.apply a)), monotone' := _}
@[simp]
theorem
omega_complete_partial_order.order_hom.ωSup_coe
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →o β))
(a : α) :
@[simp]
theorem
omega_complete_partial_order.order_hom.omega_complete_partial_order_ωSup_coe
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →o β))
(a : α) :
@[protected, instance]
def
omega_complete_partial_order.order_hom.omega_complete_partial_order
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
- omega_complete_partial_order.order_hom.omega_complete_partial_order = omega_complete_partial_order.lift order_hom.coe_fn_hom omega_complete_partial_order.order_hom.ωSup omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_2
structure
omega_complete_partial_order.continuous_hom
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Type (max u v)
- to_order_hom : α →o β
- cont : omega_complete_partial_order.continuous {to_fun := self.to_order_hom.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 order_hom.continuous.
@[protected, instance]
def
omega_complete_partial_order.continuous_hom.has_coe_to_fun
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
has_coe_to_fun (α →𝒄 β) (λ (_x : α →𝒄 β), α → β)
Equations
- omega_complete_partial_order.continuous_hom.has_coe_to_fun α β = {coe := λ (f : α →𝒄 β), f.to_order_hom.to_fun}
@[protected, instance]
def
omega_complete_partial_order.order_hom.has_coe
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
Equations
@[protected, instance]
def
omega_complete_partial_order.continuous_hom.partial_order
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β] :
partial_order (α →𝒄 β)
Equations
- omega_complete_partial_order.continuous_hom.partial_order α β = partial_order.lift (λ (f : α →𝒄 β), f.to_order_hom.to_fun) _
def
omega_complete_partial_order.continuous_hom.simps.apply
(α : Type u)
(β : Type v)
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(h : α →𝒄 β) :
α → β
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
theorem
omega_complete_partial_order.continuous_hom.congr_fun
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
{f g : α →𝒄 β}
(h : f = g)
(x : α) :
theorem
omega_complete_partial_order.continuous_hom.congr_arg
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →𝒄 β)
{x y : α}
(h : x = y) :
@[protected]
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.apply_mono
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
{f g : α →𝒄 β}
{x y : α}
(h₁ : f ≤ g)
(h₂ : x ≤ y) :
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 : α →o part β)
(g : α →o β → part γ) :
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 : α → part β)
(g : α → β → part γ) :
omega_complete_partial_order.continuous' f → 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 : α → part β)
(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 : α → part (β → γ))
(g : α → part β)
(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.
Equations
- omega_complete_partial_order.continuous_hom.of_fun f g h = {to_order_hom := {to_fun := f, monotone' := _}, cont := _}
@[simp]
theorem
omega_complete_partial_order.continuous_hom.of_fun_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α → β)
(g : α →𝒄 β)
(h : f = ⇑g)
(ᾰ : α) :
⇑(omega_complete_partial_order.continuous_hom.of_fun f g h) ᾰ = f ᾰ
def
omega_complete_partial_order.continuous_hom.of_mono
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →o β)
(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.
Equations
- omega_complete_partial_order.continuous_hom.of_mono f h = {to_order_hom := {to_fun := ⇑f, monotone' := _}, cont := h}
@[simp]
theorem
omega_complete_partial_order.continuous_hom.of_mono_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(f : α →o β)
(h : ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f))
(ᾰ : α) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.id_apply
{α : Type u}
[omega_complete_partial_order α]
(ᾰ : α) :
def
omega_complete_partial_order.continuous_hom.id
{α : Type u}
[omega_complete_partial_order α] :
α →𝒄 α
The identity as a continuous function.
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_apply
{α : Type u}
{β : Type v}
{γ : Type u_3}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
[omega_complete_partial_order γ]
(f : β →𝒄 γ)
(g : α →𝒄 β)
(ᾰ : α) :
@[protected, 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
@[protected]
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 β]
(x : β) :
α →𝒄 β
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 : α) :
@[protected, 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_coe
{α : 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_coe
{α : 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 : β) :
@[protected]
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_apply
{α : Type u}
{β : Type v}
[omega_complete_partial_order α]
[omega_complete_partial_order β]
(c : omega_complete_partial_order.chain (α →𝒄 β))
(ᾰ : α) :
@[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 (α →𝒄 β)) :
@[protected, 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 α) :
@[simp]
theorem
omega_complete_partial_order.continuous_hom.flip_apply
{β : 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.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.
Equations
- omega_complete_partial_order.continuous_hom.flip f = {to_order_hom := {to_fun := λ (x : β) (y : α), ⇑(f y) x, monotone' := _}, cont := _}
noncomputable
def
omega_complete_partial_order.continuous_hom.bind
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α →𝒄 part β)
(g : α →𝒄 β → part γ) :
part.bind as a continuous function.
@[simp]
theorem
omega_complete_partial_order.continuous_hom.map_apply
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 part β)
(x : α) :
⇑(omega_complete_partial_order.continuous_hom.map f g) x = f <$> ⇑g x
noncomputable
def
omega_complete_partial_order.continuous_hom.map
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 part β) :
part.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))) _
noncomputable
def
omega_complete_partial_order.continuous_hom.seq
{α : Type u}
[omega_complete_partial_order α]
{β γ : Type v}
(f : α →𝒄 part (β → γ))
(g : α →𝒄 part β) :
part.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))) _