isMIntegralCurveOn_iff_isMIntegralCurveAt

English

For an open set s, γ is an integral curve on s iff γ is an integral curve at every t in s.

Русский

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

LaTeX

$$$\text{IsOpen}(s) \Rightarrow \mathrm{IsMIntegralCurveOn}(\gamma,v,s) \iff \forall t\in s, \mathrm{IsMIntegralCurveAt}(\gamma,v,t).$$$

Lean4

theorem isMIntegralCurveOn_iff_isMIntegralCurveAt (hs : IsOpen s) :
    IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t :=
  ⟨fun h _ ht ↦ h.isMIntegralCurveAt (hs.mem_nhds ht), IsMIntegralCurveAt.isMIntegralCurveOn⟩

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