OAI/Geometry/HyperbolicGroups/GraphSeparatorTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PlanarRecursion.preconnected_image line 15
2. theorem OAI.HyperbolicObstruction.PlanarRecursion.component_separator_pullback line 29

   Source documentation

   Stability of the actual component-separator conclusion under an injective graph homomorphism; separator vertices outside the given carrier are not charged.

   theorem component_separator_pullback (G : SimpleGraph V) (H : SimpleGraph W)
       (f : G →g H) (hinj : Function.Injective f) (c : ℕ)
       (hH : ∀ U : Finset W, ∃ S : Finset W, S ⊆ U ∧ S.card ≤ c*Nat.sqrt U.card ∧
         ∀ A : Finset W, A ⊆ U → Disjoint A S →
           (H.induce (A : Set W)).Preconnected → 2*A.card ≤ U.card)
       (U : Finset V) :
       ∃ S : Finset V, S ⊆ U ∧ S.card ≤ c*Nat.sqrt U.card ∧
         ∀ A : Finset V, A ⊆ U → Disjoint A S →
           (G.induce (A : Set V)).Preconnected → 2*A.card ≤ U.card := by
   …