Theorems · Theorem · ordinary differential equations

ODE.continuousOn_comp

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {s : Set ℝ} {u : Set E},
  ContinuousOn (Function.uncurry f) (s ×ˢ u) → ContinuousOn α s → Set.MapsTo α s u → ContinuousOn (fun t => f t (α t)) s

Given a continuous time-dependent vector field f and a continuous curve α, the composition f t (α t) is continuous in t.

Defined in

Mathlib.Analysis.ODE.PicardLindelof

Cited by

3 results in Mathlib

Foundations

Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace