PicturePlanarSeparator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.planar_component_separator line 23

Source documentation

Literal genus-zero planar separator, independent of face degrees, vertex degrees, all parallel copies, and the specified vertex carrier.

theorem planar_component_separator (hG : M.GenusZero) (hc : M.underlyingGraph.Connected)
    (U : Finset M.GraphVertex) :
    ∃ S : Finset M.GraphVertex, S ⊆ U ∧ S.card ≤ 11*Nat.sqrt U.card ∧
      ∀ W : Finset M.GraphVertex, W ⊆ U → Disjoint W S →
        (M.underlyingGraph.induce (W : Set M.GraphVertex)).Preconnected →
        2*W.card ≤ U.card := by
…

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.planar_balanced_separators line 35
Source documentation
A connected genus-zero rotation system has balanced separators.
```
theorem planar_balanced_separators (hG : M.GenusZero) (hc : M.underlyingGraph.Connected) :
    HasBalancedSeparators M.underlyingGraph 11 :=
…
```