measurable_nnnorm

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

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

English

The NNReal norm (nnnorm) of a measurable function is measurable.

Русский

NNNorm измеримой функции измерим.

LaTeX

$$$\\text{Measurable}(\\text{nnnorm} : \\alpha \\to \\mathbb{R}_{\\ge 0})$$$

Lean4

@[measurability]
theorem measurable_nnnorm : Measurable (nnnorm : α → ℝ≥0) :=
  continuous_nnnorm.measurable

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

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

Разделы

Аффилиация

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