OAI/Geometry/NodalSets/Charts/AdaptedChartFamilyLemmas.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Yau.Geometry.actual_connection_symmetric line 16
  2. lemma OAI.Yau.Geometry.actual_connection_cancel line 24
  3. def OAI.Yau.Geometry.actualFrameConnection line 34
  4. def OAI.Yau.Geometry.actualMetricChart line 38
  5. lemma OAI.Yau.Geometry.actualMetricChart_metric_first_zero line 42
  6. lemma OAI.Yau.Geometry.actualFrameConnection_continuous line 52
  7. theorem OAI.Yau.Geometry.exists_actual_adapted_chart_family line 59
  8. lemma OAI.Yau.Geometry.compact_family_common_radius line 117
  9. theorem OAI.Yau.Geometry.compact_quadratic_chart_domain line 129