prod_indicator_const_apply — Mathlib

English

Let s be finite, f_i ⊆ κ, and g : κ → R. Then the product over i∈s of the indicator of f_i by g equals the indicator of the intersection with g raised to the |s|-th power.

Русский

Пусть s — конечное множество, f_i ⊆ κ, и g : κ → R. Тогда произведение индикаторов f_i, применённых к g, по i∈s равно индикатору пересечения f_i, применяемому к g^{|s|}.

LaTeX

$$$$ \\prod_{i \\in s} (f(i)).indicator g = \\left( \\bigcap_{x \\in s} f(x) \\right).indicator \\left( g^{|s|} \\right). $$$$

Lean4

theorem prod_indicator_const_apply (s : Finset ι) (f : ι → Set κ) (g : κ → R) (j : κ) :
    ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ #s) j := by simp [prod_indicator_apply]

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