E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
⊢ Continuous (vComp f)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ Continuous (vComp f)
have := (continuous_subtype_val.prod_mk f.continuous).comp v.continuous_proj
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
x : ℝ
⊢ ((fun x => (↑x, toFun f x)) ∘ proj v) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
⊢ Continuous (vComp f)
refine' ContinuousOn.comp_continuous v.continuousOn this fun x => _
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
this : Continuous ((fun x => (↑x, toFun f x)) ∘ proj v)
x : ℝ
⊢ ((fun x => (↑x, toFun f x)) ∘ proj v) x ∈ Icc v.tMin v.tMax ×ˢ closedBall v.x₀ ↑v.R
exact ⟨(v.proj x).2, f.mem_closedBall _⟩