norm

Mathlib.MeasureTheory.Constructions.BorelSpace.Metric

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

English

If f is measurable, then the function a ↦ ||f(a)|| is measurable.

Русский

Если f измерима, то a ↦ ||f(a)|| измеримо.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(\\lambda a. \\lVert f(a) \\rVert)$$$

Lean4

@[measurability, fun_prop]
theorem norm {f : β → α} (hf : Measurable f) : Measurable fun a => norm (f a) :=
  measurable_norm.comp hf

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

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

Разделы

Аффилиация

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