indicator_mul_const — Mathlib

English

For s ⊆ ι, f: ι → M₀ and a ∈ M₀, the function s.indicator (f · a) satisfies s.indicator (f(i) · a) = s.indicator f(i) · a for all i.

Русский

Для любого подмножества s ⊆ ι, функции f и константы a ∈ M₀ выполняется s.indicator (f(i) · a) = s.indicator f(i) · a для всех i.

LaTeX

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

Lean4

theorem indicator_mul_const (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι) : s.indicator (f · * a) i = s.indicator f i * a :=
  by rw [indicator_mul_left]

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