charFun_map_smul — Mathlib

English

For any r ∈ ℝ and t ∈ E, χ_{μ map (r • ·)}(t) = χ_{μ}(r • t).

Русский

При любом r ∈ ℝ и t ∈ E выполняется χ_{μ∘(r·)}(t) = χ_{μ}(r t).

LaTeX

$$$$\\chi_{\\mu \\mapsto (r \\cdot \\mu)}(t) = \\chi_{\\mu}(r t).$$$$

Lean4

theorem charFun_map_smul [BorelSpace E] (r : ℝ) (t : E) : charFun (μ.map (r • ·)) t = charFun μ (r • t) :=
  by
  rw [charFun_apply, charFun_apply, integral_map (by fun_prop) (by fun_prop)]
  simp_rw [inner_smul_right, ← real_inner_smul_left]

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