Theorems · Definition · logic and foundations
WellOrderingRel
{α : Type u} → α → α → PropAny type can be endowed with a well order, obtained by pulling back the well order over cardinals by some embedding.
- Defined in
- Mathlib.SetTheory.Cardinal.Order
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Cardinalproof · cited by 2,598
- Order.Preimageproof · cited by 42
- embeddingToCardinalproof · cited by 2
Cited by34
Results whose statement or proof uses this declaration.
- SimpleGraph.nonuniformWitnessproof · cited by 7
- Ordinal.bfamilyOfFamilystatement and proof · cited by 7
- BumpCovering.toPOUFunproof · cited by 6
- BumpCovering.toPOUFun_eq_mul_prodstatement and proof · cited by 3
- Ordinal.bsup_eq_iSupstatement and proof · cited by 2
- BumpCovering.toPOUFun_zero_of_zeroproof · cited by 2
- BumpCovering.exists_finset_toPOUFun_eventuallyEqstatement and proof · cited by 1
- BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEqstatement · cited by 1
- BumpCovering.sum_toPOUFun_eqproof · cited by 1
- BumpCovering.toPartitionOfUnity_eq_mul_prodstatement and proof · cited by 1
- exteriorPower.finrank_eqproof · cited by 1
- MvPolynomial.combinatorial_nullstellensatz_exists_linearCombinationproof · cited by 1