OAI/Geometry/HyperbolicGroups/PictureComponentGraph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentDarts line 20
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentDarts_face line 23
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentDarts_edge line 31
  4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentPicture line 38
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentPicture_genusZero line 41
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentPicture_cycle line 45
  7. instance OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentDarts_nonempty line 51
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentPicture_connected line 58
  9. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentVertex line 73

    Source documentation

    Original graph-component vertices are carried to the actual restricted rotation system, using representatives only to define the quotient map.

    def componentVertex (v : C.supp) : (M.componentPicture C).GraphVertex :=
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.GraphVertex

  10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentVertex_class line 80
  11. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentVertex_injective line 88
  12. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.componentHom line 96
  13. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.graph_component_separator line 113

    Source documentation

    Every graph component has the separator produced by its literal restricted genus-zero map. In particular no embedding of an induced graph is being assumed.

    theorem graph_component_separator (hG : M.GenusZero) (U : Finset C.supp) :
    ∃ S : Finset C.supp, S ⊆ U ∧ S.card ≤ 11*Nat.sqrt U.card ∧
      ∀ W : Finset C.supp, W ⊆ U → Disjoint W S →
        (C.toSimpleGraph.induce (W : Set C.supp)).Preconnected → 2*W.card ≤ U.card := by
…