English
Let s be finite, f_i ⊆ κ, and g_i : κ → R. Then the product of the indicators across i∈s equals the indicator of the intersection, with the product of the g_i as the value function.
Русский
Пусть s — конечное множество, f_i ⊆ κ, и g_i : κ → R. Тогда произведение индикаторов по i∈s равно индикатору пересечения f_i, при этом значение функции — произведение g_i.
LaTeX
$$$$ \\prod_{i \\in s} (f(i)).indicator (g(i)) = \\left( \\bigcap_{x \\in s} f(x) \\right).indicator \\left( \\prod_{i \\in s} g(i) \\right). $$$$
Lean4
theorem prod_indicator (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R) :
∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) := by ext a;
simpa using prod_indicator_apply ..
