card_sum — Mathlib

English

If α and β are finite, then Nat.card (α ⊕ β) = Nat.card α + Nat.card β.

Русский

Если α и β конечны, то Кардинальность суммы α ⊕ β равна сумме кардинальностей α и β.

LaTeX

$$$$ Nat.card(\alpha \oplus \beta) = Nat.card(\alpha) + Nat.card(\beta) $$$$

Lean4

@[simp]
theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β :=
  by
  have := Fintype.ofFinite α
  have := Fintype.ofFinite β
  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]

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