continuous_integral — Mathlib

English

The map sending f to its Bochner integral is a continuous function from L1(μ;E) to E.

Русский

Карта, отправляющая f в его Бо́хнеров интеграл, непрерывна по норме в L1(μ;E).

LaTeX

$$$\\text{Continuous}\\big( f \\mapsto \\int f\\,d\\mu \\big)$$$

Lean4

@[continuity]
theorem continuous_integral : Continuous fun f : α →₁[μ] E => integral f :=
  by
  simp only [integral]
  exact L1.integralCLM.continuous

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