English
If p(x) holds for almost all x except possibly one distinguished x, then the subtype {x // p x} has strictly smaller cardinality than α. In particular, if not p(x) for some x, then |{x // p x}| < |α|.
Русский
Если для некоторого x выполняется ¬p(x), тогда кардинальность подтипа {x | p x}strictly меньше кардинальности α.
LaTeX
$$$|\{ x // p x \}| < |\alpha| \quad\text{whenever } \neg p(x) \text{ holds for some } x$$
Lean4
theorem card_subtype_lt [Fintype α] {p : α → Prop} [Fintype { a // p a }] {x : α} (hx : ¬p x) :
Fintype.card { x // p x } < Fintype.card α :=
Fintype.card_lt_of_injective_of_notMem (b := x) (↑) Subtype.coe_injective <| by rwa [Subtype.range_coe_subtype]
