isMIntegralCurveOn — Mathlib

English

If γ is integral at every t ∈ s, then γ is an integral curve on s.

Русский

Если γ интегрирована в каждой точке t ∈ s, то γ является интегральной кривой на s.

LaTeX

$$$\bigl(\forall t \in s, \mathrm{IsMIntegralCurveAt}(\gamma,v,t)\bigr) \Rightarrow \mathrm{IsMIntegralCurveOn}(\gamma,v,s).$$$

Lean4

/-- If `γ` is an integral curve at each `t ∈ s`, it is an integral curve on `s`. -/
theorem isMIntegralCurveOn (h : ∀ t ∈ s, IsMIntegralCurveAt γ v t) : IsMIntegralCurveOn γ v s :=
  by
  intro t ht
  apply HasMFDerivAt.hasMFDerivWithinAt
  obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
  exact h _ (mem_of_mem_nhds hs')

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