dens_inter_add_dens_union — Mathlib

English

The same additive relation holds with interchanged terms: dens(s ∩ t) + dens(s ∪ t) = dens(s) + dens(t).

Русский

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

LaTeX

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

Lean4

theorem dens_inter_add_dens_union (s t : Finset α) : dens (s ∩ t) + dens (s ∪ t) = dens s + dens t := by
  rw [add_comm, dens_union_add_dens_inter]

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