OAI/Geometry/HyperbolicGroups/PictureVertexCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.incident_darts_card line 21
2. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.relative_cuts_le_separator line 37

   Source documentation

   Recover the true multigraph cut count from a vertex separator in the underlying simple graph. Every unordered edge copy is retained; multiple contacts inject into distinct incident darts of separator vertices.

   theorem relative_cuts_le_separator (active : D → Prop) (part : M.GraphVertex → I)
       (S : Finset M.GraphVertex) (d : ℕ)
       (hdegree : ∀ v ∈ S, Nat.card {x : D // M.vertexClass x = v} ≤ d)
       (hhit : ∀ x, active x → active (M.edge x) →
         part (M.vertexClass x) ≠ part (M.vertexClass (M.edge x)) →
         M.vertexClass x ∈ S ∨ M.vertexClass (M.edge x) ∈ S) :
       Fintype.card (RelativeCutContact M active (part ∘ M.vertexClass)) ≤ d * S.card := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.RelativeCutContact