OAI/Geometry/Symplectic/MorseBounds/ManifoldModel.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArnoldCounterexample.Nondegenerate.E line 13
  2. abbrev OAI.ArnoldCounterexample.Nondegenerate.model line 14
  3. structure OAI.ArnoldCounterexample.Nondegenerate.ClosedManifold line 16
  4. instance OAI.ArnoldCounterexample.Nondegenerate.(instance at line 30) line 30
  5. abbrev OAI.ArnoldCounterexample.Nondegenerate.TwoForm line 32
  6. def OAI.ArnoldCounterexample.Nondegenerate.coordinateForm line 35
  7. structure OAI.ArnoldCounterexample.Nondegenerate.SymplecticForm line 40
  8. def OAI.ArnoldCounterexample.Nondegenerate.criticalSet line 49
  9. def OAI.ArnoldCounterexample.Nondegenerate.hessian line 52
  10. def OAI.ArnoldCounterexample.Nondegenerate.IsMorse line 57
  11. def OAI.ArnoldCounterexample.Nondegenerate.morseNumber line 61
  12. def OAI.ArnoldCounterexample.Nondegenerate.rationalHomology line 65
  13. def OAI.ArnoldCounterexample.Nondegenerate.eulerChar line 69
  14. structure OAI.ArnoldCounterexample.Nondegenerate.Hamiltonian line 73
  15. def OAI.ArnoldCounterexample.Nondegenerate.fixedSet line 85
  16. def OAI.ArnoldCounterexample.Nondegenerate.IsNondegenerate line 88
  17. abbrev OAI.ArnoldCounterexample.Nondegenerate.Interval line 93
  18. def OAI.ArnoldCounterexample.Nondegenerate.intervalZero line 95
  19. def OAI.ArnoldCounterexample.Nondegenerate.intervalOne line 96
  20. def OAI.ArnoldCounterexample.Nondegenerate.ContractibleLoop line 98
  21. def OAI.ArnoldCounterexample.Nondegenerate.contractibleFixedSet line 106
  22. def OAI.ArnoldCounterexample.Nondegenerate.MainConclusion line 109
  23. lemma OAI.ArnoldCounterexample.Nondegenerate.contractibleFixedSet_subset_fixedSet line 116
  24. lemma OAI.ArnoldCounterexample.Nondegenerate.contractibleFixedSet_finite line 120
  25. theorem OAI.ArnoldCounterexample.Nondegenerate.contractibleFixedSet_ncard_le line 125
  26. theorem OAI.ArnoldCounterexample.Nondegenerate.contractibleFixedSet_ncard_lt_morseNumber line 130