encard_union_add_encard_inter — Mathlib

English

For sets S and T, (S ∪ T).encard + (S ∩ T).encard = S.encard + T.encard.

Русский

Для множеств S и T выполняется (S ∪ T).encard + (S ∩ T).encard = S.encard + T.encard.

LaTeX

$$$\operatorname{encard}(S \cup T) + \operatorname{encard}(S \cap T) = \operatorname{encard}(S) + \operatorname{encard}(T)$$$

Lean4

theorem encard_union_add_encard_inter (s t : Set α) : (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard := by
  rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm, encard_diff_add_encard_inter]

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