dens_eq_sum_dens_fiberwise — Mathlib

English

Let f : β → α and t finite with a map h: t.toSet.MapsTo f s.toSet. Then t.dens equals the sum over a in s of the dens of {b ∈ t | f b = a}.

Русский

Пусть f : β → α, t конечен и h: t.toSet.MapsTo f s.toSet. Тогда dens(t) = ∑_{a∈s} dens({b∈t | f b = a}).

LaTeX

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

Lean4

theorem dens_eq_sum_dens_fiberwise [DecidableEq α] {f : β → α} {t : Finset β} (h : t.toSet.MapsTo f s) :
    t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens := by simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]

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