OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ConcurrentAnchors.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.allowable_line_anchor line 15
  2. abbrev OAI.SimpleAmenable.VertexType line 35
  3. def OAI.SimpleAmenable.AllowableVertexLine line 37
  4. theorem OAI.SimpleAmenable.finite_vertex_anchors line 40
  5. theorem OAI.SimpleAmenable.representative_line_allowable line 58
  6. theorem OAI.SimpleAmenable.translated_vertex_anchors line 67
  7. theorem OAI.SimpleAmenable.concurrent_chart_tables_eventually line 90
  8. theorem OAI.SimpleAmenable.real_two_lines_intersect line 106
  9. theorem OAI.SimpleAmenable.real_two_lines_distance_bound line 112
  10. theorem OAI.SimpleAmenable.real_lineDet_ne_zero line 148
  11. theorem OAI.SimpleAmenable.allowable_lines_intersect line 154