card_eq_sum_card_image — Mathlib

English

For f: ι → M and s finite, |s| equals the sum over b in s.image f of the fiber sizes.

Русский

Для отображения f:ι→M и конечного множества s, |s| равно сумме размеров волокон по каждому b из image f(s).

LaTeX

$$$$|s| = \\sum_{b \\in s.image f} \\#\\{ a \\in s \\mid f a = b \\}$$$$

Lean4

theorem card_eq_sum_card_image [DecidableEq M] (f : ι → M) (s : Finset ι) :
    #s = ∑ b ∈ s.image f, #({a ∈ s | f a = b}) :=
  card_eq_sum_card_fiberwise fun _ => mem_image_of_mem _

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