indicator_smul_const — Mathlib

English

For s ⊆ α, r: α → R, and m ∈ M, the indicator of the map x ↦ r(x) · m on s is the same as the map a ↦ indicator s r a · m; i.e., indicator s (r · • m) = indicator s r · • m.

Русский

Для s ⊆ α, r : α → R и m ∈ M индикатор отображения x ↦ r(x) · m на s равен отображению a ↦ индикатор s r a · m; то есть indicator s (r · • m) = (indicator s r) · • m.

LaTeX

$$$$ \\mathrm{indicator}_s (r \\cdot \\mathbf{•} m) = (\\mathrm{indicator}_s r) \\cdot \\mathbf{•} m. $$$$

Lean4

theorem indicator_smul_const (s : Set α) (r : α → R) (m : M) : indicator s (r · • m) = (indicator s r · • m) :=
  funext <| indicator_smul_const_apply _ _ _

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