continuousOn_primitive_interval — Mathlib

English

If f is continuous in the parameter, then the interval integral varies continuously with the endpoint parameter.

Русский

Если функция непрерывна по параметру, то интеграл по интервалу меняется непрерывно при изменении конца интервала.

LaTeX

$$$\\text{Continuous}\\bigl(\\lambda p, \\int_a^{p.2} f(p.1, t) dt\\bigr)$$$

Lean4

theorem continuousOn_primitive_interval (h_int : IntegrableOn f (uIcc a b) μ) :
    ContinuousOn (fun x => ∫ t in a..x, f t ∂μ) (uIcc a b) :=
  continuousOn_primitive_interval' h_int.intervalIntegrable left_mem_uIcc

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