sum_card_fiberwise_eq_card_filter

English

For s ⊆ ι, t ⊆ κ, g: ι → κ, we have ∑ j ∈ t |{ i ∈ s | g i = j }| = |{ i ∈ s | g i ∈ t }|.

Русский

Для подмножеств s ⊆ ι, t ⊆ κ и отображения g: ι → κ имеем сумму по j ∈ t чисел |{i ∈ s | g(i) = j}| равную |{ i ∈ s | g(i) ∈ t }|.

LaTeX

$$$$\\sum_{j \\in t} \\#\\{ i \\in s \\mid g(i) = j \\} = \\#\\{ i \\in s \\mid g(i) \\in t \\}$$$$

Lean4

theorem sum_card_fiberwise_eq_card_filter {κ : Type*} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) :
    ∑ j ∈ t, #({i ∈ s | g i = j}) = #({i ∈ s | g i ∈ t}) := by
  simpa only [card_eq_sum_ones] using sum_fiberwise_eq_sum_filter _ _ _ _

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