English
If p and q are disjoint predicates on α, then the cardinality of { x : α | p x ∨ q x } equals the sum of the cardinalities of { x : α | p x } and { x : α | q x }.
Русский
Если предикаты p и q на α несовместны, то кардинал подтипа { x ∈ α | p x ∨ q x } равен сумме кардиналов подтипов { x ∈ α | p x } и { x ∈ α | q x }.
LaTeX
$$$$|\\{ x : α \\mid p x \\lor q x \\}| = |\\{ x : α \\mid p x \\}| + |\\{ x : α \\mid q x \\}|.$$$$
Lean4
theorem card_subtype_or_disjoint (p q : α → Prop) (h : Disjoint p q) [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_congr (subtypeOrEquiv p q h)
simp
