Theorems · Theorem · logic and foundations
Cardinal.isRegular_succ
∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → (Order.succ c).IsRegular- Defined in
- Mathlib.SetTheory.Cardinal.Regular
- Cited by
- 6 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.
Cites19
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
- Set.Iioproof · cited by 1,166
- Order.succstatement and proof · cited by 633
- Cardinal.aleph0statement and proof · cited by 521
- Cardinal.IsRegularstatement · cited by 282
- Cardinal.ordproof · cited by 266
- Ordinal.cofproof · cited by 125
- Order.le_succproof · cited by 96
- Cardinal.card_ordproof · cited by 23
- Eq.not_ltproof · cited by 22
Cited by6
Results whose statement or proof uses this declaration.
- Cardinal.isRegular_aleph_oneproof · cited by 3
- Cardinal.isRegular_preAleph_add_oneproof · cited by 2
- Cardinal.infinite_pigeonhole_card_ltproof · cited by 2
- Cardinal.isRegular_aleph_add_oneproof · cited by 2
- Cardinal.not_isSingular_succproof · cited by 1
- HasCardinalLT.exists_regular_cardinalproof · cited by 1