Cardinality_of_Complement
Provedcardinalitycombinatoricsproofwikiset-difference
Let such that . Then where denotes the complement of relative to denotes the difference between and .
Preamble
import Mathlib.Data.Finset.Card
Formal statement
theorem Cardinality_of_Complement {S : Finset ℕ} {T : Finset ℕ} (h : T ⊆ S) : (S \ T).card = S.card - T.card := by sorrySource