indicator_mul — Mathlib

English

For any set s ⊆ ι and functions f,g: ι → M₀, the indicator of the product equals the product of indicators: indicator_s(f · g) = (indicator_s f) · (indicator_s g).

Русский

Пусть s ⊆ ι и функции f,g: ι → M₀. Индикация произведения равна произведению индикиров: 1_s(f·g) = 1_s f · 1_s g.

LaTeX

$$$ \operatorname{indicator}_s (f \cdot g) = (\operatorname{indicator}_s f) \cdot (\operatorname{indicator}_s g). $$$

Lean4

theorem indicator_mul (s : Set ι) (f g : ι → M₀) :
    indicator s (fun i ↦ f i * g i) = fun i ↦ indicator s f i * indicator s g i :=
  by
  funext
  simp only [indicator]
  split_ifs
  · rfl
  rw [mul_zero]

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