continuousOn_primitive_interval_left

English

For a function f that is integrable on symmetric intervals around an anchor, the primitive on left/right endpoints is continuous.

Русский

Для функции f, интегрируемой на симметричных окрестностях центра, примитив по левой/правой границе непрерывен.

LaTeX

$$$\\text{ContinuousOn}(\\lambda x, \\int_{x}^{b} f(t) dt, \\ Icc a b)$$$

Lean4

theorem continuousOn_primitive_interval_left (h_int : IntegrableOn f (uIcc a b) μ) :
    ContinuousOn (fun x => ∫ t in x..b, f t ∂μ) (uIcc a b) :=
  by
  rw [uIcc_comm a b] at h_int ⊢
  simp only [integral_symm b]
  exact (continuousOn_primitive_interval h_int).neg

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