English
For predicates p, q on α, the cardinality of the subtype { x : α | p x ∨ q x } is at most the sum of the cardinalities of { x : α | p x } and { x : α | q x } when these subtypes are finite.
Русский
Для предикатов p, q на α кардинал подтипа { x ∈ α | p x ∨ q x } не превосходит суммы кардиналов подтипов { x ∈ α | p x } и { x ∈ α | q x } при условии конечности подтипов.
LaTeX
$$$$|\\{ x : α \\mid p x \\lor q x \\}| \\le |\\{ x : α \\mid p x \\}| + |\\{ x : α \\mid q x \\}|.$$$$
Lean4
theorem card_subtype_or (p q : α → Prop) [Fintype { x // p x }] [Fintype { x // q x }] [Fintype { x // p x ∨ q x }] :
Fintype.card { x // p x ∨ q x } ≤ Fintype.card { x // p x } + Fintype.card { x // q x } := by
classical
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
rw [Fintype.card_sum]
