Theorems · Theorem · logic and foundations
Set.Infinite.ncard
∀ {α : Type u_1} {s : Set α}, s.Infinite → s.ncard = 0- Defined in
- Mathlib.Data.Set.Card
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.ncardstatement · cited by 344
- Set.Infinitestatement and proof · cited by 263
- Nat.card_eq_zero_of_infiniteproof · cited by 46
- Nat.card_coe_set_eqproof · cited by 19
Cited by12
Results whose statement or proof uses this declaration.
- Set.ncard_sdiffproof · cited by 4
- Set.ncard_union_leproof · cited by 4
- Set.finite_of_ncard_ne_zeroproof · cited by 4
- Set.ncard_le_ncard_sdiff_add_ncardproof · cited by 2
- Set.ncard_sdiff_singleton_leproof · cited by 1
- Set.exists_subsuperset_card_eqproof · cited by 1
- Set.ncard_sumEquiv_symm_applyproof · cited by 1
- Set.ncard_insert_leproof · cited by 1
- finsum_oneproof · cited by 1
- Set.ncard_le_ncard_insertproof · cited by 0
- Set.exists_union_disjoint_cardinal_eq_iffproof · cited by 0
- Set.exists_eq_insert_iff_ncardproof · cited by 0