card_union_eq_card_add_card

Mathlib.Data.Finset.Card

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

English

The equality |s ∪ t| = |s| + |t| holds if and only if s and t are disjoint.

Русский

Равенство |s ∪ t| = |s| + |t| выполняется тогда и только тогда, когда s and t не перекрываются.

LaTeX

$$|s ∪ t| = |s| + |t| ↔ Disjoint(s, t)$$

Lean4

theorem card_union_eq_card_add_card : #(s ∪ t) = #s + #t ↔ Disjoint s t := by rw [← card_union_add_card_inter];
  simp [disjoint_iff_inter_eq_empty]

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

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

Разделы

Аффилиация

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