dens_biUnion_le — Mathlib

English

For DecidableEq β, dens of biUnion is bounded by the sum of the individual densities:

Русский

Для DecidableEq β плотность объединения не превышает сумму плотностей по элементам.

LaTeX

$$$(s.biUnion t).dens \le \sum_{a \\in s} (t a).dens$$$

Lean4

theorem dens_biUnion_le [DecidableEq β] : (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens :=
  by
  simp only [dens, ← sum_div]
  gcongr
  exact mod_cast card_biUnion_le

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