Theorems · Definition · order theory
OmegaCompletePartialOrder.Chain.pair
{α : Type u_2} → [inst : Preorder α] → (a b : α) → a ≤ b → OmegaCompletePartialOrder.Chain αAn example of a Chain constructed from an ordered pair.
- Defined in
- Mathlib.Order.OmegaCompletePartialOrder
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- OmegaCompletePartialOrder.Chainstatement · cited by 85
Cited by8
Results whose statement or proof uses this declaration.
- OmegaCompletePartialOrder.ωScottContinuous.monotoneproof · cited by 15
- OmegaCompletePartialOrder.Chain.range_pairstatement · cited by 3
- Topology.IsScott.ωScottContinuous_iff_continuousproof · cited by 0
- OmegaCompletePartialOrder.Chain.pair_succstatement · cited by 0
- OmegaCompletePartialOrder.Chain.pair_zerostatement · cited by 0
- OmegaCompletePartialOrder.Chain.pair_zip_pairstatement and proof · cited by 0
- Prod.ωScottContinuous.prodMkproof · cited by 0
- OmegaCompletePartialOrder.Chain.pair.congr_simpstatement and proof · cited by 0