OAI/Geometry/Relativity/CKS/AreaCuts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSArea.AmbientMat line 12
  2. abbrev OAI.CKSArea.TangentFrame line 13
  3. def OAI.CKSArea.gram line 15
  4. lemma OAI.CKSArea.gram_posDef line 17
  5. lemma OAI.CKSArea.gram_difference line 21
  6. lemma OAI.CKSArea.gram_density_lower line 25
  7. def OAI.CKSArea.chartArea line 34
  8. theorem OAI.CKSArea.chartArea_lower line 37
  9. theorem OAI.CKSArea.full_infimum_lower line 48
  10. theorem OAI.CKSArea.full_chart_infimum_lower line 54
  11. theorem OAI.CKSArea.real_full_chart_infimum_lower line 62