order.omega_complete_partial_order

def order_hom.bind {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →o part β) (g : α →o β → part γ) :

part.bind as a monotone function

Equations

f.bind g = {to_fun := λ (x : α), ⇑f x >>= ⇑g x, monotone' := _}

@[simp]

theorem order_hom.bind_coe {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →o part β) (g : α →o β → part γ) (x : α) :

⇑(f.bind g) x = ⇑f x >>= ⇑g x

source

def omega_complete_partial_order.chain (α : Type u) [preorder α] :

Type u

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations

omega_complete_partial_order.chain α = (ℕ →o α)

Instances for omega_complete_partial_order.chain

source

@[protected, instance]

def omega_complete_partial_order.chain.has_coe_to_fun {α : Type u} [preorder α] :

has_coe_to_fun (omega_complete_partial_order.chain α) (λ (_x : omega_complete_partial_order.chain α), ℕ → α)

Equations

omega_complete_partial_order.chain.has_coe_to_fun = order_hom.has_coe_to_fun

source

@[protected, instance]

def omega_complete_partial_order.chain.inhabited {α : Type u} [preorder α] [inhabited α] :

inhabited (omega_complete_partial_order.chain α)

Equations

omega_complete_partial_order.chain.inhabited = {default := {to_fun := inhabited.default (pi.inhabited ℕ), monotone' := _}}

source

@[protected, instance]

def omega_complete_partial_order.chain.has_mem {α : Type u} [preorder α] :

has_mem α (omega_complete_partial_order.chain α)

Equations

omega_complete_partial_order.chain.has_mem = {mem := λ (a : α) (c : ℕ →o α), ∃ (i : ℕ), a = ⇑c i}

source

@[protected, instance]

def omega_complete_partial_order.chain.has_le {α : Type u} [preorder α] :

has_le (omega_complete_partial_order.chain α)

Equations

omega_complete_partial_order.chain.has_le = {le := λ (x y : omega_complete_partial_order.chain α), ∀ (i : ℕ), ∃ (j : ℕ), ⇑x i ≤ ⇑y j}

source

def omega_complete_partial_order.chain.map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →o β) :

omega_complete_partial_order.chain β

map function for chain

Equations

c.map f = f.comp c

source

@[simp]

theorem omega_complete_partial_order.chain.map_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →o β) :

⇑(c.map f) = ⇑f ∘ ⇑c

source

theorem omega_complete_partial_order.chain.mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →o β} (x : α) :

x ∈ c → ⇑f x ∈ c.map f

source

theorem omega_complete_partial_order.chain.exists_of_mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →o β} {b : β} :

b ∈ c.map f → (∃ (a : α), a ∈ c ∧ ⇑f a = b)

source

theorem omega_complete_partial_order.chain.mem_map_iff {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →o β} {b : β} :

b ∈ c.map f ↔ ∃ (a : α), a ∈ c ∧ ⇑f a = b

source

@[simp]

theorem omega_complete_partial_order.chain.map_id {α : Type u} [preorder α] (c : omega_complete_partial_order.chain α) :

c.map order_hom.id = c

source

theorem omega_complete_partial_order.chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [preorder α] [preorder β] [preorder γ] (c : omega_complete_partial_order.chain α) {f : α →o β} (g : β →o γ) :

(c.map f).map g = c.map (g.comp f)

source

theorem omega_complete_partial_order.chain.map_le_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f g : α →o β} (h : f ≤ g) :

c.map f ≤ c.map g

source

def omega_complete_partial_order.chain.zip {α : Type u} {β : Type v} [preorder α] [preorder β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) :

omega_complete_partial_order.chain (α × β)

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

Equations

c₀.zip c₁ = order_hom.prod c₀ c₁

source

@[simp]

theorem omega_complete_partial_order.chain.zip_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) (x : ℕ) :

⇑(c₀.zip c₁) x = (⇑c₀ x, ⇑c₁ x)

source

@[class]

structure omega_complete_partial_order (α : Type u_1) :

Type u_1

to_partial_order : partial_order α
ωSup : omega_complete_partial_order.chain α → α
le_ωSup : ∀ (c : omega_complete_partial_order.chain α) (i : ℕ), ⇑c i ≤ omega_complete_partial_order.ωSup c
ωSup_le : ∀ (c : omega_complete_partial_order.chain α) (x : α), (∀ (i : ℕ), ⇑c i ≤ x) → omega_complete_partial_order.ωSup c ≤ x

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

Instances of this typeclass

Instances of other typeclasses for omega_complete_partial_order

omega_complete_partial_order.has_sizeof_inst

source

@[protected, reducible]

def omega_complete_partial_order.lift {α : Type u} {β : Type v} [omega_complete_partial_order α] [partial_order β] (f : β →o α) (ωSup₀ : omega_complete_partial_order.chain β → β) (h : ∀ (x y : β), ⇑f x ≤ ⇑f y → x ≤ y) (h' : ∀ (c : omega_complete_partial_order.chain β), ⇑f (ωSup₀ c) = omega_complete_partial_order.ωSup (c.map f)) :

omega_complete_partial_order β

Transfer a omega_complete_partial_order on β to a omega_complete_partial_order 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

omega_complete_partial_order.lift f ωSup₀ h h' = {to_partial_order := _inst_2, ωSup := ωSup₀, le_ωSup := _, ωSup_le := _}

source

theorem omega_complete_partial_order.le_ωSup_of_le {α : Type u} [omega_complete_partial_order α] {c : omega_complete_partial_order.chain α} {x : α} (i : ℕ) (h : x ≤ ⇑c i) :

x ≤ omega_complete_partial_order.ωSup c

source

theorem omega_complete_partial_order.ωSup_total {α : Type u} [omega_complete_partial_order α] {c : omega_complete_partial_order.chain α} {x : α} (h : ∀ (i : ℕ), ⇑c i ≤ x ∨ x ≤ ⇑c i) :

omega_complete_partial_order.ωSup c ≤ x ∨ x ≤ omega_complete_partial_order.ωSup c

source

theorem omega_complete_partial_order.ωSup_le_ωSup_of_le {α : Type u} [omega_complete_partial_order α] {c₀ c₁ : omega_complete_partial_order.chain α} (h : c₀ ≤ c₁) :

omega_complete_partial_order.ωSup c₀ ≤ omega_complete_partial_order.ωSup c₁

source

theorem omega_complete_partial_order.ωSup_le_iff {α : Type u} [omega_complete_partial_order α] (c : omega_complete_partial_order.chain α) (x : α) :

omega_complete_partial_order.ωSup c ≤ x ↔ ∀ (i : ℕ), ⇑c i ≤ x

source

def omega_complete_partial_order.subtype {α : Type u_1} [omega_complete_partial_order α] (p : α → Prop) (hp : ∀ (c : omega_complete_partial_order.chain α), (∀ (i : α), i ∈ c → p i) → p (omega_complete_partial_order.ωSup c)) :

omega_complete_partial_order (subtype p)

A subset p : α → Prop of the type closed under ωSup induces an omega_complete_partial_order on the subtype {a : α // p a}.

Equations

omega_complete_partial_order.subtype p hp = omega_complete_partial_order.lift (order_hom.subtype.val p) (λ (c : omega_complete_partial_order.chain (subtype p)), ⟨omega_complete_partial_order.ωSup (c.map (order_hom.subtype.val p)), _⟩) _ _

source

def omega_complete_partial_order.continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →o β) :

Prop

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

omega_complete_partial_order.continuous f = ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f)

source

def omega_complete_partial_order.continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) :

Prop

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

Equations

omega_complete_partial_order.continuous' f = ∃ (hf : monotone f), omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}

source

theorem omega_complete_partial_order.continuous'.to_monotone {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f : α → β} (hf : omega_complete_partial_order.continuous' f) :

monotone f

source

theorem omega_complete_partial_order.continuous.of_bundled {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (hf : monotone f) (hf' : omega_complete_partial_order.continuous {to_fun := f, monotone' := hf}) :

omega_complete_partial_order.continuous' f

source

theorem omega_complete_partial_order.continuous.of_bundled' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →o β) (hf' : omega_complete_partial_order.continuous f) :

omega_complete_partial_order.continuous' ⇑f

source

theorem omega_complete_partial_order.continuous'.to_bundled {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (hf : omega_complete_partial_order.continuous' f) :

omega_complete_partial_order.continuous {to_fun := f, monotone' := _}

source

@[simp, norm_cast]

theorem omega_complete_partial_order.continuous'_coe {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f : α →o β} :

omega_complete_partial_order.continuous' ⇑f ↔ omega_complete_partial_order.continuous f

source

theorem omega_complete_partial_order.continuous_id {α : Type u} [omega_complete_partial_order α] :

omega_complete_partial_order.continuous order_hom.id

source

theorem omega_complete_partial_order.continuous_comp {α : Type u} {β : Type v} {γ : Type u_1} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : α →o β) (g : β →o γ) (hfc : omega_complete_partial_order.continuous f) (hgc : omega_complete_partial_order.continuous g) :

omega_complete_partial_order.continuous (g.comp f)

source

theorem omega_complete_partial_order.id_continuous' {α : Type u} [omega_complete_partial_order α] :

omega_complete_partial_order.continuous' id

source

theorem omega_complete_partial_order.continuous_const {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (x : β) :

omega_complete_partial_order.continuous (⇑(order_hom.const α) x)

source

theorem omega_complete_partial_order.const_continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (x : β) :

omega_complete_partial_order.continuous' (function.const α x)

source

theorem part.eq_of_chain {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a b : α} (ha : part.some a ∈ c) (hb : part.some b ∈ c) :

a = b

source

@[protected]

noncomputable def part.ωSup {α : Type u} (c : omega_complete_partial_order.chain (part α)) :

part α

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

Equations

part.ωSup c = dite (∃ (a : α), part.some a ∈ c) (λ (h : ∃ (a : α), part.some a ∈ c), part.some (classical.some h)) (λ (h : ¬∃ (a : α), part.some a ∈ c), part.none)

source

theorem part.ωSup_eq_some {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a : α} (h : part.some a ∈ c) :

part.ωSup c = part.some a

source

theorem part.ωSup_eq_none {α : Type u} {c : omega_complete_partial_order.chain (part α)} (h : ¬∃ (a : α), part.some a ∈ c) :

part.ωSup c = part.none

source

theorem part.mem_chain_of_mem_ωSup {α : Type u} {c : omega_complete_partial_order.chain (part α)} {a : α} (h : a ∈ part.ωSup c) :

part.some a ∈ c

source

@[protected, instance]

noncomputable def part.omega_complete_partial_order {α : Type u} :

omega_complete_partial_order (part α)

Equations

part.omega_complete_partial_order = {to_partial_order := part.partial_order α, ωSup := part.ωSup α, le_ωSup := _, ωSup_le := _}

source

theorem part.mem_ωSup {α : Type u} (x : α) (c : omega_complete_partial_order.chain (part α)) :

x ∈ omega_complete_partial_order.ωSup c ↔ part.some x ∈ c

source

@[protected, instance]

def pi.omega_complete_partial_order {α : Type u_1} {β : α → Type u_2} [Π (a : α), omega_complete_partial_order (β a)] :

omega_complete_partial_order (Π (a : α), β a)

Equations

pi.omega_complete_partial_order = {to_partial_order := pi.partial_order (λ (i : α), omega_complete_partial_order.to_partial_order), ωSup := λ (c : omega_complete_partial_order.chain (Π (a : α), β a)) (a : α), omega_complete_partial_order.ωSup (c.map (pi.eval_order_hom a)), le_ωSup := _, ωSup_le := _}

source

theorem pi.omega_complete_partial_order.flip₁_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : Π (x : α), γ → β x) (a : α) (hf : omega_complete_partial_order.continuous' (λ (x : γ) (y : α), f y x)) :

omega_complete_partial_order.continuous' (f a)

source

theorem pi.omega_complete_partial_order.flip₂_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : γ → Π (x : α), β x) (hf : ∀ (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :

omega_complete_partial_order.continuous' f

source

@[simp]

theorem prod.ωSup_snd {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α × β)) :

(prod.ωSup c).snd = omega_complete_partial_order.ωSup (c.map order_hom.snd)

source

@[simp]

theorem prod.ωSup_fst {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α × β)) :

(prod.ωSup c).fst = omega_complete_partial_order.ωSup (c.map order_hom.fst)

source

@[protected]

def prod.ωSup {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α × β)) :

α × β

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

Equations

prod.ωSup c = (omega_complete_partial_order.ωSup (c.map order_hom.fst), omega_complete_partial_order.ωSup (c.map order_hom.snd))

source

@[simp]

theorem prod.omega_complete_partial_order_ωSup_fst {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α × β)) :

(omega_complete_partial_order.ωSup c).fst = omega_complete_partial_order.ωSup (c.map order_hom.fst)

source

@[simp]

theorem prod.omega_complete_partial_order_ωSup_snd {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α × β)) :

(omega_complete_partial_order.ωSup c).snd = omega_complete_partial_order.ωSup (c.map order_hom.snd)

source

@[protected, instance]

def prod.omega_complete_partial_order {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] :

omega_complete_partial_order (α × β)

Equations

prod.omega_complete_partial_order = {to_partial_order := prod.partial_order α β omega_complete_partial_order.to_partial_order, ωSup := prod.ωSup _inst_2, le_ωSup := _, ωSup_le := _}

source

theorem prod.ωSup_zip {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) :

omega_complete_partial_order.ωSup (c₀.zip c₁) = (omega_complete_partial_order.ωSup c₀, omega_complete_partial_order.ωSup c₁)

source

@[protected, instance]

def complete_lattice.omega_complete_partial_order (α : Type u) [complete_lattice α] :

omega_complete_partial_order α

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

Equations

complete_lattice.omega_complete_partial_order α = {to_partial_order := complete_semilattice_Inf.to_partial_order α (complete_lattice.to_complete_semilattice_Inf α), ωSup := λ (c : omega_complete_partial_order.chain α), ⨆ (i : ℕ), ⇑c i, le_ωSup := _, ωSup_le := _}

source

theorem complete_lattice.Sup_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] (s : set (α →o β)) (hs : ∀ (f : α →o β), f ∈ s → omega_complete_partial_order.continuous f) :

omega_complete_partial_order.continuous (has_Sup.Sup s)

source

theorem complete_lattice.supr_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] {ι : Sort u_1} {f : ι → α →o β} (h : ∀ (i : ι), omega_complete_partial_order.continuous (f i)) :

omega_complete_partial_order.continuous (⨆ (i : ι), f i)

source

theorem complete_lattice.Sup_continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] (s : set (α → β)) (hc : ∀ (f : α → β), f ∈ s → omega_complete_partial_order.continuous' f) :

omega_complete_partial_order.continuous' (has_Sup.Sup s)

source

theorem complete_lattice.sup_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] {f g : α →o β} (hf : omega_complete_partial_order.continuous f) (hg : omega_complete_partial_order.continuous g) :

omega_complete_partial_order.continuous (f ⊔ g)

source

theorem complete_lattice.top_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] :

omega_complete_partial_order.continuous ⊤

source

theorem complete_lattice.bot_continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] :

omega_complete_partial_order.continuous ⊥

source

theorem complete_lattice.inf_continuous {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [complete_linear_order β] (f g : α →o β) (hf : omega_complete_partial_order.continuous f) (hg : omega_complete_partial_order.continuous g) :

omega_complete_partial_order.continuous (f ⊓ g)

source

theorem complete_lattice.inf_continuous' {α : Type u_1} {β : Type u_2} [omega_complete_partial_order α] [complete_linear_order β] {f g : α → β} (hf : omega_complete_partial_order.continuous' f) (hg : omega_complete_partial_order.continuous' g) :

omega_complete_partial_order.continuous' (f ⊓ g)

source

@[protected]

def omega_complete_partial_order.order_hom.ωSup {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α →o β)) :

α →o β

The ωSup operator for monotone functions.

Equations

omega_complete_partial_order.order_hom.ωSup c = {to_fun := λ (a : α), omega_complete_partial_order.ωSup (c.map (order_hom.apply a)), monotone' := _}

source

@[simp]

theorem omega_complete_partial_order.order_hom.ωSup_coe {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α →o β)) (a : α) :

⇑(omega_complete_partial_order.order_hom.ωSup c) a = omega_complete_partial_order.ωSup (c.map (order_hom.apply a))

source

@[simp]

theorem omega_complete_partial_order.order_hom.omega_complete_partial_order_ωSup_coe {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c : omega_complete_partial_order.chain (α →o β)) (a : α) :

⇑(omega_complete_partial_order.ωSup c) a = omega_complete_partial_order.ωSup (c.map (order_hom.apply a))

source

@[protected, instance]

def omega_complete_partial_order.order_hom.omega_complete_partial_order {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] :

omega_complete_partial_order (α →o β)

Equations

omega_complete_partial_order.order_hom.omega_complete_partial_order = omega_complete_partial_order.lift order_hom.coe_fn_hom omega_complete_partial_order.order_hom.ωSup omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_1 omega_complete_partial_order.order_hom.omega_complete_partial_order._proof_2

source

structure omega_complete_partial_order.continuous_hom (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :

Type (max u v)

to_order_hom : α →o β
cont : omega_complete_partial_order.continuous {to_fun := self.to_order_hom.to_fun, monotone' := _}

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 order_hom.continuous.

Instances for omega_complete_partial_order.continuous_hom

omega_complete_partial_order.continuous_hom.has_sizeof_inst
omega_complete_partial_order.continuous_hom.has_coe_to_fun
omega_complete_partial_order.order_hom.has_coe
omega_complete_partial_order.continuous_hom.partial_order
omega_complete_partial_order.continuous_hom.inhabited
omega_complete_partial_order.continuous_hom.omega_complete_partial_order

source

@[protected, instance]

def omega_complete_partial_order.continuous_hom.has_coe_to_fun (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :

has_coe_to_fun (α →𝒄 β) (λ (_x : α →𝒄 β), α → β)

Equations

omega_complete_partial_order.continuous_hom.has_coe_to_fun α β = {coe := λ (f : α →𝒄 β), f.to_order_hom.to_fun}

source

@[protected, instance]

def omega_complete_partial_order.order_hom.has_coe (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :

has_coe (α →𝒄 β) (α →o β)

Equations

omega_complete_partial_order.order_hom.has_coe α β = {coe := omega_complete_partial_order.continuous_hom.to_order_hom _inst_2}

source

@[protected, instance]

def omega_complete_partial_order.continuous_hom.partial_order (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :

partial_order (α →𝒄 β)

Equations

omega_complete_partial_order.continuous_hom.partial_order α β = partial_order.lift (λ (f : α →𝒄 β), f.to_order_hom.to_fun) _

source

def omega_complete_partial_order.continuous_hom.simps.apply (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] (h : α →𝒄 β) :

α → β

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

omega_complete_partial_order.continuous_hom.simps.apply α β h = ⇑h

source

theorem omega_complete_partial_order.continuous_hom.congr_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} (h : f = g) (x : α) :

⇑f x = ⇑g x

source

theorem omega_complete_partial_order.continuous_hom.congr_arg {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →𝒄 β) {x y : α} (h : x = y) :

⇑f x = ⇑f y

source

@[protected]

theorem omega_complete_partial_order.continuous_hom.monotone {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →𝒄 β) :

monotone ⇑f

source

theorem omega_complete_partial_order.continuous_hom.apply_mono {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) :

⇑f x ≤ ⇑g y

source

theorem omega_complete_partial_order.continuous_hom.ite_continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {p : Prop} [hp : decidable p] (f g : α → β) (hf : omega_complete_partial_order.continuous' f) (hg : omega_complete_partial_order.continuous' g) :

omega_complete_partial_order.continuous' (λ (x : α), ite p (f x) (g x))

source

theorem omega_complete_partial_order.continuous_hom.ωSup_bind {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (c : omega_complete_partial_order.chain α) (f : α →o part β) (g : α →o β → part γ) :

omega_complete_partial_order.ωSup (c.map (f.bind g)) = omega_complete_partial_order.ωSup (c.map f) >>= omega_complete_partial_order.ωSup (c.map g)

source

theorem omega_complete_partial_order.continuous_hom.bind_continuous' {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α → part β) (g : α → β → part γ) :

omega_complete_partial_order.continuous' f → omega_complete_partial_order.continuous' g → omega_complete_partial_order.continuous' (λ (x : α), f x >>= g x)

source

theorem omega_complete_partial_order.continuous_hom.map_continuous' {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : β → γ) (g : α → part β) (hg : omega_complete_partial_order.continuous' g) :

omega_complete_partial_order.continuous' (λ (x : α), f <$> g x)

source

theorem omega_complete_partial_order.continuous_hom.seq_continuous' {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α → part (β → γ)) (g : α → part β) (hf : omega_complete_partial_order.continuous' f) (hg : omega_complete_partial_order.continuous' g) :

omega_complete_partial_order.continuous' (λ (x : α), f x <*> g x)

source

theorem omega_complete_partial_order.continuous_hom.continuous {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (F : α →𝒄 β) (C : omega_complete_partial_order.chain α) :

⇑F (omega_complete_partial_order.ωSup C) = omega_complete_partial_order.ωSup (C.map ↑F)

source

@[reducible]

def omega_complete_partial_order.continuous_hom.of_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = ⇑g) :

α →𝒄 β

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

Equations

omega_complete_partial_order.continuous_hom.of_fun f g h = {to_order_hom := {to_fun := f, monotone' := _}, cont := _}

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.of_fun_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = ⇑g) (ᾰ : α) :

⇑(omega_complete_partial_order.continuous_hom.of_fun f g h) ᾰ = f ᾰ

source

@[reducible]

def omega_complete_partial_order.continuous_hom.of_mono {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →o β) (h : ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f)) :

α →𝒄 β

Construct a continuous function from a monotone function with a proof of continuity.

Equations

omega_complete_partial_order.continuous_hom.of_mono f h = {to_order_hom := {to_fun := ⇑f, monotone' := _}, cont := h}

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.of_mono_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →o β) (h : ∀ (c : omega_complete_partial_order.chain α), ⇑f (omega_complete_partial_order.ωSup c) = omega_complete_partial_order.ωSup (c.map f)) (ᾰ : α) :

⇑(omega_complete_partial_order.continuous_hom.of_mono f h) ᾰ = ⇑f ᾰ

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.id_apply {α : Type u} [omega_complete_partial_order α] (ᾰ : α) :

⇑omega_complete_partial_order.continuous_hom.id ᾰ = ᾰ

source

def omega_complete_partial_order.continuous_hom.id {α : Type u} [omega_complete_partial_order α] :

α →𝒄 α

The identity as a continuous function.

Equations

omega_complete_partial_order.continuous_hom.id = omega_complete_partial_order.continuous_hom.of_mono order_hom.id omega_complete_partial_order.continuous_id

source

def omega_complete_partial_order.continuous_hom.comp {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) :

α →𝒄 γ

The composition of continuous functions.

Equations

f.comp g = omega_complete_partial_order.continuous_hom.of_mono (↑f.comp ↑g) _

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) (ᾰ : α) :

⇑(f.comp g) ᾰ = ⇑↑f (⇑↑g ᾰ)

source

@[protected, ext]

theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) (h : ∀ (x : α), ⇑f x = ⇑g x) :

f = g

source

@[protected]

theorem omega_complete_partial_order.continuous_hom.coe_inj {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) (h : ⇑f = ⇑g) :

f = g

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.comp_id {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) :

f.comp omega_complete_partial_order.continuous_hom.id = f

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.id_comp {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) :

omega_complete_partial_order.continuous_hom.id.comp f = f

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] [omega_complete_partial_order φ] (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :

f.comp (g.comp h) = (f.comp g).comp h

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.coe_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (a : α) (f : α →𝒄 β) :

⇑↑f a = ⇑f a

source

def omega_complete_partial_order.continuous_hom.const {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (x : β) :

α →𝒄 β

function.const is a continuous function.

Equations

omega_complete_partial_order.continuous_hom.const x = omega_complete_partial_order.continuous_hom.of_mono (⇑(order_hom.const α) x) _

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.const_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : β) (a : α) :

⇑(omega_complete_partial_order.continuous_hom.const f) a = f

source

@[protected, instance]

def omega_complete_partial_order.continuous_hom.inhabited {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] [inhabited β] :

inhabited (α →𝒄 β)

Equations

omega_complete_partial_order.continuous_hom.inhabited = {default := omega_complete_partial_order.continuous_hom.const inhabited.default}

source

def omega_complete_partial_order.continuous_hom.to_mono {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] :

(α →𝒄 β) →o α →o β

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

Equations

omega_complete_partial_order.continuous_hom.to_mono = {to_fun := λ (f : α →𝒄 β), ↑f, monotone' := _}

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.to_mono_coe {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →𝒄 β) :

⇑omega_complete_partial_order.continuous_hom.to_mono f = ↑f

source

@[simp]

theorem omega_complete_partial_order.continuous_hom.forall_forall_merge {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain (α →𝒄 β)) (c₁ : omega_complete_partial_order.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.

source

@[simp]