English
One can transfer an OmegaCompletePartialOrder structure along a strictly monotone order-preserving map f : β →o α, given a compatible definition of ωSup on β and compatibility conditions with ωSup on α. This yields an OmegaCompletePartialOrder structure on β with ωSup defined via the given ωSup on β and f preserving ωSup.
Русский
Можно перенести структуру Омега-частично упорядоченного типа вдоль строго монотонного отображения f: β →o α, при условии совместимости определения ωSup на β и сохранения ωSup через f; в результате β получает структуру ωCPO, где ωSupβ определяется через заданное ωSupβ и отображение f сохраняет ωSup.
LaTeX
$$$(\\text{Let } f : β \\to_o α,\\ ωSup_0 : \\text{Chain } β \\to β,\\ h : \\forall x,y, f x \\le f y \\Rightarrow x \\le y,\\ h' : \\forall c, f(ωSup_0(c)) = ωSup(c.map f)) \\Rightarrow \\OmegaCompletePartialOrder β$$$
Lean4
/-- 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 `α`. -/
protected abbrev lift [PartialOrder β] (f : β →o α) (ωSup₀ : Chain β → β) (h : ∀ x y, f x ≤ f y → x ≤ y)
(h' : ∀ c, f (ωSup₀ c) = ωSup (c.map f)) : OmegaCompletePartialOrder β
where
ωSup := ωSup₀
ωSup_le c x hx := h _ _ (by rw [h']; apply ωSup_le; intro i; apply f.monotone (hx i))
le_ωSup c i := h _ _ (by rw [h']; apply le_ωSup (c.map f))
