Theorems · Theorem · order theory
Set.card_ne_eq
∀ {α : Type u} [inst : Fintype α] (a : α) [inst_1 : Fintype ↑{x | x ≠ a}],
Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetproof · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Set.Elemstatement and proof · cited by 7,166
- Set.ofPredstatement and proof · cited by 6,101
- Finset.univproof · cited by 3,473
- Finset.cardproof · cited by 2,327
- Fintype.cardstatement and proof · cited by 1,386
- Finset.mem_univproof · cited by 361
- Classical.decEqproof · cited by 134
- Set.toFinset_cardproof · cited by 63
- Finset.card_univproof · cited by 58
- Finset.card_erase_of_memproof · cited by 38
Cited by1
Results whose statement or proof uses this declaration.
- HallMarriageTheorem.hall_hard_inductive_step_Aproof · cited by 1