indicator_const_smul_apply — Mathlib

English

If r is a constant scalar, the indicator of r • f at a point equals r times the indicator of f at that point.

Русский

Если r — константный скаляр, индикатор r • f в точке равен r умножить на индикатор f в этой точке.

LaTeX

$$$ \mathrm{indicator}(s, (\lambda x . r \cdot f(x))) = r \cdot \mathrm{indicator}(s, f) $$$

Lean4

theorem indicator_const_smul_apply (s : Set α) (r : R) (f : α → M) (a : α) :
    indicator s (r • f ·) a = r • indicator s f a :=
  indicator_smul_apply s (fun _ ↦ r) f a

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