OAI/Analysis/SphereIsometry/SubdivisionPointRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Coordinate compatibility of original-face restriction

  1. theorem OAI.Tingley.iterDataPoint_embedding_apply line 16
  2. theorem OAI.Tingley.iterDataPoint_embedding_eq_zero line 42
  3. theorem OAI.Tingley.lastFace_point_castSucc line 56
  4. theorem OAI.Tingley.lastFace_point_last line 60