PairingTreeCotree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.subpairing_components_le line 22
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.tree_cotree line 35
Source documentation
Actual tree--cotree decomposition of each component of a genus-zero ribbon graph. Both permutations pair subsets of the original edge copies. Their supports are complementary, neither collapses parallel edges, and both spanning forests have exactly one boundary cycle per component.
```
theorem tree_cotree (hG : M.GenusZero) : ∃ 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) : ℤ) ∧
    SameCycle.setoid M.face ⊔ SameCycle.setoid (q * M.edge) = M.components ∧
    cycles (M.face * (q * M.edge)) = (Nat.card (Quotient M.components) : ℤ) := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles