card_disjSum — Mathlib

English

Let s and t be finite sets in types α and β, respectively. The finite set obtained by forming their disjoint sum has cardinality equal to the sum of the cardinalities: |s disjoint-sum t| = |s| + |t|.

Русский

Пусть s и t — конечные множества над типами α и β соответственно. Кардинал дизъюнктивной суммы их элементов равен сумме кардиналів: |s ⊎ t| = |s| + |t|.

LaTeX

$$$|s \disjSum t| = |s| + |t|$$$

Lean4

@[simp]
theorem card_disjSum : (s.disjSum t).card = s.card + t.card :=
  Multiset.card_disjSum _ _

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