card_inter_add_card_union — Mathlib

English

For finite sets s,t, the sum of the cardinalities of their intersection and their union equals the sum of the cardinalities of s and t.

Русский

Для конечных множеств s,t сумма кардинальностей пересечения и объединения равна сумме кардинальностей s и t.

LaTeX

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

Lean4

theorem card_inter_add_card_union (s t : Finset α) : #(s ∩ t) + #(s ∪ t) = #s + #t := by grind

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