Vertices straddling an edge-score threshold #
A real score on the edges of a graph orders them, and a threshold t splits them into the
edges scoring below t and those scoring at least t. EdgeStraddles H score t v says that
the vertex v has incident edges on both sides of this split.
def
Algebraic.Cutwidth.Gaussian.EdgeStraddles
{W : Type}
[Fintype W]
(H : SimpleGraph W)
[DecidableRel H.Adj]
(score : Sym2 W → ℝ)
(t : ℝ)
(v : W)
:
Some edge at v scores below t and another scores at least t.
Equations
- Algebraic.Cutwidth.Gaussian.EdgeStraddles H score t v = ∃ e ∈ H.incidenceFinset v, score e < t ∧ ∃ e' ∈ H.incidenceFinset v, t ≤ score e'