dens_eq_sum_dens_image — Mathlib

English

Let f: β → α and t finite. Then t.dens equals the sum over a in image f of the density of those b ∈ t with f b = a.

Русский

Пусть f: β → α и t конечен. Тогда dens(t) равно сумме по a в image f плотностей множества {b ∈ t | f(b) = a}.

LaTeX

$$$t.dens = \sum_{a \in \mathrm{image}(f) } {b \in t | f(b) = a}.dens$$$

Lean4

theorem dens_eq_sum_dens_image [DecidableEq α] (f : β → α) (t : Finset β) :
    t.dens = ∑ a ∈ t.image f, {b ∈ t | f b = a}.dens :=
  dens_eq_sum_dens_fiberwise fun _ ↦ mem_image_of_mem _

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