OAI/Geometry/HeilbronnTriangle/PlaneRowTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.PlaneRowTransport.IntMatrix line 12
  2. abbrev OAI.Problem355.PlaneRowTransport.PlaneMatrices line 14
  3. def OAI.Problem355.PlaneRowTransport.rows line 16
  4. theorem OAI.Problem355.PlaneRowTransport.rows_coordinate line 24
  5. theorem OAI.Problem355.PlaneRowTransport.rows_injective line 28
  6. theorem OAI.Problem355.PlaneRowTransport.linearIndependent_of_minor_ne_zero line 37
  7. theorem OAI.Problem355.PlaneRowTransport.rows_pair_linearIndependent_of_minor line 56
  8. theorem OAI.Problem355.PlaneRowTransport.rows_span_eq_top_of_minor line 70
  9. theorem OAI.Problem355.PlaneRowTransport.norm_rows line 86
  10. theorem OAI.Problem355.PlaneRowTransport.norm_rows_le_of_coordinate_bounds line 89
  11. theorem OAI.Problem355.PlaneRowTransport.card_rows_image line 105
  12. def OAI.Problem355.PlaneRowTransport.projectedColumn line 110
  13. theorem OAI.Problem355.PlaneRowTransport.exists_minor_of_projected_columns_ne line 113
  14. theorem OAI.Problem355.PlaneRowTransport.rows_span_eq_top_of_projected_columns_ne line 131
  15. theorem OAI.Problem355.PlaneRowTransport.norm_rows_le_four_mul line 140
  16. abbrev OAI.Problem355.PlaneRowTransport.MatricesIn line 149
  17. def OAI.Problem355.PlaneRowTransport.rowsIn line 152
  18. theorem OAI.Problem355.PlaneRowTransport.rowsIn_coe line 156
  19. theorem OAI.Problem355.PlaneRowTransport.rowsIn_injective line 160
  20. theorem OAI.Problem355.PlaneRowTransport.card_rowsIn_image line 169