prod_indicator_const — Mathlib

English

Same as the previous statement, just expressed as an equality of functions.

Русский

То же самое, что и в предыдущем proposition, но в виде равенства функций.

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 (s : Finset ι) (f : ι → Set κ) (g : κ → R) :
    ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ #s) := by simp [prod_indicator]

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