card_sum — Mathlib

English

The cardinality of a disjoint sum is the sum of the cardinalities: ENat.card(α ⊕ β) = ENat.card α + ENat.card β.

Русский

Кардинал суммы двух типов равен сумме их кардиналов: ENat.card(α ⊕ β) = ENat.card α + ENat.card β.

LaTeX

$$$\operatorname{ENat}.card(\alpha \oplus \beta) = \operatorname{ENat}.card(\alpha) + \operatorname{ENat}.card(\beta)$$$

Lean4

@[simp]
theorem card_sum (α β : Type*) : card (α ⊕ β) = card α + card β := by simp only [card, mk_sum, map_add, toENat_lift]

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