dens_union_add_dens_inter — Mathlib

English

For Finsets s, t, the density satisfies dens(s ∪ t) + dens(s ∩ t) = dens(s) + dens(t).

Русский

Плотности образуют равенство: плотность объединения плюс плотность пересечения равны сумме плотностей.

LaTeX

$$$ \\operatorname{dens}(s \\cup t) + \\operatorname{dens}(s \\cap t) = \\operatorname{dens}(s) + \\operatorname{dens}(t) $$$

Lean4

theorem dens_union_add_dens_inter (s t : Finset α) : dens (s ∪ t) + dens (s ∩ t) = dens s + dens t := by
  simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]

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