OAI/Geometry/Relativity/CKS/BoundaryCharts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSBoundarySurface.insertNormalZero_add line 13
  2. lemma OAI.CKSBoundarySurface.insertNormalZero_smul line 18
  3. lemma OAI.CKSBoundarySurface.insertNormalZero_continuous line 23
  4. lemma OAI.CKSBoundarySurface.tangentialCoordinates_add line 36
  5. lemma OAI.CKSBoundarySurface.tangentialCoordinates_smul line 42
  6. lemma OAI.CKSBoundarySurface.tangentialCoordinates_continuous line 47
  7. lemma OAI.CKSBoundarySurface.liftPlane_zero line 53
  8. lemma OAI.CKSBoundarySurface.liftPlane_succ line 54
  9. lemma OAI.CKSBoundarySurface.dropPlane_apply line 55
  10. lemma OAI.CKSBoundarySurface.drop_lift line 56
  11. lemma OAI.CKSBoundarySurface.lift_drop line 57
  12. lemma OAI.CKSBoundarySurface.liftHalf_continuous line 63
  13. lemma OAI.CKSBoundarySurface.I3_liftHalf line 65
  14. lemma OAI.CKSBoundarySurface.boundary_iff_zero line 71
  15. lemma OAI.CKSBoundarySurface.chart_inverse_boundary line 87