Theorems · Theorem · logic and foundations
Ordinal.card_opow_le_of_omega0_le_left
∀ {a : Ordinal.{u_1}}, Ordinal.omega0 ≤ a → ∀ (b : Ordinal.{u_1}), (a ^ b).card ≤ max a.card b.card- Defined in
- Mathlib.SetTheory.Cardinal.Ordinal
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites38
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemproof · cited by 7,166
- LE.le.transproof · cited by 3,151
- Cardinalstatement and proof · cited by 2,598
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- Ordinalstatement and proof · cited by 1,688
- Set.Iioproof · cited by 1,166
- LT.lt.trans_leproof · cited by 678
- le_imp_le_of_le_of_leproof · cited by 576
- LT.lt.not_geproof · cited by 305
- Order.IsSuccLimitproof · cited by 255
- sup_of_le_leftproof · cited by 218
Cited by3
Results whose statement or proof uses this declaration.
- Ordinal.card_opow_le_of_omega0_le_rightproof · cited by 2
- Ordinal.card_opow_eq_of_omega0_le_leftproof · cited by 1
- Ordinal.card_opow_leproof · cited by 1