English
Let s be a finite set of indices, f_i ⊆ κ, and g_i : κ → R. Then for every j ∈ κ, the product over i ∈ s of the indicator of f_i evaluated at g_i, all at j, equals the indicator of the intersection of all f_i evaluated at the product ∏_{i∈s} g_i, evaluated at j.
Русский
Пусть s — конечное множество индексов, f_i ⊆ κ, и g_i : κ → R. Тогда для каждого j ∈ κ произведение по i∈s индикаторов f_i∶ g_i(j) равно индикатору пересечения всех f_i, применённому к произведению ∏_{i∈s} g_i, в точке j.
LaTeX
$$$$ \\prod_{i \\in s} (f(i).indicator (g(i)))(j) = \\left( \\bigcap_{x \\in s} f(x) \\right).indicator \\left( \\prod_{i \\in s} g(i) \\right)(j). $$$$
Lean4
theorem prod_indicator_apply (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R) (j : κ) :
∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j :=
by
rw [Set.indicator]
split_ifs with hj
· rw [Finset.prod_apply]
congr! 1 with i hi
simp only [Set.mem_iInter] at hj
exact Set.indicator_of_mem (hj _ hi) _
· obtain ⟨i, hi, hj⟩ := by simpa using hj
exact Finset.prod_eq_zero hi <| Set.indicator_of_notMem hj _
