OAI/Geometry/ProjectionVolume/SupportGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Paper092.SupportGeometry.support line 16
  2. theorem OAI.Paper092.SupportGeometry.le_support line 18
  3. theorem OAI.Paper092.SupportGeometry.support_le line 22
  4. theorem OAI.Paper092.SupportGeometry.exists_support line 26
  5. theorem OAI.Paper092.SupportGeometry.support_add line 30
  6. theorem OAI.Paper092.SupportGeometry.support_smul line 38
  7. theorem OAI.Paper092.SupportGeometry.support_prod line 44
  8. theorem OAI.Paper092.SupportGeometry.support_sum line 56
  9. theorem OAI.Paper092.SupportGeometry.mem_iff_le_support line 75
  10. theorem OAI.Paper092.SupportGeometry.eq_of_support_eq line 83
  11. theorem OAI.Paper092.SupportGeometry.isCompact_segment line 89
  12. theorem OAI.Paper092.SupportGeometry.support_segment line 93
  13. theorem OAI.Paper092.SupportGeometry.support_centered_segment line 100
  14. theorem OAI.Paper092.SupportGeometry.support_sum_centered_segments line 107
  15. theorem OAI.Paper092.SupportGeometry.eq_sum_centered_segments_iff line 117
  16. theorem OAI.Paper092.SupportGeometry.mem_iff_inner_le_support line 139
  17. theorem OAI.Paper092.SupportGeometry.halfSpaces_eq_of_eq_support line 150
  18. theorem OAI.Paper092.SupportGeometry.eq_of_inner_support_eq line 157