dens_biUnion — Mathlib

English

If f is a function and t finite, then t.dens equals the sum over a in s of the dens of the fiber {b ∈ t | f b = a}.

Русский

Если f — функция и t — конечный, то dens(t) равно сумме по a∈s плотностей фибра {b ∈ t | f(b) = a}.

LaTeX

$$$t.dens = \sum_{a \in s} \{ b \in t \mid f(b) = a \}.dens$$$

Lean4

theorem dens_biUnion [DecidableEq β] (h : s.toSet.PairwiseDisjoint t) : (s.biUnion t).dens = ∑ u ∈ s, (t u).dens := by
  simp [dens, card_biUnion h, sum_div]

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