card_disjUnion

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_disjUnion

English

If s and t are disjoint, then the cardinality of their disjoint union equals the sum of their cardinalities.

Русский

Если s и t не пересекаются, то кардинальность их дизъюнкции равна сумме кардинальностей.

LaTeX

$$Disjoint(s, t) ⇒ |s \uplus t| = |s| + |t|$$

Lean4

@[simp, grind =]
theorem card_disjUnion (s t : Finset α) (h) : #(s.disjUnion t h) = #s + #t :=
  Multiset.card_add _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru