measurable_enorm

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

URI: https://scilib.ai/kg/mathlib#measurable_enorm

English

The enorm function on ε is measurable: enorm: ε → ℝ≥0∞ is a measurable map.

Русский

Функция enorm с пространства ε измерима: enorm: ε → ℝ≥0∞ — измерима.

LaTeX

$$$\\text{Measurable}(\\text{enorm} : \\varepsilon \\to \\mathbb{R}_{\\ge 0}^{\\infty})$$$

Lean4

@[measurability, fun_prop]
theorem measurable_enorm : Measurable (enorm : ε → ℝ≥0∞) :=
  continuous_enorm.measurable

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

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

Разделы

Аффилиация

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