measurable_re

Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike

URI: https://scilib.ai/kg/mathlib#RCLike.measurable_re

English

The map x ↦ Re(f(x)) is measurable whenever f is measurable.

Русский

Любая функция f: α → 𝕜 измерима, тогда x ↦ Re(f(x)) измерима.

LaTeX

$$$ \\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\lambda x, RCLike.re (f(x))) $$$

Lean4

@[measurability]
theorem measurable_re : Measurable (re : 𝕜 → ℝ) :=
  continuous_re.measurable

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

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

Разделы

Аффилиация

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