SubpairingDarts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.retained_contact_edge_of_covers line 20
lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.tree_retained_loopless line 29
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.tree_retained_dart_unique line 45
Source documentation
Exact oriented dart-copy uniqueness in the primal spanning tree. It is stronger than acyclicity of the simplified graph: parallel copies cannot be discarded before using a boundary-conservation argument.
```
theorem tree_retained_dart_unique (x y : D) (hx : q x ≠ x) (hy : q y ≠ y)
    (hv : M.vertexClass x = M.vertexClass y)
    (hw : M.vertexClass (M.edge x) = M.vertexClass (M.edge y)) : x = y := by
…
```