OAI/Geometry/ProjectionVolume/PolytopeIncidence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper092.HPolytope.projectionVolume_le_surface line 19
  2. theorem OAI.Paper092.HPolytope.projected_face_inter_null line 30
  3. theorem OAI.Paper092.HPolytope.strict_face_point_mem_intrinsicInterior line 36
  4. def OAI.Paper092.HPolytope.badProjection line 67
  5. theorem OAI.Paper092.HPolytope.badProjection_null line 71
  6. theorem OAI.Paper092.HPolytope.strict_of_not_badProjection line 78
  7. theorem OAI.Paper092.HPolytope.affineSpan_face_of_not_badProjection line 88
  8. theorem OAI.Paper092.HPolytope.parameter_of_projection_eq line 99
  9. theorem OAI.Paper092.HPolytope.interval_of_opposite_faces line 105
  10. theorem OAI.Paper092.HPolytope.two_facet_interiors_outside_bad line 132
  11. theorem OAI.Paper092.HPolytope.ae_two_facet_interiors line 218