OAI/Geometry/QuadricBundles/Charts.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.reciprocalP1_infty line 10
  2. lemma OAI.QuadricCounterexample.reciprocalP1_zero line 11
  3. lemma OAI.QuadricCounterexample.reciprocalP1_coe line 12
  4. lemma OAI.QuadricCounterexample.reciprocalP1_involutive line 15
  5. lemma OAI.QuadricCounterexample.reciprocalP1_coe_continuousAt_zero line 24
  6. lemma OAI.QuadricCounterexample.continuous_reciprocalP1 line 38
  7. def OAI.QuadricCounterexample.reciprocalP1Homeomorph line 63
  8. lemma OAI.QuadricCounterexample.affineP1_continuous line 71
  9. lemma OAI.QuadricCounterexample.affineP1_isOpenEmbedding line 76
  10. lemma OAI.QuadricCounterexample.affineP1_cover line 81
  11. lemma OAI.QuadricCounterexample.affineQuadric_isOpenEmbedding line 86
  12. lemma OAI.QuadricCounterexample.affineQuadric_cover line 90
  13. lemma OAI.QuadricCounterexample.coordP1_affine line 103
  14. lemma OAI.QuadricCounterexample.coordQuadric_affine line 106
  15. lemma OAI.QuadricCounterexample.affineP1_coord line 110
  16. lemma OAI.QuadricCounterexample.affineQuadric_coord line 115
  17. lemma OAI.QuadricCounterexample.mem_range_affineP1 line 120
  18. lemma OAI.QuadricCounterexample.powerP1_affine line 142
  19. lemma OAI.QuadricCounterexample.powerQuadric_affine line 151
  20. lemma OAI.QuadricCounterexample.powerP1_mem_range_iff line 155
  21. lemma OAI.QuadricCounterexample.mem_range_affineQuadric line 165
  22. lemma OAI.QuadricCounterexample.powerQuadric_mem_range_iff line 171
  23. def OAI.QuadricCounterexample.pullbackPolynomial line 176
  24. lemma OAI.QuadricCounterexample.baseEval_pullback line 179
  25. lemma OAI.QuadricCounterexample.power_principalChart line 187
  26. lemma OAI.QuadricCounterexample.coordP1_overlap line 204
  27. lemma OAI.QuadricCounterexample.hyperplaneTransition_mul line 219
  28. lemma OAI.QuadricCounterexample.polarizationTransition_mul line 232
  29. lemma OAI.QuadricCounterexample.baseEval_one line 244
  30. lemma OAI.QuadricCounterexample.baseEval_zero line 245
  31. lemma OAI.QuadricCounterexample.baseEval_mul line 246
  32. lemma OAI.QuadricCounterexample.algebraicallyRegular_polynomial line 249
  33. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.mono line 254
  34. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.congr line 260
  35. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.mul line 266
  36. lemma OAI.QuadricCounterexample.AlgebraicallyRegularOn.comp_power line 278
  37. lemma OAI.QuadricCounterexample.polarizationTransition_polynomial line 289
  38. lemma OAI.QuadricCounterexample.polarizationTransition_regular line 296
  39. def OAI.QuadricCounterexample.powerPullbackTwist line 300
  40. lemma OAI.QuadricCounterexample.powerPullbackTwist_spec line 334
  41. lemma OAI.QuadricCounterexample.exists_powerPullbackTwist line 338