OAI/Geometry/QuadricBundles/Equalizer.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.QuadricCounterexample.EqualizerData line 9
  2. def OAI.QuadricCounterexample.EqualizerData.topFactor line 25
  3. def OAI.QuadricCounterexample.EqualizerData.quotientFactor line 26
  4. def OAI.QuadricCounterexample.EqualizerData.bottomFactor line 27
  5. def OAI.QuadricCounterexample.EqualizerData.numerator line 30
  6. lemma OAI.QuadricCounterexample.EqualizerData.topFactor_regular line 34
  7. lemma OAI.QuadricCounterexample.EqualizerData.quotientFactor_regular line 36
  8. lemma OAI.QuadricCounterexample.EqualizerData.bottomFactor_regular line 38
  9. lemma OAI.QuadricCounterexample.EqualizerData.numerator_regular line 43
  10. lemma OAI.QuadricCounterexample.EqualizerData.exists_low line 51
  11. def OAI.QuadricCounterexample.EqualizerData.low line 59
  12. lemma OAI.QuadricCounterexample.EqualizerData.low_regular line 60
  13. lemma OAI.QuadricCounterexample.EqualizerData.low_spec line 62
  14. lemma OAI.QuadricCounterexample.EqualizerData.divisor_factor line 65
  15. lemma OAI.QuadricCounterexample.EqualizerData.topFactor_mul line 74
  16. lemma OAI.QuadricCounterexample.EqualizerData.quotientFactor_mul line 79
  17. lemma OAI.QuadricCounterexample.EqualizerData.bottomFactor_mul line 84
  18. lemma OAI.QuadricCounterexample.EqualizerData.numerator_mul line 92
  19. lemma OAI.QuadricCounterexample.EqualizerData.low_mul line 114
  20. lemma OAI.QuadricCounterexample.EqualizerData.topFactor_self line 131
  21. lemma OAI.QuadricCounterexample.EqualizerData.quotientFactor_self line 133
  22. lemma OAI.QuadricCounterexample.EqualizerData.bottomFactor_self line 135
  23. lemma OAI.QuadricCounterexample.EqualizerData.coordinateOverlap_self line 137
  24. lemma OAI.QuadricCounterexample.EqualizerData.low_self line 140
  25. def OAI.QuadricCounterexample.EqualizerData.coordinateTransition line 149
  26. lemma OAI.QuadricCounterexample.EqualizerData.coordinateTransition_self line 152
  27. lemma OAI.QuadricCounterexample.EqualizerData.coordinateTransition_mul line 156
  28. lemma OAI.QuadricCounterexample.EqualizerData.coordinateTransition_regular line 166
  29. def OAI.QuadricCounterexample.standardChartNat line 182
  30. def OAI.QuadricCounterexample.standardEquationNat line 184
  31. lemma OAI.QuadricCounterexample.standardChartNat_surj line 186
  32. lemma OAI.QuadricCounterexample.principalChart_one line 194
  33. lemma OAI.QuadricCounterexample.standardCharts_cover line 197
  34. def OAI.QuadricCounterexample.EqualizerData.globalTransition line 208
  35. lemma OAI.QuadricCounterexample.EqualizerData.globalTransition_self line 211
  36. lemma OAI.QuadricCounterexample.EqualizerData.coord_mem_overlap line 214
  37. lemma OAI.QuadricCounterexample.EqualizerData.globalTransition_mul line 220
  38. def OAI.QuadricCounterexample.EqualizerData.bundle line 229
  39. def OAI.QuadricCounterexample.EqualizerData.inclusionMatrix line 247
  40. lemma OAI.QuadricCounterexample.EqualizerData.inclusionMatrix_change line 250
  41. lemma OAI.QuadricCounterexample.EqualizerData.second_projection_surjective line 262
  42. lemma OAI.QuadricCounterexample.EqualizerData.inclusionMatrix_det line 275