mulIndicator_mul — Mathlib

English

For any s ⊆ α and functions f,g: α → M, the map (mulIndicator s) (f · g) equals (mulIndicator s f) · (mulIndicator s g) pointwise.

Русский

Для множества s ⊆ α и функций f,g: α → M имеем (mulIndicator s)(f·g) = (mulIndicator s f) · (mulIndicator s g) по точкам.

LaTeX

$$$\\bigl\\{\\text{mulIndicator}(s) (f \\cdot g) = \\text{mulIndicator}(s) f \\cdot \\text{mulIndicator}(s) g\\bigr\\}.$$$

Lean4

@[to_additive]
theorem mulIndicator_mul (s : Set α) (f g : α → M) :
    (mulIndicator s fun a => f a * g a) = fun a => mulIndicator s f a * mulIndicator s g a :=
  by
  funext
  simp only [mulIndicator]
  split_ifs
  · rfl
  rw [mul_one]

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