OAI/Geometry/SurfaceImmersion/Whitney/EndpointSignModel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The simplest affine coefficient with the two prescribed endpoint signs.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.nonzeroSign line 11
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel line 13
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.nonzeroSign_mul_pos line 16
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_left line 22
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_right line 26
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_smooth line 30
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_left_mul_pos line 35
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_right_mul_pos line 40
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_same line 45
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.endpointSignModel_opposite line 53