OAI/Geometry/NodalSets/Charts/TargetProductChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.modelCoordinateEquiv line 12
  2. def OAI.Yau.Target.productChart line 16
  3. def OAI.Yau.Target.productChartInverse line 20
  4. def OAI.Yau.Target.productChartDomain line 23
  5. lemma OAI.Yau.Target.productChart_inverse_mem line 26
  6. lemma OAI.Yau.Target.productChart_right_inv line 31
  7. lemma OAI.Yau.Target.productChart_contMDiffOn line 38
  8. lemma OAI.Yau.Target.productChartInverse_continuousOn line 50
  9. lemma OAI.Yau.Target.compact_productChart_extension line 57