OAI/Geometry/HeilbronnTriangle/PlaneLines.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.PlaneLines.card_lines line 18
  2. theorem OAI.Problem355.PlaneLines.line_index line 22
  3. theorem OAI.Problem355.PlaneLines.line_preimage_index line 33
  4. theorem OAI.Problem355.PlaneLines.exists_line_containing line 41
  5. theorem OAI.Problem355.PlaneLines.exists_line_containing_rows line 53
  6. def OAI.Problem355.PlaneLines.normalMap line 60
  7. theorem OAI.Problem355.PlaneLines.normalMap_surjective line 64
  8. theorem OAI.Problem355.PlaneLines.normal_plane_finrank line 80
  9. theorem OAI.Problem355.PlaneLines.card_normal_plane_lines line 89
  10. def OAI.Problem355.PlaneLines.lineRows line 93
  11. theorem OAI.Problem355.PlaneLines.card_rows_le_lines_mul line 97
  12. def OAI.Problem355.PlaneLines.lineFiber line 122
  13. theorem OAI.Problem355.PlaneLines.card_family_le_lines_mul line 127