OAI/Combinatorics/Progressions/Geometry/HorizontalCoordinateBounds.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DegreeRankLieFiltration.horizontalImageOfSubmodule line 14
  2. theorem OAI.Erdos3.DegreeRankLieFiltration.layerHorizontalImage_eq_of_submodule line 18
  3. theorem OAI.Erdos3.DegreeRankLieFiltration.layerHorizontalImage_eq_of_map_eq line 34
  4. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalCoordinates line 56
  5. def OAI.Erdos3.DegreeRankLieFiltration.ambientHorizontalCoordinates line 59
  6. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalCoordinates_injective line 62
  7. def OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalCoordinates line 65
  8. def OAI.Erdos3.DegreeRankLieFiltration.fourAmbientCoordinates line 69
  9. theorem OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalCoordinates_injective line 72
  10. theorem OAI.Erdos3.DegreeRankLieFiltration.fourHorizontalCoordinates_map line 77
  11. theorem OAI.Erdos3.DegreeRankLieFiltration.horizontalImage_coordinates line 83
  12. theorem OAI.Erdos3.DegreeRankLieFiltration.fourAmbientCoordinates_height line 96
  13. def OAI.Erdos3.DegreeRankLieFiltration.realFourCoordinateEquiv line 118
  14. def OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates line 122
  15. def OAI.Erdos3.DegreeRankLieFiltration.realFourAmbientCoordinates line 127
  16. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates_injective line 132
  17. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates_tensor_map line 139
  18. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates_map line 153
  19. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates_image line 160
  20. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourAmbientCoordinates_component line 172
  21. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourHorizontalCoordinates_component line 184
  22. def OAI.Erdos3.realRationalCoordinateEquiv line 211
  23. theorem OAI.Erdos3.realRationalCoordinateEquiv_tmul line 214
  24. theorem OAI.Erdos3.realFourCoordinateEquiv_tmul line 221
  25. def OAI.Erdos3.realRationalCoordinateSpan line 229
  26. def OAI.Erdos3.realFourCoordinateSpan line 232
  27. theorem OAI.Erdos3.realCoordinate_projection line 236
  28. theorem OAI.Erdos3.realFourCoordinateSpan_span line 245
  29. def OAI.Erdos3.realQuotientCoordinateMap line 280
  30. theorem OAI.Erdos3.realQuotientCoordinateMap_apply line 284
  31. theorem OAI.Erdos3.realQuotientCoordinateMap_tmul_one line 288
  32. theorem OAI.Erdos3.realQuotientCoordinateMap_eq_zero_iff line 293
  33. def OAI.Erdos3.subspaceQuotientMatrix line 306
  34. theorem OAI.Erdos3.subspaceQuotientMatrix_real_apply line 309
  35. theorem OAI.Erdos3.exists_subspace_basis_coordinates line 325
  36. theorem OAI.Erdos3.subspaceQuotientMatrix_height line 333
  37. theorem OAI.Erdos3.realRationalCoordinateSpan_span line 353
  38. theorem OAI.Erdos3.realRationalCoordinateSpan_eq_image line 372
  39. def OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates line 395
  40. theorem OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates_component line 398
  41. theorem OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates_injective line 410
  42. theorem OAI.Erdos3.DegreeRankLieFiltration.realHigherHorizontalCoordinates_image line 417
  43. def OAI.Erdos3.quotientCoordinateMatrix line 443
  44. theorem OAI.Erdos3.realQuotientCoordinateMap_eq_matrix line 447
  45. theorem OAI.Erdos3.realQuotientCoordinateMap_norm_bound line 466
  46. theorem OAI.Erdos3.realQuotientCoordinateMap_grid line 474
  47. theorem OAI.Erdos3.real_pi_projection_coordinates line 492
  48. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourAmbientCoordinates_bound line 504
  49. theorem OAI.Erdos3.DegreeRankLieFiltration.realFourAmbientCoordinates_grid line 527