card_sdiff_add_card_inter — Mathlib

English

Let s and t be finite sets. Then the number of elements in s not in t plus the number of elements in s that are in t equals the number of elements in s.

Русский

Пусть s и t — конечные множества. Тогда число элементов в s, не принадлежащих t, плюс число элементов в s, принадлежащих t, равно числу элементов в s.

LaTeX

$$$|s \\setminus t| + |s \\cap t| = |s|$$$

Lean4

@[simp]
theorem card_sdiff_add_card_inter (s t : Finset α) : #(s \ t) + #(s ∩ t) = #s := by
  rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

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