SeparatorComponents.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PlanarRecursion.component_separators_union line 19

Source documentation

At most one original connected component can occupy more than half of a specified carrier. Thus a uniform separator theorem for the actual connected components extends with the SAME constant to disconnected graphs.

theorem component_separators_union (G : SimpleGraph V) (c : ℕ)
    (hcomp : ∀ C : G.ConnectedComponent, ∀ U : Finset C.supp,
      ∃ S : Finset C.supp, S ⊆ U ∧ S.card ≤ c*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)
    (U : Finset V) :
    ∃ S : Finset V, S ⊆ U ∧ S.card ≤ c*Nat.sqrt U.card ∧
      ∀ W : Finset V, W ⊆ U → Disjoint W S →
        (G.induce (W : Set V)).Preconnected → 2*W.card ≤ U.card := by
…