English
The cardinality of the complement subtype {x // ¬p x} equals the cardinality of α minus the cardinality of the subtype {x // p x}.
Русский
Кардинальность дополнения подтипа {x // ¬p x} равна кардинальности α минус кардинальность подтипа {x // p x}.
LaTeX
$$$|\{ x // \neg p x \}| = |\alpha| - |\{ x // p x \}|$$
Lean4
@[simp]
theorem card_subtype_compl [Fintype α] (p : α → Prop) [Fintype { x // p x }] [Fintype { x // ¬p x }] :
Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x } := by
classical
rw [Fintype.card_of_subtype (Set.toFinset {x | p x}ᶜ), Set.toFinset_compl, Finset.card_compl,
Fintype.card_of_subtype] <;>
· intro
simp only [Set.mem_toFinset, Set.mem_compl_iff, Set.mem_setOf]
