charFun_map_mul

Mathlib.MeasureTheory.Measure.CharacteristicFunction

URI: https://scilib.ai/kg/mathlib#MeasureTheory.charFun_map_mul

English

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

Русский

Для любого r ∈ ℝ верно χ_{μ map (r • ·)}(t) = χ_{μ}(r t).

LaTeX

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

Lean4

theorem charFun_map_mul {μ : Measure ℝ} (r t : ℝ) : charFun (μ.map (r * ·)) t = charFun μ (r * t) :=
  charFun_map_smul r t

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru