indicator_mul_left — Mathlib

English

For a set s and functions f,g: ι → M₀, the i-th value of indicator_s(f(i)·g(i)) equals indicator_s f(i) · g(i).

Русский

Для множества s и функций f,g: ι → M₀, значение indicator_s(f(i)·g(i)) равно indicator_s f(i) · g(i).

LaTeX

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

Lean4

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

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