OAI/Geometry/Arnold/CriticalLifts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ArnoldCounterexample.Construction.vec_five_two line 18
  2. lemma OAI.ArnoldCounterexample.Construction.vec_five_three line 19
  3. lemma OAI.ArnoldCounterexample.Construction.vec_five_four line 20
  4. def OAI.ArnoldCounterexample.Construction.zeroVector line 22
  5. def OAI.ArnoldCounterexample.Construction.otherVector line 23
  6. lemma OAI.ArnoldCounterexample.Construction.zeroVector_unit line 25
  7. lemma OAI.ArnoldCounterexample.Construction.otherVector_unit line 30
  8. def OAI.ArnoldCounterexample.Construction.zeroLift line 37
  9. def OAI.ArnoldCounterexample.Construction.plusLift line 38
  10. def OAI.ArnoldCounterexample.Construction.minusLift line 39
  11. lemma OAI.ArnoldCounterexample.Construction.zeroVector_factors line 41
  12. lemma OAI.ArnoldCounterexample.Construction.otherVector_factors line 45
  13. lemma OAI.ArnoldCounterexample.Construction.plusLift_factors line 50
  14. lemma OAI.ArnoldCounterexample.Construction.minusLift_factors line 52
  15. lemma OAI.ArnoldCounterexample.Construction.core_zeroVector line 55
  16. lemma OAI.ArnoldCounterexample.Construction.core_otherVector line 67