Theorems · Theorem · global analysis

isMIntegralCurveOn_piecewise

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] [T2Space M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} [BoundarylessManifold I M],
  (ContMDiff I I.tangent 1 fun x => ⟨x, v x⟩) →
    ∀ {a b a' b' : ℝ},
      IsMIntegralCurveOn γ v (Set.Ioo a b) →
        IsMIntegralCurveOn γ' v (Set.Ioo a' b') →
          ∀ {t₀ : ℝ},
            t₀ ∈ Set.Ioo a b ∩ Set.Ioo a' b' →
              γ t₀ = γ' t₀ → IsMIntegralCurveOn ((Set.Ioo a b).piecewise γ γ') v (Set.Ioo a b ∪ Set.Ioo a' b')

The extension of an integral curve by another integral curve is an integral curve. If two integral curves are defined on overlapping open intervals, and they agree at a point in their common domain, then they can be patched together to form a longer integral curve. This is stated for manifolds without boundary for simplicity. We actually only need to assume that the images of γ and γ' lie in the interior of the manifold. TODO: Generalise to manifolds with boundary.

Defined in

Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Cited by

1 results in Mathlib

Foundations

Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldT2SpaceBoundarylessManifold