norm — Mathlib

English

Let f be interval-integrable on [a,b] with respect to μ. Then the function t ↦ ||f(t)|| is interval-integrable on [a,b].

Русский

Пусть f является интервално интегрируемой на [a,b] по мере μ. Тогда функция t ↦ ||f(t)|| интегрируема по интервалу [a,b].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \Rightarrow \operatorname{IntervalIntegrable}(\|f\|,\mu,a,b)$$$

Lean4

theorem norm {f : ℝ → E} (h : IntervalIntegrable f μ a b) : IntervalIntegrable (‖f ·‖) μ a b :=
  ⟨h.1.norm, h.2.norm⟩

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