OAI/Geometry/HyperbolicGroups/ColoredApex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.sameCycle_subtypePerm_iff line 19
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.apexCount line 35
3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.apexPerm line 38
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.apexCount_eq line 41
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.color_of_sameCycle line 49
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.radial_far line 54
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_color line 63
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.apexPerm_switch line 71
9. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_apexCount line 94

   Source documentation

   The termination measure counts actual apex vertex instances, rather than all vertices: at each repeated radial-label switch this increases by one.

   theorem switch_apexCount (h : ∀ x, c (M.vertex x) = c x) {a b : D}
       (hne : a ≠ b) (hv : M.vertex.SameCycle a b)
       (ha : c a = true) (hb : c b = true)
       (hfa : c (M.edge a) = false) (hfb : c (M.edge b) = false) :
       (M.switch a b).apexCount c = M.apexCount c + 1 := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.apexCount