Theorems · Theorem · logic and foundations
Cardinal.toNat_le_toNat
∀ {c d : Cardinal.{u}}, c ≤ d → d < Cardinal.aleph0 → Cardinal.toNat c ≤ Cardinal.toNat d- Defined in
- Mathlib.SetTheory.Cardinal.ToNat
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Cardinalstatement and proof · cited by 2,598
- LE.le.trans_ltproof · cited by 795
- MonoidWithZeroHomstatement · cited by 704
- Cardinal.aleph0statement and proof · cited by 521
- Cardinal.toNatstatement · cited by 153
- Cardinal.toNat_monotoneOnproof · cited by 1
Cited by14
Results whose statement or proof uses this declaration.
- Submodule.finrank_leproof · cited by 20
- Nat.card_le_card_of_injectiveproof · cited by 19
- Nat.card_le_card_of_surjectiveproof · cited by 11
- Submodule.finrank_monoproof · cited by 11
- Module.finrank_le_finrank_of_rank_le_rankproof · cited by 7
- Matrix.rank_mul_le_leftproof · cited by 5
- Nat.card_monoproof · cited by 5
- finrank_le_oneproof · cited by 2
- Subalgebra.finrank_sup_le_of_freeproof · cited by 2
- Submodule.FG.spanFinrank_baseChange_leproof · cited by 1
- card_algHom_le_finrankproof · cited by 1
- Set.natCard_add_leproof · cited by 1