intervalIntegrable_comp_compProj — Mathlib

English

If IsPicardLindelof f t0 x0 a r L K holds, then α ∈ FunSpace implies contiguously that t ↦ f(t, α.compProj t) is continuous on Icc tmin tmax.

Русский

При условии IsPicardLindelof f t0 x0 a r L K, для любого α ∈ FunSpace отображение t ↦ f(t, α.compProj t) непрерывно на Icc(tmin,tmax).

LaTeX

$$continuousOn (fun t' => f t' (α.compProj t')) (Icc tmin tmax)$$

Lean4

/-- The integrand in `next` is integrable. -/
theorem intervalIntegrable_comp_compProj (hf : IsPicardLindelof f t₀ x₀ a r L K) (α : FunSpace t₀ x₀ r L)
    (t : Icc tmin tmax) : IntervalIntegrable (fun t' ↦ f t' (α.compProj t')) volume t₀ t :=
  by
  apply ContinuousOn.intervalIntegrable
  apply α.continuousOn_comp_compProj hf |>.mono
  exact uIcc_subset_Icc t₀.2 t.2

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