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,seqas continuous morphisms
Instances of OmegaCompletePartialOrder #
Part- every
CompleteLattice - pi-types
- product types
OrderHomContinuousHom(with notation →𝒄)- an instance of
OmegaCompletePartialOrder (α →𝒄 β)
- an instance of
ContinuousHom.ofFunContinuousHom.ofMono- continuous functions:
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]
A chain is a monotone sequence.
See the definition on page 114 of [gunter1992].
Equations
Instances For
instance
OmegaCompletePartialOrder.Chain.instOrderHomClassNat
{α : Type u_2}
[Preorder α]
:
OrderHomClass (Chain α) ℕ α
instance
OmegaCompletePartialOrder.Chain.instMembership
{α : Type u_2}
[Preorder α]
:
Membership α (Chain α)
Equations
@[simp]
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].
- ωSup : Chain α → α
The supremum of an increasing sequence
ωSupis an upper bound of the increasing sequenceωSupis a lower bound of the set of upper bounds of the increasing sequence
Instances
@[reducible, inline]
abbrev
OmegaCompletePartialOrder.lift
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[PartialOrder β]
(f : β →o α)
(ωSup₀ : Chain β → β)
(h : ∀ (x y : β), f x ≤ f y → x ≤ y)
(h' : ∀ (c : Chain β), f (ωSup₀ c) = ωSup (c.map f))
:
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
Instances For
theorem
OmegaCompletePartialOrder.le_ωSup_of_le
{α : Type u_2}
[OmegaCompletePartialOrder α]
{c : Chain α}
{x : α}
(i : ℕ)
(h : x ≤ c i)
:
theorem
OmegaCompletePartialOrder.ωSup_le_ωSup_of_le
{α : Type u_2}
[OmegaCompletePartialOrder α]
{c₀ c₁ : Chain α}
(h : c₀ ≤ c₁)
:
@[simp]
theorem
OmegaCompletePartialOrder.ωSup_le_iff
{α : Type u_2}
[OmegaCompletePartialOrder α]
{c : Chain α}
{x : α}
:
theorem
OmegaCompletePartialOrder.isLUB_range_ωSup
{α : Type u_2}
[OmegaCompletePartialOrder α]
(c : Chain α)
:
theorem
OmegaCompletePartialOrder.ωSup_eq_of_isLUB
{α : Type u_2}
[OmegaCompletePartialOrder α]
{c : Chain α}
{a : α}
(h : IsLUB (Set.range ⇑c) a)
:
def
OmegaCompletePartialOrder.subtype
{α : Type u_6}
[OmegaCompletePartialOrder α]
(p : α → Prop)
(hp : ∀ (c : Chain α), (∀ i ∈ c, p i) → p (ωSup c))
:
A subset p : α → Prop of the type closed under ωSup induces an
OmegaCompletePartialOrder on the subtype {a : α // p a}.
Equations
Instances For
def
OmegaCompletePartialOrder.ωScottContinuous
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α → β)
:
A function f between ω-complete partial orders is ωScottContinuous if it is
Scott continuous over chains.
Equations
Instances For
theorem
ScottContinuous.ωScottContinuous
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
(hf : ScottContinuous f)
:
theorem
OmegaCompletePartialOrder.ωScottContinuous.monotone
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
(h : ωScottContinuous f)
:
Monotone f
theorem
OmegaCompletePartialOrder.ωScottContinuous.isLUB
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
{c : Chain α}
(hf : ωScottContinuous f)
:
theorem
OmegaCompletePartialOrder.ωScottContinuous.id
{α : Type u_2}
[OmegaCompletePartialOrder α]
:
theorem
OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
(hf : ωScottContinuous f)
(c : Chain α)
:
theorem
OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
:
ωScottContinuous f asserts that f is both monotone and distributes over ωSup.
theorem
OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
:
Alias of the reverse direction of OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup.
ωScottContinuous f asserts that f is both monotone and distributes over ωSup.
theorem
OmegaCompletePartialOrder.ωScottContinuous.monotone_map_ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α → β}
:
Alias of the forward direction of OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup.
ωScottContinuous f asserts that f is both monotone and distributes over ωSup.
theorem
OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α →o β}
:
theorem
OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α →o β}
:
Alias of the reverse direction of OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom.
theorem
OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f : α →o β}
:
Alias of the forward direction of OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom.
theorem
OmegaCompletePartialOrder.ωScottContinuous.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
{f : α → β}
{g : β → γ}
(hg : ωScottContinuous g)
(hf : ωScottContinuous f)
:
ωScottContinuous (g ∘ f)
theorem
OmegaCompletePartialOrder.ωScottContinuous.const
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{x : β}
:
theorem
Part.eq_of_chain
{α : Type u_2}
{c : OmegaCompletePartialOrder.Chain (Part α)}
{a b : α}
(ha : some a ∈ c)
(hb : some b ∈ c)
:
theorem
Part.ωSup_eq_some
{α : Type u_2}
{c : OmegaCompletePartialOrder.Chain (Part α)}
{a : α}
(h : some a ∈ c)
:
theorem
Part.mem_chain_of_mem_ωSup
{α : Type u_2}
{c : OmegaCompletePartialOrder.Chain (Part α)}
{a : α}
(h : a ∈ Part.ωSup c)
:
Equations
instance
instOmegaCompletePartialOrderForall
{α : Type u_2}
{β : α → Type u_6}
[(a : α) → OmegaCompletePartialOrder (β a)]
:
OmegaCompletePartialOrder ((a : α) → β a)
Equations
theorem
OmegaCompletePartialOrder.ωScottContinuous.apply₂
{α : Type u_2}
{γ : Type u_4}
{β : α → Type u_6}
[(x : α) → OmegaCompletePartialOrder (β x)]
[OmegaCompletePartialOrder γ]
{f : γ → (x : α) → β x}
(hf : ωScottContinuous f)
(a : α)
:
ωScottContinuous fun (x : γ) => f x a
theorem
OmegaCompletePartialOrder.ωScottContinuous.of_apply₂
{α : Type u_2}
{γ : Type u_4}
{β : α → Type u_6}
[(x : α) → OmegaCompletePartialOrder (β x)]
[OmegaCompletePartialOrder γ]
{f : γ → (x : α) → β x}
(hf : ∀ (a : α), ωScottContinuous fun (x : γ) => f x a)
:
theorem
OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂
{α : Type u_2}
{γ : Type u_4}
{β : α → Type u_6}
[(x : α) → OmegaCompletePartialOrder (β x)]
[OmegaCompletePartialOrder γ]
{f : γ → (x : α) → β x}
:
def
Prod.ωSupImpl
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : OmegaCompletePartialOrder.Chain (α × β))
:
The supremum of a chain in the product ω-CPO.
Equations
Instances For
@[simp]
theorem
Prod.ωSupImpl_snd
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : OmegaCompletePartialOrder.Chain (α × β))
:
@[simp]
theorem
Prod.ωSupImpl_fst
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : OmegaCompletePartialOrder.Chain (α × β))
:
instance
Prod.instOmegaCompletePartialOrder
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
OmegaCompletePartialOrder (α × β)
Equations
@[simp]
theorem
Prod.ωSup_snd
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : OmegaCompletePartialOrder.Chain (α × β))
:
@[simp]
theorem
Prod.ωSup_fst
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : OmegaCompletePartialOrder.Chain (α × β))
:
theorem
Prod.ωSup_zip
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c₀ : OmegaCompletePartialOrder.Chain α)
(c₁ : OmegaCompletePartialOrder.Chain β)
:
@[instance 100]
Any complete lattice has an ω-CPO structure where the countable supremum is a special case
of arbitrary suprema.
Equations
theorem
CompleteLattice.ωScottContinuous.prodMk
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
{f g : α → β}
(hf : OmegaCompletePartialOrder.ωScottContinuous f)
(hg : OmegaCompletePartialOrder.ωScottContinuous g)
:
OmegaCompletePartialOrder.ωScottContinuous fun (x : α) => (f x, g x)
theorem
CompleteLattice.ωScottContinuous.iSup
{ι : Sort u_1}
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
{f : ι → α → β}
(hf : ∀ (i : ι), OmegaCompletePartialOrder.ωScottContinuous (f i))
:
OmegaCompletePartialOrder.ωScottContinuous (⨆ (i : ι), f i)
theorem
CompleteLattice.ωScottContinuous.sSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
{s : Set (α → β)}
(hs : ∀ f ∈ s, OmegaCompletePartialOrder.ωScottContinuous f)
:
theorem
CompleteLattice.ωScottContinuous.sup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
{f g : α → β}
(hf : OmegaCompletePartialOrder.ωScottContinuous f)
(hg : OmegaCompletePartialOrder.ωScottContinuous g)
:
theorem
CompleteLattice.ωScottContinuous.top
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
:
theorem
CompleteLattice.ωScottContinuous.bot
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLattice β]
:
theorem
CompleteLattice.ωScottContinuous.inf
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[CompleteLinearOrder β]
{f g : α → β}
(hf : OmegaCompletePartialOrder.ωScottContinuous f)
(hg : OmegaCompletePartialOrder.ωScottContinuous g)
:
def
OmegaCompletePartialOrder.OrderHom.ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →o β))
:
The ωSup operator for monotone functions.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.OrderHom.ωSup_coe
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →o β))
(a : α)
:
instance
OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
OmegaCompletePartialOrder (α →o β)
Equations
@[simp]
theorem
OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →o β))
(a : α)
:
structure
OmegaCompletePartialOrder.ContinuousHom
(α : Type u_2)
(β : Type u_3)
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
extends α →o β :
Type (max u_2 u_3)
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.
- toFun : α → β
The underlying function of a
ContinuousHomis continuous, i.e. it preservesωSup
Instances For
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
Instances For
instance
OmegaCompletePartialOrder.instFunLikeContinuousHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
Equations
instance
OmegaCompletePartialOrder.instOrderHomClassContinuousHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
OrderHomClass (α →𝒄 β) α β
instance
OmegaCompletePartialOrder.instPartialOrderContinuousHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
PartialOrder (α →𝒄 β)
Equations
theorem
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
:
def
OmegaCompletePartialOrder.ContinuousHom.Simps.apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(h : α →𝒄 β)
:
α → β
See Note [custom simps projection]. We specify this explicitly because we don't have a DFunLike instance.
Equations
Instances For
theorem
OmegaCompletePartialOrder.ContinuousHom.congr_fun
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f g : α →𝒄 β}
(h : f = g)
(x : α)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.congr_arg
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
{x y : α}
(h : x = y)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.monotone
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
:
Monotone ⇑f
theorem
OmegaCompletePartialOrder.ContinuousHom.apply_mono
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f g : α →𝒄 β}
{x y : α}
(h₁ : f ≤ g)
(h₂ : x ≤ y)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
{α : Type u_2}
[OmegaCompletePartialOrder α]
{β γ : Type u_6}
{f : α → Part β}
{g : α → β → Part γ}
(hf : ωScottContinuous f)
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : α) => f x >>= g x
theorem
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map
{α : Type u_2}
[OmegaCompletePartialOrder α]
{β γ : Type u_6}
{f : β → γ}
{g : α → Part β}
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : α) => f <$> g x
theorem
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.seq
{α : Type u_2}
[OmegaCompletePartialOrder α]
{β γ : Type u_6}
{f : α → Part (β → γ)}
{g : α → Part β}
(hf : ωScottContinuous f)
(hg : ωScottContinuous g)
:
ωScottContinuous fun (x : α) => f x <*> g x
theorem
OmegaCompletePartialOrder.ContinuousHom.continuous
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(F : α →𝒄 β)
(C : Chain α)
:
def
OmegaCompletePartialOrder.ContinuousHom.copy
{α : Type u_2}
{β : Type u_3}
[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
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.copy_apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α → β)
(g : α →𝒄 β)
(h : f = ⇑g)
(a✝ : α)
:
The identity as a continuous function.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.id_apply
{α : Type u_2}
[OmegaCompletePartialOrder α]
(a : α)
:
def
OmegaCompletePartialOrder.ContinuousHom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
(f : β →𝒄 γ)
(g : α →𝒄 β)
:
The composition of continuous functions.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
(f : β →𝒄 γ)
(g : α →𝒄 β)
(a✝ : α)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.ext
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f g : α →𝒄 β)
(h : ∀ (x : α), f x = g x)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.ext_iff
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
{f g : α →𝒄 β}
:
theorem
OmegaCompletePartialOrder.ContinuousHom.coe_inj
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f g : α →𝒄 β)
(h : ⇑f = ⇑g)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.comp_id
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
(f : β →𝒄 γ)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.id_comp
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
(f : β →𝒄 γ)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
[OmegaCompletePartialOrder δ]
(f : γ →𝒄 δ)
(g : β →𝒄 γ)
(h : α →𝒄 β)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.coe_apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(a : α)
(f : α →𝒄 β)
:
def
OmegaCompletePartialOrder.ContinuousHom.const
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(x : β)
:
Function.const is a continuous function.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.const_apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(x : β)
(a✝ : α)
:
instance
OmegaCompletePartialOrder.ContinuousHom.instInhabited
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
[Inhabited β]
:
Equations
def
OmegaCompletePartialOrder.ContinuousHom.toMono
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
The map from continuous functions to monotone functions is itself a monotone function.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.toMono_coe
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : α →𝒄 β)
:
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c₀ : Chain (α →𝒄 β))
(c₁ : 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
OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge'
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c₀ : Chain (α →𝒄 β))
(c₁ : Chain α)
(z : β)
:
def
OmegaCompletePartialOrder.ContinuousHom.ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →𝒄 β))
:
The ωSup operator for continuous functions, which takes the pointwise countable supremum
of the functions in the ω-chain.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.ωSup_apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →𝒄 β))
(a : α)
:
instance
OmegaCompletePartialOrder.ContinuousHom.inst
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
OmegaCompletePartialOrder (α →𝒄 β)
Equations
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.ωSup_def
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c : Chain (α →𝒄 β))
:
def
OmegaCompletePartialOrder.ContinuousHom.Prod.apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
:
The application of continuous functions as a continuous function.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(f : (α →𝒄 β) × α)
:
theorem
OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup
{α : Type u_2}
{β : Type u_3}
[OmegaCompletePartialOrder α]
[OmegaCompletePartialOrder β]
(c₀ : Chain (α →𝒄 β))
(c₁ : Chain α)
:
def
OmegaCompletePartialOrder.ContinuousHom.flip
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
{α : Type u_6}
(f : α → β →𝒄 γ)
:
A family of continuous functions yields a continuous family of functions.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.flip_apply
{β : Type u_3}
{γ : Type u_4}
[OmegaCompletePartialOrder β]
[OmegaCompletePartialOrder γ]
{α : Type u_6}
(f : α → β →𝒄 γ)
(x : β)
(y : α)
:
noncomputable def
OmegaCompletePartialOrder.ContinuousHom.map
{α : Type u_2}
[OmegaCompletePartialOrder α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 Part β)
:
Part.map as a continuous function.
Equations
Instances For
@[simp]
theorem
OmegaCompletePartialOrder.ContinuousHom.map_apply
{α : Type u_2}
[OmegaCompletePartialOrder α]
{β γ : Type v}
(f : β → γ)
(g : α →𝒄 Part β)
(x : α)
:
def
OmegaCompletePartialOrder.fixedPoints.iterateChain
{α : Type u_2}
[OmegaCompletePartialOrder α]
(f : α →o α)
(x : α)
(h : x ≤ f x)
:
Chain α
Iteration of a function on an initial element interpreted as a chain.
Equations
Instances For
theorem
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint
{α : Type u_2}
[OmegaCompletePartialOrder α]
(f : α →𝒄 α)
(x : α)
(h : x ≤ f x)
:
The supremum of iterating a function on x arbitrary often is a fixed point
theorem
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint
{α : Type u_2}
[OmegaCompletePartialOrder α]
(f : α →𝒄 α)
(x : α)
(h : x ≤ f x)
{a : α}
(h_a : f a ≤ a)
(h_x_le_a : x ≤ a)
:
The supremum of iterating a function on x arbitrary often is smaller than any prefixed point.
A prefixed point is a value a with f a ≤ a.
theorem
OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_fixedPoint
{α : Type u_2}
[OmegaCompletePartialOrder α]
(f : α →𝒄 α)
(x : α)
(h : x ≤ f x)
{a : α}
(h_a : a ∈ Function.fixedPoints ⇑f)
(h_x_le_a : x ≤ a)
:
The supremum of iterating a function on x arbitrary often is smaller than any fixed point.