OAI/Combinatorics/Progressions/Geometry/RealSubspaceCoordinateRetraction.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.real_matrix_right_inverse line 17
  2. theorem OAI.Erdos3.realification_mkQ_ker line 26
  3. theorem OAI.Erdos3.realification_mkQ_surjective line 29
  4. def OAI.Erdos3.realQuotientEquiv line 32
  5. theorem OAI.Erdos3.realQuotientEquiv_mk line 38
  6. def OAI.Erdos3.realTransportedQuotientEquiv line 44
  7. theorem OAI.Erdos3.realTransportedQuotientEquiv_mk line 48
  8. def OAI.Erdos3.realTransportedQuotientBasis line 55
  9. theorem OAI.Erdos3.realTransportedQuotientBasis_repr_mk line 60
  10. theorem OAI.Erdos3.realTransportedQuotientBasis_repr_basis line 69
  11. theorem OAI.Erdos3.rational_coordinate_map line 96
  12. theorem OAI.Erdos3.rational_coordinate_map_grid line 102
  13. theorem OAI.Erdos3.rational_coordinate_map_weighted line 108
  14. theorem OAI.Erdos3.rational_coordinate_map_weighted_exp line 121
  15. def OAI.Erdos3.rationalCoordinateSection line 148
  16. theorem OAI.Erdos3.rationalCoordinateSection_coordinates line 151
  17. theorem OAI.Erdos3.rationalCoordinateSection_grid line 155
  18. theorem OAI.Erdos3.rationalCoordinateSection_weighted line 162
  19. theorem OAI.Erdos3.rationalCoordinateSection_rightInverse line 180
  20. theorem OAI.Erdos3.scalarExtension_basis_coordinates line 203
  21. theorem OAI.Erdos3.scalarExtension_equiv_matrix line 210
  22. theorem OAI.Erdos3.scalarExtension_grid_of_height_one line 220
  23. theorem OAI.Erdos3.controlled_weighted_quotient_coordinates line 254
  24. theorem OAI.Erdos3.linearMap_coordinate_norm_le line 318
  25. theorem OAI.Erdos3.linearMap_coordinate_dist_le line 328
  26. theorem OAI.Erdos3.scalarExtension_coordinate_norm_le line 336
  27. theorem OAI.Erdos3.scalarExtension_coordinate_dist_le line 354
  28. theorem OAI.Erdos3.realified_linear_coordinate_matrix line 378
  29. theorem OAI.Erdos3.realified_linear_coordinate_norm line 386
  30. theorem OAI.Erdos3.realified_linear_coordinate_grid line 396
  31. theorem OAI.Erdos3.realified_section_correction_coordinate_norm line 404
  32. theorem OAI.Erdos3.exists_bracketLiftMatrix_leftInverse line 441
  33. def OAI.Erdos3.realSubspaceCoordinateMap line 454
  34. theorem OAI.Erdos3.realSubspaceCoordinateMap_apply line 459
  35. theorem OAI.Erdos3.realSubspaceCoordinateMap_lift line 464
  36. theorem OAI.Erdos3.lift_realSubspaceCoordinateMap line 473
  37. theorem OAI.Erdos3.realSubspaceCoordinateMap_norm line 480
  38. theorem OAI.Erdos3.realSubspaceCoordinateMap_grid line 487