case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap ↔ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f : FunSpace v
⊢ range ↑toContinuousMap = {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
ext f
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap → f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}

case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → f ∈ range ↑toContinuousMap
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap ↔ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
constructor
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ ↑toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
case h.mp
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ range ↑toContinuousMap → f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
rintro ⟨⟨f, hf₀, hf_lip⟩, rfl⟩
no goals
case h.mp.intro.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf₀ : f v.t₀ = v.x₀
hf_lip : LipschitzWith v.C f
⊢ ↑toContinuousMap { toFun := f, map_t₀' := hf₀, lipschitz' := hf_lip } ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f}
exact ⟨hf₀, hf_lip⟩
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ ContinuousMap.mk f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → ContinuousMap.mk f ∈ range ↑toContinuousMap
case h.mpr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : C(↑(Icc v.tMin v.tMax), E)
⊢ f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → f ∈ range ↑toContinuousMap
rcases f with ⟨f, hf⟩
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : ↑(ContinuousMap.mk f) v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ↑(ContinuousMap.mk f)
⊢ ContinuousMap.mk f ∈ range ↑toContinuousMap
case h.mpr.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
⊢ ContinuousMap.mk f ∈ {f | ↑f v.t₀ = v.x₀ ∧ LipschitzWith v.C ↑f} → ContinuousMap.mk f ∈ range ↑toContinuousMap
rintro ⟨hf₀, hf_lip⟩
no goals
case h.mpr.mk.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f✝ : FunSpace v
f : ↑(Icc v.tMin v.tMax) → E
hf : Continuous f
hf₀ : ↑(ContinuousMap.mk f) v.t₀ = v.x₀
hf_lip : LipschitzWith v.C ↑(ContinuousMap.mk f)
⊢ ContinuousMap.mk f ∈ range ↑toContinuousMap
exact ⟨⟨f, hf₀, hf_lip⟩, rfl⟩