card_union_add_card_inter

Mathlib.Data.Finset.Card

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

English

For any finite sets s,t, the cardinality of their union equals the sum of their cardinalities minus the cardinality of their intersection.

Русский

Для любых конечных множеств s,t выполняется |s ∪ t| = |s| + |t| − |s ∩ t|.

LaTeX

$$|s ∪ t| = |s| + |t| − |s ∩ t|$$

Lean4

theorem card_union_add_card_inter (s t : Finset α) : #(s ∪ t) + #(s ∩ t) = #s + #t :=
  Finset.induction_on t (by simp) (by grind)

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

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

Разделы

Аффилиация

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