English
Let α and β be finite types. The cardinality of the disjoint sum α ⊕ β is the sum of the cardinalities: |α ⊕ β| = |α| + |β|.
Русский
Пусть α и β — конечные множества. Кардинал объединения α ⊕ β равен сумме кардиналов: |α ⊕ β| = |α| + |β|.
LaTeX
$$$$|\\alpha \\oplus \\beta| = |\\alpha| + |\\beta|.$$$$
Lean4
@[simp]
theorem card_sum [Fintype α] [Fintype β] : Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β :=
card_disjSum _ _