OAI/Geometry/HyperbolicGroups/MacroCycle.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.MacroGraph.three_points line 17

   Source documentation

   Every nonempty vertex subset all of whose vertices have two distinct neighbors in the subset contains at least three point vertices.

   theorem three_points (S : Finset Vertex) (hne : S.Nonempty)
       (hn : ∀ v ∈ S, ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ Adjacent v a ∧ Adjacent v b) :
       3 ≤ (Finset.univ.filter (fun i => point i ∈ S)).card := by
   …

   Mentions: OAI.HyperbolicObstruction.MacroGraph.Vertex, OAI.HyperbolicObstruction.MacroGraph.Adjacent, OAI.HyperbolicObstruction.MacroGraph.point

2. structure OAI.HyperbolicObstruction.MacroGraph.Polygon line 50

   Source documentation

   A cyclic simple macro polygon with at least three sides, expressed by its actual vertices and successor. The normal-form splitting must produce this data; all template bounds below are derived.

   structure Polygon where
   …

3. def OAI.HyperbolicObstruction.MacroGraph.Polygon.vertices line 61
4. def OAI.HyperbolicObstruction.MacroGraph.Polygon.points line 63
5. lemma OAI.HyperbolicObstruction.MacroGraph.Polygon.perimeter_le line 65
6. lemma OAI.HyperbolicObstruction.MacroGraph.Polygon.two_neighbors line 69
7. lemma OAI.HyperbolicObstruction.MacroGraph.Polygon.points_ge line 83