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
• Recursive definitions of partial functions and their computations
• Semantics of Programming Languages: Structures and Techniques

def OmegaCompletePartialOrder.Chain (α : Type u) [Preorder α] : Type u

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations

• OmegaCompletePartialOrder.Chain α = (ℕ →o α)

instance OmegaCompletePartialOrder.Chain.instFunLikeNat {α : Type u_2} [Preorder α] : FunLike (Chain α) ℕ α

Equations

• OmegaCompletePartialOrder.Chain.instFunLikeNat = inferInstanceAs (FunLike (ℕ →o α) ℕ α)

instance OmegaCompletePartialOrder.Chain.instOrderHomClassNat {α : Type u_2} [Preorder α] : OrderHomClass (Chain α) ℕ α

instance OmegaCompletePartialOrder.Chain.instInhabited {α : Type u_2} [Preorder α] [Inhabited α] : Inhabited (Chain α)

Equations

• OmegaCompletePartialOrder.Chain.instInhabited = { default := { toFun := default, monotone' := ⋯ } }

instance OmegaCompletePartialOrder.Chain.instMembership {α : Type u_2} [Preorder α] : Membership α (Chain α)

Equations

• OmegaCompletePartialOrder.Chain.instMembership = { mem := fun (c : ℕ →o α) (a : α) => ∃ (i : ℕ), a = c i }

instance OmegaCompletePartialOrder.Chain.instLE {α : Type u_2} [Preorder α] : LE (Chain α)

Equations

• OmegaCompletePartialOrder.Chain.instLE = { le := fun (x y : OmegaCompletePartialOrder.Chain α) => ∀ (i : ℕ), ∃ (j : ℕ), x i ≤ y j }

theorem OmegaCompletePartialOrder.Chain.isChain_range {α : Type u_2} [Preorder α] (c : Chain α) : IsChain (fun (x1 x2 : α) => x1 ≤ x2) (Set.range ⇑c)

theorem OmegaCompletePartialOrder.Chain.directed {α : Type u_2} [Preorder α] (c : Chain α) : Directed (fun (x1 x2 : α) => x1 ≤ x2) ⇑c

def OmegaCompletePartialOrder.Chain.map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) (f : α →o β) : Chain β

map function for Chain

Equations

• c.map f = f.comp c

@[simp]

theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) (f : α →o β) : ⇑(c.map f) = ⇑f ∘ ⇑c

theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} (x : α) : x ∈ c → f x ∈ c.map f

theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} {b : β} : b ∈ c.map f → ∃ a ∈ c, f a = b

@[simp]

theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} {b : β} : b ∈ c.map f ↔ ∃ a ∈ c, f a = b

@[simp]

theorem OmegaCompletePartialOrder.Chain.map_id {α : Type u_2} [Preorder α] (c : Chain α) : c.map OrderHom.id = c

theorem OmegaCompletePartialOrder.Chain.map_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (c : Chain α) {f : α →o β} (g : β →o γ) : (c.map f).map g = c.map (g.comp f)

theorem OmegaCompletePartialOrder.Chain.map_le_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g

def OmegaCompletePartialOrder.Chain.zip {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c₀ : Chain α) (c₁ : Chain β) : Chain (α × β)

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

Equations

• c₀.zip c₁ = OrderHom.prod c₀ c₁

@[simp]

theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c₀ : Chain α) (c₁ : Chain β) (n : ℕ) : (c₀.zip c₁) n = (c₀ n, c₁ n)

def OmegaCompletePartialOrder.Chain.pair {α : Type u_2} [Preorder α] (a b : α) (hab : a ≤ b) : Chain α

An example of a Chain constructed from an ordered pair.

Equations

• OmegaCompletePartialOrder.Chain.pair a b hab = { toFun := fun (x : ℕ) => match x with | 0 => a | x => b, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.pair_zero {α : Type u_2} [Preorder α] (a b : α) (hab : a ≤ b) : (pair a b hab) 0 = a

@[simp]

theorem OmegaCompletePartialOrder.Chain.pair_succ {α : Type u_2} [Preorder α] (a b : α) (hab : a ≤ b) (n : ℕ) : (pair a b hab) (n + 1) = b

@[simp]

theorem OmegaCompletePartialOrder.Chain.range_pair {α : Type u_2} [Preorder α] (a b : α) (hab : a ≤ b) : Set.range ⇑(pair a b hab) = {a, b}

@[simp]

theorem OmegaCompletePartialOrder.Chain.pair_zip_pair {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

class OmegaCompletePartialOrder (α : Type u_6) extends PartialOrder α : Type u_6

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• ωSup : Chain α → α

  The supremum of an increasing sequence

• le_ωSup (c : Chain α) (i : ℕ) : c i ≤ ωSup c

  ωSup is an upper bound of the increasing sequence

• ωSup_le (c : Chain α) (x : α) : (∀ (i : ℕ), c i ≤ x) → ωSup c ≤ x

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

@[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)) : OmegaCompletePartialOrder β

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

• OmegaCompletePartialOrder.lift f ωSup₀ h h' = OmegaCompletePartialOrder.mk ωSup₀ ⋯ ⋯

theorem OmegaCompletePartialOrder.le_ωSup_of_le {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} (i : ℕ) (h : x ≤ c i) : x ≤ ωSup c

theorem OmegaCompletePartialOrder.ωSup_total {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} (h : ∀ (i : ℕ), c i ≤ x ∨ x ≤ c i) : ωSup c ≤ x ∨ x ≤ ωSup c

theorem OmegaCompletePartialOrder.ωSup_le_ωSup_of_le {α : Type u_2} [OmegaCompletePartialOrder α] {c₀ c₁ : Chain α} (h : c₀ ≤ c₁) : ωSup c₀ ≤ ωSup c₁

@[simp]

theorem OmegaCompletePartialOrder.ωSup_le_iff {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} : ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

theorem OmegaCompletePartialOrder.isLUB_range_ωSup {α : Type u_2} [OmegaCompletePartialOrder α] (c : Chain α) : IsLUB (Set.range ⇑c) (ωSup c)

theorem OmegaCompletePartialOrder.ωSup_eq_of_isLUB {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {a : α} (h : IsLUB (Set.range ⇑c) a) : a = ωSup c

def OmegaCompletePartialOrder.subtype {α : Type u_6} [OmegaCompletePartialOrder α] (p : α → Prop) (hp : ∀ (c : Chain α), (∀ i ∈ c, p i) → p (ωSup c)) : OmegaCompletePartialOrder (Subtype p)

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.

def OmegaCompletePartialOrder.ωScottContinuous {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) : Prop

A function f between ω-complete partial orders is ωScottContinuous if it is Scott continuous over chains.

Equations

• OmegaCompletePartialOrder.ωScottContinuous f = ScottContinuousOn (Set.range fun (c : OmegaCompletePartialOrder.Chain α) => Set.range ⇑c) f

theorem ScottContinuous.ωScottContinuous {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} (hf : ScottContinuous f) : OmegaCompletePartialOrder.ω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) : IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (ωSup c))

theorem OmegaCompletePartialOrder.ωScottContinuous.id {α : Type u_2} [OmegaCompletePartialOrder α] : ωScottContinuous _root_.id

theorem OmegaCompletePartialOrder.ωScottContinuous.map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} (hf : ωScottContinuous f) (c : Chain α) : f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })

theorem OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α → β} : ωScottContinuous f ↔ ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

ω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 : α → β} : (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })) → ωScottContinuous 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 : α → β} : ωScottContinuous f → ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

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 β} : ωScottContinuous ⇑f ↔ ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

theorem OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →o β} : (∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)) → ωScottContinuous ⇑f

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 β} : ωScottContinuous ⇑f → ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

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 : β} : ωScottContinuous (Function.const α x)

theorem Part.eq_of_chain {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a b : α} (ha : some a ∈ c) (hb : some b ∈ c) : a = b

noncomputable def Part.ωSup {α : Type u_2} (c : OmegaCompletePartialOrder.Chain (Part α)) : Part α

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

Equations

• Part.ωSup c = if h : ∃ (a : α), Part.some a ∈ c then Part.some (Classical.choose h) else Part.none

theorem Part.ωSup_eq_some {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} (h : some a ∈ c) : Part.ωSup c = some a

theorem Part.ωSup_eq_none {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬∃ (a : α), some a ∈ c) : Part.ωSup c = none

theorem Part.mem_chain_of_mem_ωSup {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} (h : a ∈ Part.ωSup c) : some a ∈ c

noncomputable instance Part.omegaCompletePartialOrder {α : Type u_2} : OmegaCompletePartialOrder (Part α)

Equations

• Part.omegaCompletePartialOrder = OmegaCompletePartialOrder.mk Part.ωSup ⋯ ⋯

theorem Part.mem_ωSup {α : Type u_2} (x : α) (c : OmegaCompletePartialOrder.Chain (Part α)) : x ∈ OmegaCompletePartialOrder.ωSup c ↔ some x ∈ c

instance instOmegaCompletePartialOrderForall {α : Type u_2} {β : α → Type u_6} [(a : α) → OmegaCompletePartialOrder (β a)] : OmegaCompletePartialOrder ((a : α) → β a)

Equations

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

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) : ωScottContinuous f

theorem OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂ {α : Type u_2} {γ : Type u_4} {β : α → Type u_6} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] {f : γ → (x : α) → β x} : ωScottContinuous f ↔ ∀ (a : α), ωScottContinuous fun (x : γ) => f x a

def Prod.ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : α × β

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

Equations

• Prod.ωSup c = (OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst), OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd))

@[simp]

theorem Prod.ωSup_fst {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)

@[simp]

theorem Prod.ωSup_snd {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)

instance Prod.instOmegaCompletePartialOrder {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α × β)

Equations

• Prod.instOmegaCompletePartialOrder = OmegaCompletePartialOrder.mk Prod.ωSup ⋯ ⋯

@[simp]

theorem Prod.instOmegaCompletePartialOrder_ωSup_fst {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)

@[simp]

theorem Prod.instOmegaCompletePartialOrder_ωSup_snd {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).2 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.snd)

theorem Prod.ωSup_zip {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) : OmegaCompletePartialOrder.ωSup (c₀.zip c₁) = (OmegaCompletePartialOrder.ωSup c₀, OmegaCompletePartialOrder.ωSup c₁)

@[instance 100]

instance CompleteLattice.instOmegaCompletePartialOrder {α : Type u_2} [CompleteLattice α] : OmegaCompletePartialOrder α

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

Equations

• CompleteLattice.instOmegaCompletePartialOrder = OmegaCompletePartialOrder.mk (fun (c : OmegaCompletePartialOrder.Chain α) => ⨆ (i : ℕ), c i) ⋯ ⋯

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) : OmegaCompletePartialOrder.ωScottContinuous (SupSet.sSup s)

theorem CompleteLattice.ωScottContinuous.sup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [CompleteLattice β] {f g : α → β} (hf : OmegaCompletePartialOrder.ωScottContinuous f) (hg : OmegaCompletePartialOrder.ωScottContinuous g) : OmegaCompletePartialOrder.ωScottContinuous (f ⊔ g)

theorem CompleteLattice.ωScottContinuous.top {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [CompleteLattice β] : OmegaCompletePartialOrder.ωScottContinuous ⊤

theorem CompleteLattice.ωScottContinuous.bot {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [CompleteLattice β] : OmegaCompletePartialOrder.ωScottContinuous ⊥

theorem CompleteLattice.ωScottContinuous.inf {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [CompleteLinearOrder β] {f g : α → β} (hf : OmegaCompletePartialOrder.ωScottContinuous f) (hg : OmegaCompletePartialOrder.ωScottContinuous g) : OmegaCompletePartialOrder.ωScottContinuous (f ⊓ g)

def OmegaCompletePartialOrder.OrderHom.ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →o β)) : α →o β

The ωSup operator for monotone functions.

Equations

• OmegaCompletePartialOrder.OrderHom.ωSup c = { toFun := fun (a : α) => OmegaCompletePartialOrder.ωSup (c.map (OrderHom.apply a)), monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.OrderHom.ωSup_coe {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →o β)) (a : α) : (OrderHom.ωSup c) a = ωSup (c.map (OrderHom.apply a))

instance OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α →o β)

Equations

• OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder = OmegaCompletePartialOrder.lift OrderHom.coeFnHom OmegaCompletePartialOrder.OrderHom.ωSup ⋯ ⋯

@[simp]

theorem OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ωSup_coe {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →o β)) (a : α) : (ωSup c) a = ωSup (c.map (OrderHom.apply 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 : α → β
• monotone' : Monotone self.toFun
• map_ωSup' (c : Chain α) : self.toFun (ωSup c) = ωSup (c.map self.toOrderHom)

  The underlying function of a ContinuousHom is continuous, i.e. it preserves ωSup

def OmegaCompletePartialOrder.«term_→𝒄_» : Lean.TrailingParserDescr

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.

instance OmegaCompletePartialOrder.instFunLikeContinuousHom {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : FunLike (α →𝒄 β) α β

Equations

• OmegaCompletePartialOrder.instFunLikeContinuousHom = { coe := fun (f : α →𝒄 β) => f.toFun, coe_injective' := ⋯ }

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

• OmegaCompletePartialOrder.instPartialOrderContinuousHom = PartialOrder.lift (fun (f : α →𝒄 β) => f.toFun) ⋯

theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : ωScottContinuous ⇑f

theorem OmegaCompletePartialOrder.ContinuousHom.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : f.toOrderHom = ↑f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf : ∀ (c : Chain α), f.toFun (ωSup c) = ωSup (c.map f)) : ⇑{ toOrderHom := f, map_ωSup' := hf } = ⇑f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : ⇑f.toOrderHom = ⇑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

• OmegaCompletePartialOrder.ContinuousHom.Simps.apply h = ⇑h

theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f g : α →𝒄 β} (h : f = g) (x : α) : f x = g x

theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) {x y : α} (h : x = y) : f x = f 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) : f x ≤ g y

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_bind {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (c : Chain α) (f : α →o Part β) (g : α →o β → Part γ) : ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)

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 α) : F (ωSup C) = ωSup (C.map ↑F)

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

• OmegaCompletePartialOrder.ContinuousHom.copy f g h = { toOrderHom := g.copy f h, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.copy_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α → β) (g : α →𝒄 β) (h : f = ⇑g) (a✝ : α) : (copy f g h) a✝ = f a✝

def OmegaCompletePartialOrder.ContinuousHom.id {α : Type u_2} [OmegaCompletePartialOrder α] : α →𝒄 α

The identity as a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.id = { toOrderHom := OrderHom.id, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.id_apply {α : Type u_2} [OmegaCompletePartialOrder α] (a : α) : id a = 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

• f.comp g = { toOrderHom := f.comp g.toOrderHom, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) (a✝ : α) : (f.comp g) a✝ = f (g a✝)

theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) (h : ∀ (x : α), f x = g x) : f = g

theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) (h : ⇑f = ⇑g) : f = g

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.comp_id {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) : f.comp id = f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) : id.comp f = 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 : α →𝒄 β) : f.comp (g.comp h) = (f.comp g).comp h

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a : α) (f : α →𝒄 β) : ↑f a = f a

def OmegaCompletePartialOrder.ContinuousHom.const {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) : α →𝒄 β

Function.const is a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.const x = { toOrderHom := (OrderHom.const α) x, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.const_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) (a✝ : α) : (const x) a✝ = x

instance OmegaCompletePartialOrder.ContinuousHom.instInhabited {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [Inhabited β] : Inhabited (α →𝒄 β)

Equations

• OmegaCompletePartialOrder.ContinuousHom.instInhabited = { default := OmegaCompletePartialOrder.ContinuousHom.const default }

def OmegaCompletePartialOrder.ContinuousHom.toMono {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : (α →𝒄 β) →o α →o β

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

Equations

• OmegaCompletePartialOrder.ContinuousHom.toMono = { toFun := fun (f : α →𝒄 β) => ↑f, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.toMono_coe {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) : toMono f = ↑f

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) (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_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) (z : β) : (∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ 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

• OmegaCompletePartialOrder.ContinuousHom.ωSup c = { toOrderHom := OmegaCompletePartialOrder.ωSup (c.map OmegaCompletePartialOrder.ContinuousHom.toMono), map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →𝒄 β)) (a : α) : (ContinuousHom.ωSup c) a = ωSup ((c.map toMono).map (OrderHom.apply a))

instance OmegaCompletePartialOrder.ContinuousHom.inst {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : OmegaCompletePartialOrder (α →𝒄 β)

Equations

• OmegaCompletePartialOrder.ContinuousHom.inst = OmegaCompletePartialOrder.lift OmegaCompletePartialOrder.ContinuousHom.toMono OmegaCompletePartialOrder.ContinuousHom.ωSup ⋯ ⋯

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.inst_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →𝒄 β)) : ωSup c = ContinuousHom.ωSup c

def OmegaCompletePartialOrder.ContinuousHom.Prod.apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] : (α →𝒄 β) × α →𝒄 β

The application of continuous functions as a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.Prod.apply = { toFun := fun (f : (α →𝒄 β) × α) => f.1 f.2, monotone' := ⋯, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : (α →𝒄 β) × α) : apply f = f.1 f.2

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_def {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : Chain (α →𝒄 β)) (x : α) : (ωSup c) x = (ContinuousHom.ωSup c) x

theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_apply_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : Chain (α →𝒄 β)) (c₁ : Chain α) : (ωSup c₀) (ωSup c₁) = Prod.apply (ωSup (c₀.zip c₁))

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

• OmegaCompletePartialOrder.ContinuousHom.flip f = { toFun := fun (x : β) (y : α) => (f y) x, monotone' := ⋯, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_6} (f : α → β →𝒄 γ) (x : β) (y : α) : (flip f) x y = (f y) x

noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ) : α →𝒄 Part γ

Part.bind as a continuous function.

Equations

• f.bind g = { toOrderHom := (↑f).partBind g.toOrderHom, map_ωSup' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 β → Part γ) (x : α) : (f.bind g) x = (f x).bind (g x)

noncomputable def OmegaCompletePartialOrder.ContinuousHom.map {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : β → γ) (g : α →𝒄 Part β) : α →𝒄 Part γ

Part.map as a continuous function.

Equations

• OmegaCompletePartialOrder.ContinuousHom.map f g = OmegaCompletePartialOrder.ContinuousHom.copy (fun (x : α) => f <$> g x) (g.bind (OmegaCompletePartialOrder.ContinuousHom.const (pure ∘ f))) ⋯

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : β → γ) (g : α →𝒄 Part β) (x : α) : (map f g) x = Part.map f (g x)

noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part (β → γ)) (g : α →𝒄 Part β) : α →𝒄 Part γ

Part.seq as a continuous function.

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part (β → γ)) (g : α →𝒄 Part β) (x : α) : (f.seq g) x = f x <*> g 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

• OmegaCompletePartialOrder.fixedPoints.iterateChain f x h = { toFun := fun (n : ℕ) => (⇑f)^[n] x, monotone' := ⋯ }

theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint {α : Type u_2} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x ≤ f x) : ωSup (iterateChain (↑f) x h) ∈ Function.fixedPoints ⇑f

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) : ωSup (iterateChain (↑f) x h) ≤ 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) : ωSup (iterateChain (↑f) x h) ≤ a

The supremum of iterating a function on x arbitrary often is smaller than any fixed point.