OAI/Geometry/Cannon/PlaneTopology/VertexLines.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonEmbeddedArc.Arc.finite_prescribed_star_type line 54
  2. theorem OAI.CannonEmbeddedArc.Arc.graph_face_prescribed_fan line 84
  3. structure OAI.CannonEmbeddedArc.Arc.VertexLines line 102
  4. theorem OAI.CannonEmbeddedArc.Arc.vertexLines_nonempty line 109
  5. def OAI.CannonEmbeddedArc.Arc.FaceGerm line 116
  6. instance OAI.CannonEmbeddedArc.Arc.faceGerm_finite line 121
  7. def OAI.CannonEmbeddedArc.Arc.FaceGerm.point line 126
  8. def OAI.CannonEmbeddedArc.Arc.FaceGerm.cone line 129
  9. lemma OAI.CannonEmbeddedArc.Arc.faceGerm_card line 132
  10. lemma OAI.CannonEmbeddedArc.Arc.faceGerm_at_vertex line 153
  11. theorem OAI.CannonEmbeddedArc.Arc.face_all_sector_fan line 162
  12. lemma OAI.CannonEmbeddedArc.Arc.vertex_mem_support line 205
  13. lemma OAI.CannonEmbeddedArc.Arc.vertex_parameter line 211
  14. def OAI.CannonEmbeddedArc.Arc.Faces line 219
  15. def OAI.CannonEmbeddedArc.Arc.face line 220
  16. def OAI.CannonEmbeddedArc.Arc.faceVertices line 222
  17. lemma OAI.CannonEmbeddedArc.Arc.mem_faceVertices line 225
  18. lemma OAI.CannonEmbeddedArc.Arc.face_nonempty line 230
  19. lemma OAI.CannonEmbeddedArc.Arc.face_open line 232
  20. lemma OAI.CannonEmbeddedArc.Arc.faces_finite line 238
  21. theorem OAI.CannonEmbeddedArc.Arc.face_vertex_fan line 248
  22. lemma OAI.CannonEmbeddedArc.Arc.fan_parameter_in_face line 270
  23. lemma OAI.CannonEmbeddedArc.Arc.old_fan_compatible line 278
  24. lemma OAI.CannonEmbeddedArc.Arc.different_face_fans_compatible line 294
  25. theorem OAI.CannonEmbeddedArc.Arc.global_vertex_stellation line 315