Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.PathDecomposition.Bisection.RedBlack.BridgeQuotient.Defs

The graph of components separated by designated edges #

Delete a set of designated edges and take the connected components of what remains. Two components are adjacent in the quotient when an original edge joins them. When the designated edges are bridges, this quotient is a forest, even if the contracted components themselves contain cycles. This is the contraction used in Monien and Preis's red/black tree argument.

source
def Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.graph {V : Type} (B : SimpleGraph V) (F : Set (Sym2 V)) :
SimpleGraph (B.deleteEdges F).ConnectedComponent

Contract the components remaining after deleting F, retaining the original adjacencies between distinct components.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Cutwidth.Bisection.RedBlack.BridgeQuotient.ofRegions {V ι : Type} [Fintype V] (B : SimpleGraph V) (P : ι → Finset V) :
    SimpleGraph (B.deleteEdges (⋃ (i : ι), ↑(B.cutFinset (P i)))).ConnectedComponent

    Contract the components remaining after deleting all boundaries of the given regions.

    Equations
    Instances For