indicator_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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