Limits and pointwise ω-suprema for ωCPOs

This file defines:

• Basic omega-limit operations
• Pointwise ω-suprema for function spaces needed in the compatibility axiom for ωQBS

def OmegaCompletePartialOrder.omegaLimit {α : Type u} [OmegaCompletePartialOrder α] (c : Chain α) : α

the omega-limit of a chain is its omega-supremum

Equations

• OmegaCompletePartialOrder.omegaLimit c = OmegaCompletePartialOrder.ωSup c

theorem OmegaCompletePartialOrder.omegaLimit_isLUB {α : Type u} [OmegaCompletePartialOrder α] (c : Chain α) : IsLUB (Set.range ⇑c) (omegaLimit c)

the omega-limit is a least upper bound

theorem OmegaCompletePartialOrder.omegaLimit_unique {α : Type u} [OmegaCompletePartialOrder α] (c : Chain α) {l : α} (hl : IsLUB (Set.range ⇑c) l) : l = omegaLimit c

the omega-limit is unique

def OmegaCompletePartialOrder.evalOrderHom {ι : Type u} {α : Type v} [OmegaCompletePartialOrder α] (x : ι) : (ι → α) →o α

evaluation at a point as an order homomorphism

Equations

• OmegaCompletePartialOrder.evalOrderHom x = { toFun := fun (f : ι → α) => f x, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.evalOrderHom_apply {ι : Type u} {α : Type v} [OmegaCompletePartialOrder α] (x : ι) (f : ι → α) : (evalOrderHom x) f = f x

theorem OmegaCompletePartialOrder.ωSup_eval {ι : Type u} {α : Type v} [OmegaCompletePartialOrder α] (c : Chain (ι → α)) (x : ι) : ωSup c x = ωSup (c.map (evalOrderHom x))

pointwise omega-supremum: the omega-supremum of a chain of functions is the function that takes omega-supremum pointwise