OAI/Geometry/SurfaceImmersion/Primitive/GenericPhaseCrossing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The generic covectors selected in ordinary coordinates are the first rows of the actual phase transitions.

  1. lemma OAI.ClosedSurfaceR4.phaseTransition_refl_first line 18
  2. lemma OAI.ClosedSurfaceR4.phaseTransition_refl_covector line 29
  3. lemma OAI.ClosedSurfaceR4.centeredPhase_first line 50
  4. theorem OAI.ClosedSurfaceR4.generic_phase_crossing_first_nonzero line 58