Theorems · Theorem · logic and foundations
Ordinal.le_cof_map_of_isNormal
∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, Order.IsNormal f → ∀ (a : Ordinal.{u_1}), a.cof ≤ (f a).cof- Cited by
- 1 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement and proof · cited by 2,598
- le_reflproof · cited by 2,061
- Ordinalstatement and proof · cited by 1,688
- Order.succproof · cited by 633
- Order.IsSuccLimitproof · cited by 255
- Ordinal.cofstatement and proof · cited by 125
- Order.IsNormalstatement and proof · cited by 118
- Iff.neproof · cited by 52
- Order.lt_succproof · cited by 45
- Order.IsNormal.strictMonoproof · cited by 44
- LT.lt.ne_zeroproof · cited by 34
- Ordinal.limitRecOnproof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- Ordinal.cof_le_of_isNormalproof · cited by 0