measurable_im

Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike

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

English

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

Русский

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

LaTeX

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

Lean4

@[measurability]
theorem measurable_im : Measurable (im : 𝕜 → ℝ) :=
  continuous_im.measurable

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

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

Разделы

Аффилиация

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