OAI/Geometry/SurfaceImmersion/Primitive/CrossingTargetLinear.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

An invertible target frame from two transverse planes sharing their second coordinate direction.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.baseLinear_pair line 12
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingLeft line 19
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingRight line 23
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingAxis line 27
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingLeft_apply line 30
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingRight_apply line 34
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingAxis_apply line 38
  8. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingTargetLinear line 42
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingTargetLinear_apply line 46
  10. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.crossingTargetLinear_bijective line 51