Mathlib Map

Theorems · Definition · order theory

OmegaCompletePartialOrder.Chain.toOrderHom

{α : Type u} → [inst : Preorder α] → OmegaCompletePartialOrder.Chain α → ℕ →o α
Defined in
Mathlib.Order.OmegaCompletePartialOrder
Cited by
10 results in Mathlib
Foundations
Depth 21 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.Chain.map · cited by 41Chain.mapOmegaCompletePartialOrder.Chain.zip · cited by 6Chain.zipPart.eq_of_chain · cited by 2Part.eq_of_chainOmegaCompletePartialOrder.ContinuousHom.ωSup_bind · cited by 1ContinuousHom.ωSup_bindCompleteLattice.ωScottContinuous.inf · cited by 1ωScottContinuous.infOmegaCompletePartialOrder.ContinuousHom.forall_forall_merge · cited by 1ContinuousHom.forall_fora…OmegaCompletePartialOrder.Chain.map_le_map · cited by 0Chain.map_le_mapOmegaCompletePartialOrder.Chain.map_toOrderHom · cited by 0Chain.map_toOrderHomOmegaCompletePartialOrder.ContinuousHom.ωScottContinuous_apply · cited by 0ContinuousHom.ωScottConti…Submodule.coe_scott_continuous · cited by 0Submodule.coe_scott_conti…OmegaCompletePartialOrder.Chain.coe_toOrderHom · cited by 0Chain.coe_toOrderHomOmegaCompletePartialOrder.Chain.zip_toOrderHom · cited by 0Chain.zip_toOrderHomPreorder · cited by 7952PreorderOrderHom · cited by 934OrderHomOmegaCompletePartialOrder.Chain · cited by 85OmegaCompletePartialOrder…Chain.toOrderHomCITED BYCITES

Cites3

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

Cited by12

Results whose statement or proof uses this declaration.