isMIntegralCurveAt_iff' — Mathlib

English

Local integral curve characterization around t0 as a ball around t0.

Русский

Локальная характеристика интегральной кривой вокруг t0 как шар вокруг t0.

LaTeX

$$isMIntegralCurveAt_iff'' : IsMIntegralCurveAt γ v t0 ↔ ∃ ε>0, IsMIntegralCurveOn γ v (Metric.ball t0 ε)$$

Lean4

/-- `γ` is an integral curve for `v` at `t₀` iff `γ` is an integral curve on some interval
containing `t₀`. -/
theorem isMIntegralCurveAt_iff' : IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε) :=
  by
  rw [isMIntegralCurveAt_iff]
  constructor
  · intro ⟨s, hs, h⟩
    rw [Metric.mem_nhds_iff] at hs
    obtain ⟨ε, hε, hε'⟩ := hs
    refine ⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩
  · intro ⟨ε, hε, h⟩
    exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

Похожие утверждения