continuous_integral — Mathlib

English

The map sending a Bochner-Lp element to its integral is continuous.

Русский

Отображение, отправляющее элемент Bochner-Lp в его интеграл, непрерывно.

LaTeX

$$@[continuity] theorem continuous_integral : Continuous fun f => ∫ a, f a ∂μ$$

Lean4

@[continuity]
theorem continuous_integral : Continuous fun f : α →₁[μ] G => ∫ a, f a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)
  · simp [integral, hG, continuous_const]

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