enorm

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

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

English

If f: β → ε is measurable, then the function a ↦ norm(f(a)) with ENorm is measurable.

Русский

Если f: β → ε измерима, то a ↦ ‖f(a)‖ₑ измерима.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\lambda a. \\lVert f(a) \\rVert_{\\!\\varepsilon})$$$

Lean4

@[measurability, fun_prop]
protected theorem enorm {f : β → ε} (hf : Measurable f) : Measurable (‖f ·‖ₑ) :=
  measurable_enorm.comp hf

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

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

Разделы

Аффилиация

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