dens_disjiUnion — Mathlib

English

Let s be a finite set and t: α → Finset β. Then the density of the biUnion equals the sum of the densities:

Русский

Пусть s — конечное множество и t: α → Finset β. Тогда плотность объединения по s равна сумме плотностей по элементам s.

LaTeX

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

Lean4

@[simp]
theorem dens_disjiUnion (s : Finset α) (t : α → Finset β) (h) : (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens := by
  simp [dens, sum_div]

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