card_sum — Mathlib

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 _ _

Похожие утверждения