# 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} [] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o βPart γ) (x : α) :
(f.bind g) x = f x >>= g x
def OrderHom.bind {α : Type u_1} [] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o βPart γ) :
α →o Part γ

Part.bind as a monotone function

Equations
• f.bind g = { toFun := fun (x : α) => f x >>= g x, monotone' := }
Instances For

A chain is a monotone sequence.

See the definition on page 114 of [gunter1992].

Equations
Instances For
Equations
instance OmegaCompletePartialOrder.Chain.instCoeFunForallNat {α : Type u} [] :
CoeFun fun (x : ) => α
Equations
• OmegaCompletePartialOrder.Chain.instCoeFunForallNat = { coe := DFunLike.coe }
Equations
• OmegaCompletePartialOrder.Chain.instInhabited = { default := { toFun := default, monotone' := } }
Equations
• OmegaCompletePartialOrder.Chain.instMembership = { mem := fun (a : α) (c : →o α) => ∃ (i : ), a = c i }
Equations
• OmegaCompletePartialOrder.Chain.instLE = { le := fun (x y : ) => ∀ (i : ), ∃ (j : ), x i y j }
theorem OmegaCompletePartialOrder.Chain.isChain_range {α : Type u} [] :
IsChain (fun (x x_1 : α) => x x_1) ()
theorem OmegaCompletePartialOrder.Chain.directed {α : Type u} [] :
Directed (fun (x x_1 : α) => x x_1) c
def OmegaCompletePartialOrder.Chain.map {α : Type u} {β : Type v} [] [] (f : α →o β) :

map function for Chain

Equations
• c.map f = f.comp c
Instances For
@[simp]
theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u} {β : Type v} [] [] (f : α →o β) :
(c.map f) = f c
theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u} {β : Type v} [] [] {f : α →o β} (x : α) :
x cf x c.map f
theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u} {β : Type v} [] [] {f : α →o β} {b : β} :
b c.map fac, f a = b
@[simp]
theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u} {β : Type v} [] [] {f : α →o β} {b : β} :
b c.map f ac, f a = b
@[simp]
theorem OmegaCompletePartialOrder.Chain.map_id {α : Type u} [] :
c.map OrderHom.id = c
theorem OmegaCompletePartialOrder.Chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [] [] [] {f : α →o β} (g : β →o γ) :
(c.map f).map g = c.map (g.comp f)
theorem OmegaCompletePartialOrder.Chain.map_le_map {α : Type u} {β : Type v} [] [] {f : α →o β} {g : α →o β} (h : f g) :
c.map f c.map g
def OmegaCompletePartialOrder.Chain.zip {α : Type u} {β : Type v} [] [] (c₀ : ) (c₁ : ) :

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

Equations
Instances For
@[simp]
theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u} {β : Type v} [] [] (c₀ : ) (c₁ : ) (n : ) :
(c₀.zip c₁) n = (c₀ n, c₁ n)
class OmegaCompletePartialOrder (α : Type u_1) extends :
Type u_1

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].

• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• ωSup :

The supremum of an increasing sequence

• le_ωSup : ∀ (c : ) (i : ),

ωSup is an upper bound of the increasing sequence

• ωSup_le : ∀ (c : ) (x : α), (∀ (i : ), c i x)

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

Instances
theorem OmegaCompletePartialOrder.le_ωSup {α : Type u_1} [self : ] (i : ) :

ωSup is an upper bound of the increasing sequence

theorem OmegaCompletePartialOrder.ωSup_le {α : Type u_1} [self : ] (x : α) :
(∀ (i : ), c i x)

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

@[reducible, inline]
abbrev OmegaCompletePartialOrder.lift {α : Type u} {β : Type v} [] (f : β →o α) (ωSup₀ : ) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : ), f (ωSup₀ c) = OmegaCompletePartialOrder.ω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} {x : α} (i : ) (h : x c i) :
theorem OmegaCompletePartialOrder.ωSup_total {α : Type u} {x : α} (h : ∀ (i : ), c i x x c i) :
theorem OmegaCompletePartialOrder.ωSup_le_ωSup_of_le {α : Type u} {c₀ : } {c₁ : } (h : c₀ c₁) :
theorem OmegaCompletePartialOrder.ωSup_le_iff {α : Type u} (x : α) :
∀ (i : ), c i x
theorem OmegaCompletePartialOrder.ωSup_eq_of_isLUB {α : Type u} {a : α} (h : IsLUB () a) :
def OmegaCompletePartialOrder.subtype {α : Type u_2} (p : αProp) (hp : ∀ (c : ), (ic, p i)) :

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.
Instances For
def OmegaCompletePartialOrder.Continuous {α : Type u} {β : Type v} (f : α →o β) :

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
Instances For
def OmegaCompletePartialOrder.Continuous' {α : Type u} {β : Type v} (f : αβ) :

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

Equations
Instances For
theorem OmegaCompletePartialOrder.isLUB_of_scottContinuous {α : Type u} {β : Type v} {f : αβ} (hf : ) :
IsLUB (Set.range (c.map { toFun := f, monotone' := })) ()
theorem OmegaCompletePartialOrder.ScottContinuous.continuous' {α : Type u} {β : Type v} {f : αβ} (hf : ) :
theorem OmegaCompletePartialOrder.Continuous'.to_monotone {α : Type u} {β : Type v} {f : αβ} :
theorem OmegaCompletePartialOrder.Continuous.of_bundled {α : Type u} {β : Type v} (f : αβ) (hf : ) (hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }) :
theorem OmegaCompletePartialOrder.Continuous.of_bundled' {α : Type u} {β : Type v} (f : α →o β) (hf' : ) :
theorem OmegaCompletePartialOrder.Continuous'.to_bundled {α : Type u} {β : Type v} (f : αβ) :
OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := }
@[simp]
theorem OmegaCompletePartialOrder.continuous'_coe {α : Type u} {β : Type v} {f : α →o β} :
theorem OmegaCompletePartialOrder.continuous_comp {α : Type u} {β : Type v} {γ : Type u_1} (f : α →o β) (g : β →o γ) (hfc : ) (hgc : ) :
theorem OmegaCompletePartialOrder.continuous_const {α : Type u} {β : Type v} (x : β) :
theorem OmegaCompletePartialOrder.const_continuous' {α : Type u} {β : Type v} (x : β) :
theorem Part.eq_of_chain {α : Type u} {c : } {a : α} {b : α} (ha : c) (hb : c) :
a = b
noncomputable def Part.ωSup {α : Type u} (c : ) :
Part α

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

Equations
• = if h : ∃ (a : α), c then else Part.none
Instances For
theorem Part.ωSup_eq_some {α : Type u} {c : } {a : α} (h : c) :
theorem Part.ωSup_eq_none {α : Type u} {c : } (h : ¬∃ (a : α), c) :
= Part.none
theorem Part.mem_chain_of_mem_ωSup {α : Type u} {c : } {a : α} (h : a ) :
c
noncomputable instance Part.omegaCompletePartialOrder {α : Type u} :
Equations
theorem Part.mem_ωSup {α : Type u} (x : α) (c : ) :
instance Pi.instOmegaCompletePartialOrderForall {α : Type u_1} {β : αType u_2} [(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 : α) → ] (f : (x : α) → γβ x) (a : α) (hf : OmegaCompletePartialOrder.Continuous' fun (x : γ) (y : α) => f y x) :
theorem Pi.OmegaCompletePartialOrder.flip₂_continuous' {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(x : α) → ] (f : γ(x : α) → β x) (hf : ∀ (x : α), OmegaCompletePartialOrder.Continuous' fun (g : γ) => f g x) :
@[simp]
theorem Prod.ωSup_fst {α : Type u_1} {β : Type u_2} (c : ) :
().1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
@[simp]
theorem Prod.ωSup_snd {α : Type u_1} {β : Type u_2} (c : ) :
().2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
def Prod.ωSup {α : Type u_1} {β : Type u_2} (c : ) :
α × β

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

Equations
Instances For
@[simp]
theorem Prod.instOmegaCompletePartialOrder_ωSup_fst {α : Type u_1} {β : Type u_2} (c : ) :
= OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
@[simp]
theorem Prod.instOmegaCompletePartialOrder_ωSup_snd {α : Type u_1} {β : Type u_2} (c : ) :
= OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)
instance Prod.instOmegaCompletePartialOrder {α : Type u_1} {β : Type u_2} :
Equations
theorem Prod.ωSup_zip {α : Type u_1} {β : Type u_2} (c₀ : ) (c₁ : ) :
@[instance 100]

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

Equations
theorem CompleteLattice.sSup_continuous {α : Type u} {β : Type v} [] (s : Set (α →o β)) (hs : ) :
theorem CompleteLattice.iSup_continuous {α : Type u} {β : Type v} [] {ι : Sort u_1} {f : ια →o β} (h : ∀ (i : ι), ) :
theorem CompleteLattice.sSup_continuous' {α : Type u} {β : Type v} [] (s : Set (αβ)) (hc : ) :
theorem CompleteLattice.sup_continuous {α : Type u} {β : Type v} [] {f : α →o β} {g : α →o β} :
theorem CompleteLattice.top_continuous {α : Type u} {β : Type v} [] :
theorem CompleteLattice.bot_continuous {α : Type u} {β : Type v} [] :
theorem CompleteLattice.inf_continuous {α : Type u_1} {β : Type u_2} (f : α →o β) (g : α →o β) :
theorem CompleteLattice.inf_continuous' {α : Type u_1} {β : Type u_2} {f : αβ} {g : αβ} :
@[simp]
theorem OmegaCompletePartialOrder.OrderHom.ωSup_coe {α : Type u} {β : Type v} (c : ) (a : α) :
def OmegaCompletePartialOrder.OrderHom.ωSup {α : Type u} {β : Type v} (c : ) :
α →o β

The ωSup operator for monotone functions.

Equations
Instances For
Equations
• OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder = OmegaCompletePartialOrder.lift OrderHom.coeFnHom OmegaCompletePartialOrder.OrderHom.ωSup
structure OmegaCompletePartialOrder.ContinuousHom (α : Type u) (β : Type v) extends :
Type (max u v)

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.

Instances For

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = { coe := fun (f : α →𝒄 β) => f.toFun, coe_injective' := }
Equations
• =
Equations
theorem OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe {α : Type u} {β : Type v} (f : α →𝒄 β) :
f.toOrderHom = f
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk {α : Type u} {β : Type v} (f : α →o β) :
{ toOrderHom := f, cont := hf } = f
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom {α : Type u} {β : Type v} (f : α →𝒄 β) :
f.toOrderHom = f
def OmegaCompletePartialOrder.ContinuousHom.Simps.apply {α : Type u} {β : Type v} (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} {β : Type v} {f : α →𝒄 β} {g : α →𝒄 β} (h : f = g) (x : α) :
f x = g x
theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u} {β : Type v} (f : α →𝒄 β) {x : α} {y : α} (h : x = y) :
f x = f y
theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono {α : Type u} {β : Type v} {f : α →𝒄 β} {g : α →𝒄 β} {x : α} {y : α} (h₁ : f g) (h₂ : x y) :
f x g y
theorem OmegaCompletePartialOrder.ContinuousHom.ite_continuous' {α : Type u} {β : Type v} {p : Prop} [hp : ] (f : αβ) (g : αβ) :
OmegaCompletePartialOrder.Continuous' fun (x : α) => if p then f x else g x
theorem OmegaCompletePartialOrder.ContinuousHom.bind_continuous' {α : Type u} {β : Type v} {γ : Type v} (f : αPart β) (g : αβPart γ) :
OmegaCompletePartialOrder.Continuous' fun (x : α) => f x >>= g x
theorem OmegaCompletePartialOrder.ContinuousHom.map_continuous' {α : Type u} {β : Type v} {γ : Type v} (f : βγ) (g : αPart β) :
theorem OmegaCompletePartialOrder.ContinuousHom.seq_continuous' {α : Type u} {β : Type v} {γ : Type v} (f : αPart (βγ)) (g : αPart β) :
OmegaCompletePartialOrder.Continuous' fun (x : α) => Seq.seq (f x) fun (x_1 : Unit) => g x
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.copy_apply {α : Type u} {β : Type v} (f : αβ) (g : α →𝒄 β) (h : f = g) :
∀ (a : α), = f a
def OmegaCompletePartialOrder.ContinuousHom.copy {α : Type u} {β : Type v} (f : αβ) (g : α →𝒄 β) (h : f = g) :
α →𝒄 β

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

Equations
• = { toOrderHom := g.copy f h, cont := }
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.id_apply {α : Type u} (a : α) :
OmegaCompletePartialOrder.ContinuousHom.id a = a

The identity as a continuous function.

Equations
• OmegaCompletePartialOrder.ContinuousHom.id = { toOrderHom := OrderHom.id, cont := }
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) (g : α →𝒄 β) :
∀ (a : α), (f.comp g) a = f (g a)
def OmegaCompletePartialOrder.ContinuousHom.comp {α : Type u} {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) (g : α →𝒄 β) :
α →𝒄 γ

The composition of continuous functions.

Equations
• f.comp g = { toOrderHom := f.comp g.toOrderHom, cont := }
Instances For
theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u} {β : Type v} (f : α →𝒄 β) (g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
f = g
theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u} {β : Type v} (f : α →𝒄 β) (g : α →𝒄 β) (h : f = g) :
f = g
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.comp_id {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) :
f.comp OmegaCompletePartialOrder.ContinuousHom.id = f
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type v} {γ : Type u_3} (f : β →𝒄 γ) :
OmegaCompletePartialOrder.ContinuousHom.id.comp f = f
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :
f.comp (g.comp h) = (f.comp g).comp h
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply {α : Type u} {β : Type v} (a : α) (f : α →𝒄 β) :
f a = f a
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.const_apply {α : Type u} {β : Type v} (x : β) :
∀ (a : α),
def OmegaCompletePartialOrder.ContinuousHom.const {α : Type u} {β : Type v} (x : β) :
α →𝒄 β

Function.const is a continuous function.

Equations
• = { toOrderHom := () x, cont := }
Instances For
Equations
• OmegaCompletePartialOrder.ContinuousHom.instInhabited = { default := }
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.toMono_coe {α : Type u} {β : Type v} (f : α →𝒄 β) :
OmegaCompletePartialOrder.ContinuousHom.toMono f = f

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

Equations
• OmegaCompletePartialOrder.ContinuousHom.toMono = { toFun := fun (f : α →𝒄 β) => f, monotone' := }
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u} {β : Type v} (c₀ : ) (c₁ : ) (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} (c₀ : ) (c₁ : ) (z : β) :
(∀ (j i : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply {α : Type u} {β : Type v} (c : ) (a : α) :
= OmegaCompletePartialOrder.ωSup ((c.map OmegaCompletePartialOrder.ContinuousHom.toMono).map ())

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

Equations
Instances For
@[simp]
Equations
• OmegaCompletePartialOrder.ContinuousHom.inst = OmegaCompletePartialOrder.lift OmegaCompletePartialOrder.ContinuousHom.toMono OmegaCompletePartialOrder.ContinuousHom.ωSup
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u} {β : Type v} (f : (α →𝒄 β) × α) :
OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = f.1 f.2

The application of continuous functions as a continuous function.

Equations
• OmegaCompletePartialOrder.ContinuousHom.Prod.apply = { toFun := fun (f : (α →𝒄 β) × α) => f.1 f.2, monotone' := , cont := }
Instances For
theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_def {α : Type u} {β : Type v} (c : ) (x : α) :
theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup {α : Type u} {β : Type v} (c₀ : ) (c₁ : ) :
= OmegaCompletePartialOrder.ContinuousHom.Prod.apply (OmegaCompletePartialOrder.ωSup (c₀.zip c₁))
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type v} {γ : Type u_3} {α : Type u_5} (f : αβ →𝒄 γ) (x : β) (y : α) :
= (f y) x
def OmegaCompletePartialOrder.ContinuousHom.flip {β : Type v} {γ : Type u_3} {α : Type u_5} (f : αβ →𝒄 γ) :
β →𝒄 αγ

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

Equations
• = { toFun := fun (x : β) (y : α) => (f y) x, monotone' := , cont := }
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply {α : Type u} {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) (x : α) :
(f.bind g) x = f x >>= g x
noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u} {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) :

Part.bind as a continuous function.

Equations
• f.bind g = { toOrderHom := (f).bind g.toOrderHom, cont := }
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u} {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) (x : α) :
= f <\$> g x
noncomputable def OmegaCompletePartialOrder.ContinuousHom.map {α : Type u} {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) :

Part.map as a continuous function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u} {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) (x : α) :
(f.seq g) x = Seq.seq (f x) fun (x_1 : Unit) => g x
noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u} {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) :

Part.seq as a continuous function.

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