OAI/Geometry/NodalSets/Elliptic/SeedRoundPatch.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Yau.Target.seedChartAmbient line 12
  2. lemma OAI.Yau.Target.seedChartAmbient_smooth line 15
  3. lemma OAI.Yau.Target.seedChartAmbient_zero line 20
  4. lemma OAI.Yau.Target.seedRealChart_smoothAt_zero line 23
  5. lemma OAI.Yau.Target.seedImagChart_smoothAt_zero line 28
  6. lemma OAI.Yau.Target.seedImagChart_differential_ne_zero line 33
  7. def OAI.Yau.Target.seedRoundAdmissible line 43
  8. lemma OAI.Yau.Target.seedRoundAdmissible_eventually line 50
  9. theorem OAI.Yau.Target.seed_round_compact_patch line 64