Theorems · Theorem · combinatorics
Finset.card_union_of_disjoint
∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], Disjoint s t → (s ∪ t).card = s.card + t.cardAlias of the reverse direction of Finset.card_union_eq_card_add_card.
- Defined in
- Mathlib.Data.Finset.Card
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.cardstatement · cited by 2,327
- Disjointstatement · cited by 2,201
- Finset.card_union_eq_card_add_cardproof · cited by 1
Cited by37
Results whose statement or proof uses this declaration.
- Finset.card_sdiff_of_subsetproof · cited by 35
- Finset.card_filter_add_card_filter_notproof · cited by 7
- Finset.card_dvd_card_image₂_rightproof · cited by 6
- Equiv.Perm.Disjoint.card_support_mulproof · cited by 4
- Finpartition.card_parts_equitabiliseproof · cited by 3
- cauchy_davenport_minOrder_addproof · cited by 2
- Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_invproof · cited by 2
- SimpleGraph.card_edgeFinset_replaceVertex_of_not_adjproof · cited by 2
- Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicityproof · cited by 2
- Nat.smoothNumbersUpTo_card_add_roughNumbersUpTo_cardproof · cited by 1
- Rel.card_interedges_add_card_interedges_complproof · cited by 1
- FiniteField.exists_root_sum_quadraticproof · cited by 1