English
If two predicates p and q on α have equal subtype cardinalities, then their complements also have equal cardinalities.
Русский
Если кардинальности подтипов p и q равны, то кардинальности их дополнений тоже равны.
LaTeX
$$$\text{If } |\{ x // p x \}| = |\{ x // q x \}| \Rightarrow |\{ x // \neg p x \}| = |\{ x // \neg q x \}|$$$
Lean4
/-- If two subtypes of a fintype have equal cardinality, so do their complements. -/
theorem card_compl_eq_card_compl [Finite α] (p q : α → Prop) [Fintype { x // p x }] [Fintype { x // ¬p x }]
[Fintype { x // q x }] [Fintype { x // ¬q x }] (h : Fintype.card { x // p x } = Fintype.card { x // q x }) :
Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x } :=
by
cases nonempty_fintype α
simp only [Fintype.card_subtype_compl, h]
