Theorems · Definition · global analysis

IsMIntegralCurveOn

{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] → (ℝ → M) → ((x : M) → TangentSpace I x) → Set ℝ → Prop

If γ : ℝ → M is $C^1$ on s : Set ℝ and v is a vector field on M, IsMIntegralCurveOn γ v s means γ t is tangent to v (γ t) for all t ∈ s. The value of γ outside of s is irrelevant and considered junk.

Defined in

Mathlib.Geometry.Manifold.IntegralCurve.Basic

Cited by

31 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace