English
An equivalence form: existence of a ball around t0 producing an integral curve on that ball.
Русский
Эквивалентность: существует шар вокруг t0, на котором γ интегральна.
LaTeX
$$isMIntegralCurveAt_iff' : IsMIntegralCurveAt γ v t0 ↔ ∃ ε>0, IsMIntegralCurveOn γ v (Metric.ball t0 ε)$$
Lean4
theorem isMIntegralCurveAt_iff : IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s :=
by
constructor
· intro h
rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem] at h
obtain ⟨s, hs, h⟩ := h
exact ⟨s, hs, fun t ht ↦ (h t ht).hasMFDerivWithinAt⟩
· rintro ⟨s, hs, h⟩
rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]
obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs
refine ⟨s', h2.mem_nhds h3, ?_⟩
intro t ht
apply (h t (h1 ht)).hasMFDerivAt
rw [mem_nhds_iff]
exact ⟨s', h1, h2, ht⟩
