Theorems · Inductive type · order theory

OmegaCompletePartialOrder.ContinuousHom

(α : Type u_2) → (β : Type u_3) → [OmegaCompletePartialOrder α] → [OmegaCompletePartialOrder β] → 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.

Defined in

Mathlib.Order.OmegaCompletePartialOrder

Cited by

41 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

OmegaCompletePartialOrderOmegaCompletePartialOrder