re

Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike

URI: https://scilib.ai/kg/mathlib#Measurable.re

English

If f: α → 𝕜 is measurable, then x ↦ Re(f(x)) is measurable.

Русский

Пусть f: α → 𝕜 измерима, тогда x ↦ Re(f(x)) измерима.

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem re (hf : Measurable f) : Measurable fun x => RCLike.re (f x) :=
  RCLike.measurable_re.comp hf

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

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

Разделы

Аффилиация

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