isMIntegralCurve_iff_isMIntegralCurveOn

English

If γ is an integral curve, then γ is an integral curve on any subset s.

Русский

Если γ является интегральной кривой, то она является интегральной кривой на любом подмножество s.

LaTeX

$$isMIntegralCurveOn (h : IsMIntegralCurve γ v) (s : Set Real) : IsMIntegralCurveOn γ v s$$

Lean4

theorem isMIntegralCurve_iff_isMIntegralCurveOn : IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v univ :=
  ⟨fun h ↦ h.isMIntegralCurveOn _, fun h t ↦ (h t (mem_univ _)).hasMFDerivAt Filter.univ_mem⟩

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