E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.51570
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * exp (K * (t - a))
⊢ f t = g t
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.51570
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t
have := dist_le_of_trajectories_ODE_of_mem_set hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.51570
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * exp (K * (t - a))
⊢ f t = g t
rwa [MulZeroClass.zero_mul, dist_le_zero] at this