OAI/Geometry/SurfaceImmersion/Whitney/RegularArcPaths.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Paths generated by finitely many compact regular smooth arcs, with explicit subdivision, concatenation and endpoint casts.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothCompactArc.path line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothCompactArc.path_injective line 29
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothCompactArc.path_range line 36
  4. inductive OAI.ClosedSurfaceR4.FiniteOrderSmoothing.FiniteRegularPath line 53

    Source documentation

    A finite expression made from actual compact regular smooth arcs. This records the geometric pieces even when their concatenation has corners.

    inductive FiniteRegularPath (J : ModelWithCorners ℝ E H) : {x y : N} → Path x y → Prop
  | arc (P : SmoothCompactArc J N) : FiniteRegularPath J P.path
  | subpath {x y : N} {γ : Path x y} (hγ : FiniteRegularPath J γ) (s t : I) :
      FiniteRegularPath J (γ.subpath s t)
  | trans {x y z : N} {γ : Path x y} {δ : Path y z}
      (hγ : FiniteRegularPath J γ) (hδ : FiniteRegularPath J δ) :
      FiniteRegularPath J (γ.trans δ)
  | cast {x y x' y' : N} {γ : Path x y} (hγ : FiniteRegularPath J γ)
      (hx : x' = x) (hy : y' = y) : FiniteRegularPath J (γ.cast hx hy)

variable [T2Space N] {x y z : N}

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothCompactArc

  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_regular_path_last_join line 65
  6. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finite_regular_path_join line 76