dens_disjUnion — Mathlib

English

If s and t are disjoint Finsets, then the density of their disjoint union equals the sum of densities.

Русский

Если s и t распр. Finset, плотность их дизъюнкции равна сумме плотностей.

LaTeX

$$$\\forall s,t:\\ Finset\\ \\alpha,\\ \\text{Disjoint}(s,t)\\Rightarrow \\mathrm{dens}(s\\disjUnion t) = \\mathrm{dens}(s) + \\mathrm{dens}(t)$$$

Lean4

@[simp]
theorem dens_disjUnion (s t : Finset α) (h) : dens (s.disjUnion t h) = dens s + dens t := by
  simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]

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