Theorems · Theorem · logic and foundations
Set.ncard_eq_toFinset_card
∀ {α : Type u_1} (s : Set α) (hs : autoParam s.Finite Set.ncard_eq_toFinset_card._auto_1), s.ncard = hs.toFinset.card- Defined in
- Mathlib.Data.Set.Card
- Cited by
- 21 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemproof · cited by 7,166
- Finset.cardstatement and proof · cited by 2,327
- Set.Finitestatement and proof · cited by 1,814
- Fintype.cardproof · cited by 1,386
- Set.Finite.toFinsetstatement and proof · cited by 351
- Set.ncardstatement · cited by 344
- Nat.card_eq_fintype_cardproof · cited by 200
- Nat.card_coe_set_eqproof · cited by 19
- Set.Finite.card_toFinsetproof · cited by 2
Cited by21
Results whose statement or proof uses this declaration.
- Set.ncard_coe_finsetproof · cited by 15
- Set.one_lt_ncardproof · cited by 4
- Set.two_lt_ncard_iffproof · cited by 3
- Set.ncard_le_oneproof · cited by 3
- Set.exists_union_disjoint_cardinal_eq_of_evenproof · cited by 2
- Ideal.height_le_height_add_spanFinrank_of_leproof · cited by 2
- Ideal.exists_finset_card_eq_height_of_isNoetherianRingproof · cited by 2
- ProbabilityTheory.map_ncard_setBernoulli_real_singletonproof · cited by 2
- Set.three_lt_ncard_iffproof · cited by 1
- Set.eq_insert_of_ncard_eq_succproof · cited by 1
- finsum_oneproof · cited by 1
- Set.ncard_le_one_iff_subset_singletonproof · cited by 1