Mathlib Map

Theorems · Inductive type · order theory

OmegaCompletePartialOrder.Chain

(α : Type u) → [Preorder α] → Type u

A chain is a monotone sequence. This is made a one-field structure around order homomorphisms ℕ →o α because we want to endow chains with the domination order rather than the pointwise order. See Chain.instLE. See the definition on page 114 of [gunter1992].

Defined in
Mathlib.Order.OmegaCompletePartialOrder
Cited by
85 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Preorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

OmegaCompletePartialOrder.ωSup · cited by 48OmegaCompletePartialOrder…OmegaCompletePartialOrder.ωScottContinuous · cited by 47OmegaCompletePartialOrder…OmegaCompletePartialOrder.Chain.map · cited by 41Chain.mapOmegaCompletePartialOrder.ωScottContinuous.monotone · cited by 15ωScottContinuous.monotoneOmegaCompletePartialOrder.ωSup_le · cited by 11OmegaCompletePartialOrder…OmegaCompletePartialOrder.ωScottContinuous.map_ωSup · cited by 11ωScottContinuous.map_ωSupOmegaCompletePartialOrder.Chain.toOrderHom · cited by 10Chain.toOrderHomOmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup · cited by 9ωScottContinuous.of_monot…OmegaCompletePartialOrder.Chain.pair · cited by 8Chain.pairOmegaCompletePartialOrder.le_ωSup · cited by 8OmegaCompletePartialOrder…Part.Fix.approxChain · cited by 6Fix.approxChainOmegaCompletePartialOrder.Chain.zip · cited by 6Chain.zipPart.ωSup · cited by 4Part.ωSupOmegaCompletePartialOrder.fixedPoints.iterateChain · cited by 4fixedPoints.iterateChainOmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom · cited by 4ωScottContinuous.of_map_ω…Preorder · cited by 7952PreorderOmegaCompletePartialOrder.Cha…CITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by117

Results whose statement or proof uses this declaration.