OAI/Combinatorics/Ramsey/CycleClique/Construction/FiveCycleGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exterior edges and two-edge paths which close to an exact five-cycle.

  1. theorem OAI.CycleClique.Construction.clique_third_vertex line 8
  2. theorem OAI.CycleClique.Construction.fiveCycle_triangle_exterior_no_edge line 15
  3. theorem OAI.CycleClique.Construction.fiveCycle_triangle_exterior_no_common line 30
  4. theorem OAI.CycleClique.Construction.fiveCycle_fourClique_exterior_disjoint line 45
  5. def OAI.CycleClique.Construction.exteriorClosedNeighborhood line 73
  6. theorem OAI.CycleClique.Construction.mem_exteriorClosedNeighborhood line 78
  7. theorem OAI.CycleClique.Construction.exteriorClosedNeighborhood_disjoint line 85
  8. theorem OAI.CycleClique.Construction.fiveCycle_exterior_closed_disjoint line 101