OAI/Geometry/HyperbolicGroups/PairingForest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.forestEdges line 21

    Source documentation

    Kruskal's spanning forest, retaining literal paired-side indices.

    def forestEdges (s : Setoid D) : List (D × D) → List (D × D)
  | [] => []
  | (a,b)::l => if s a b then forestEdges s l else (a,b)::forestEdges (glue s a b) l

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.glue

  2. lemma OAI.HyperbolicObstruction.PictureSwitch.forestEdges_sublist line 25
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.forestEdges_joins line 34
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.forestEdges_card line 46
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.forestEdges_cycles line 62
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.setoid_eq_of_card_eq line 80
  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.swap_subpair line 96
  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_mul line 106
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.swaps_subpairing line 118
  10. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.spanning_forest line 130

    Source documentation

    An actual spanning forest sub-pairing. It has precisely one boundary cycle per component; no topological drawing, tree axiom, or separator is assumed. This constructor is valid even before imposing genus zero.

    theorem spanning_forest : ∃ q : Perm D,
    (∀ x, q x = x ∨ q x = M.edge x) ∧
    SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = M.components ∧
    cycles (M.vertex * q) = (Nat.card (Quotient M.components) : ℤ) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles