st-numberings and bipolar acyclic orientations of simple graphs

An st-numbering of a finite simple graph G on V with chosen source s and sink t is a bijection V ≃ Fin (Fintype.card V) assigning 0 to s and Fintype.card V - 1 to t such that every vertex other than s and t has both a lower-numbered neighbour and a higher-numbered neighbour. Directing each edge from its lower-numbered endpoint to its higher-numbered endpoint yields a bipolar acyclic orientation of G: it has no positive-length directed closed paths, and whenever G is preconnected (in particular whenever s and t are adjacent or V has at least three vertices), s is the unique source, t is the unique sink, and every vertex lies on a directed path from s to t.

On a finite vertex type with at least three vertices and s ≠ t, Lempel, Even, and Cederbaum characterized the existence of an st-numbering by 2-vertex-connectivity of G ⊔ edge s t (and hence of G itself when G.Adj s t). The existence direction is proved here by iteratively attaching open ears to a partial vertex list starting at [s, t] via the fan lemma (SimpleGraph.IsVertexConnected.exists_fan), inserting the internal vertices of each new ear between its two attachment vertices.

Main definitions

• SimpleGraph.STNumbering G s t: a bijective numbering V ≃ Fin (Fintype.card V) placing s first, t last, and giving every other vertex both a lower-numbered and a higher-numbered neighbour.
• SimpleGraph.STNumbering.symm, SimpleGraph.STNumbering.symmEquiv: order reversal on Fin (Fintype.card V), exchanging s and t.
• SimpleGraph.STNumbering.map, SimpleGraph.Iso.stNumberingEquiv: transport of st-numberings along graph isomorphisms.
• SimpleGraph.STNumbering.mapLe: transport of an st-numbering to a supergraph on the same vertex type.
• SimpleGraph.STNumbering.toOrientation: the TauCeti.DoubledQuiver.Orientation directing each edge toward its higher-numbered endpoint.
• SimpleGraph.STNumbering.arrow, SimpleGraph.STNumbering.homEquiv: arrow transport between OrientedQuiver G n.toOrientation and adjacency with strict numbering inequality.

Main results

• SimpleGraph.STNumbering.isAcyclic_toOrientation: the induced orientation is acyclic.
• SimpleGraph.STNumbering.preconnected_of_reachable, SimpleGraph.STNumbering.connected_of_reachable: when t is reachable from s (in particular when G.Adj s t or 3 ≤ Fintype.card V), G is preconnected and connected.
• SimpleGraph.STNumbering.isSource_source, SimpleGraph.STNumbering.isSink_sink, SimpleGraph.STNumbering.nonempty_path_from_source, SimpleGraph.STNumbering.nonempty_path_to_sink, SimpleGraph.STNumbering.isSource_iff, SimpleGraph.STNumbering.isSink_iff: s is a source and t is a sink of OrientedQuiver G n.toOrientation; when G is preconnected, every vertex is reachable from s and can reach t, s is the unique source, and t is the unique sink (together with the graph-level neighbour characterizations forall_not_adj_and_numbering_lt_iff and forall_not_adj_and_lt_numbering_iff).
• SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two_sup_edge, SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two, SimpleGraph.IsVertexConnected.nonempty_stNumbering: Lempel–Even–Cederbaum theorem: on at least three vertices with s ≠ t, G admits an st-numbering if and only if G ⊔ SimpleGraph.edge s t is 2-vertex-connected.

References

• A. Lempel, S. Even, and I. Cederbaum, An algorithm for planarity testing of graphs, in Theory of Graphs: International Symposium (Rome, 1966), Gordon and Breach, New York, 1967, 215–232.
• S. Even and R. E. Tarjan, Computing an st-numbering, Theor. Comput. Sci. 2 (1976), 339–344, Theorem 1.
• R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017.

structure SimpleGraph.STNumbering {V : Type u} (G : SimpleGraph V) [Fintype V] (s t : V) : Type u

An st-numbering of a finite simple graph G with source s and sink t is a bijection V ≃ Fin (Fintype.card V) sending s to 0 and t to Fintype.card V - 1 such that every vertex other than s and t has both a lower-numbered neighbour and a higher-numbered neighbour.

• numbering : V ≃ Fin (Fintype.card V)

  The bijective numbering of the vertices by Fin (Fintype.card V).

• source_first : ↑(self.numbering s) = 0

  The source s receives number 0.

• sink_last : ↑(self.numbering t) + 1 = Fintype.card V

  The sink t receives number Fintype.card V - 1.

• lower_neighbor ⦃v : V⦄ : v ≠ s → v ≠ t → ∃ (u : V), G.Adj u v ∧ self.numbering u < self.numbering v

  Every vertex other than s and t has a lower-numbered neighbour.

• higher_neighbor ⦃v : V⦄ : v ≠ s → v ≠ t → ∃ (w : V), G.Adj v w ∧ self.numbering v < self.numbering w

  Every vertex other than s and t has a higher-numbered neighbour.

Basic numbering API

theorem SimpleGraph.STNumbering.ext {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {n₁ n₂ : G.STNumbering s t} (h : ∀ (v : V), n₁.numbering v = n₂.numbering v) : n₁ = n₂

Two st-numberings are equal when they assign the same index to every vertex.

theorem SimpleGraph.STNumbering.ext_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {n₁ n₂ : G.STNumbering s t} : n₁ = n₂ ↔ ∀ (v : V), n₁.numbering v = n₂.numbering v

theorem SimpleGraph.STNumbering.ext_val {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {n₁ n₂ : G.STNumbering s t} (h : ∀ (v : V), ↑(n₁.numbering v) = ↑(n₂.numbering v)) : n₁ = n₂

Two st-numberings are equal when they assign the same natural number to every vertex.

theorem SimpleGraph.STNumbering.val_numbering_injective {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : Function.Injective fun (v : V) => ↑(n.numbering v)

The natural-number values of an st-numbering are injective.

theorem SimpleGraph.STNumbering.nonempty {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} : ∀ (x : G.STNumbering s t), Nonempty V

A graph admitting an st-numbering has a nonempty vertex type.

theorem SimpleGraph.STNumbering.card_pos {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : 0 < Fintype.card V

A graph admitting an st-numbering has positive vertex count.

@[simp]

theorem SimpleGraph.STNumbering.val_numbering_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : ↑(n.numbering s) = 0

@[simp]

theorem SimpleGraph.STNumbering.val_numbering_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : ↑(n.numbering t) = Fintype.card V - 1

theorem SimpleGraph.STNumbering.numbering_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : n.numbering s = ⟨0, ⋯⟩

Explicit Fin value of the source in an st-numbering.

theorem SimpleGraph.STNumbering.numbering_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : n.numbering t = ⟨Fintype.card V - 1, ⋯⟩

Explicit Fin value of the sink in an st-numbering.

@[simp]

theorem SimpleGraph.STNumbering.val_numbering_eq_zero_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} : ↑(n.numbering v) = 0 ↔ v = s

A vertex receives number 0 if and only if it is the source s.

@[simp]

theorem SimpleGraph.STNumbering.val_numbering_eq_card_sub_one_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} : ↑(n.numbering v) = Fintype.card V - 1 ↔ v = t

A vertex receives number Fintype.card V - 1 if and only if it is the sink t.

theorem SimpleGraph.STNumbering.source_eq_sink_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : s = t ↔ Fintype.card V = 1

In an st-numbering, s = t holds exactly when the graph has a single vertex.

theorem SimpleGraph.STNumbering.source_ne_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} [Nontrivial V] (n : G.STNumbering s t) : s ≠ t

On a nontrivial vertex type, the source and sink of an st-numbering are distinct.

theorem SimpleGraph.STNumbering.numbering_source_le {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : n.numbering s ≤ n.numbering v

The source s has the minimum number among all vertices.

@[simp]

theorem SimpleGraph.STNumbering.not_lt_numbering_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : ¬n.numbering v < n.numbering s

@[simp]

theorem SimpleGraph.STNumbering.numbering_source_lt_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} : n.numbering s < n.numbering v ↔ v ≠ s

A vertex has strictly larger number than s if and only if it is distinct from s.

theorem SimpleGraph.STNumbering.le_numbering_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : n.numbering v ≤ n.numbering t

The sink t has the maximum number among all vertices.

@[simp]

theorem SimpleGraph.STNumbering.not_numbering_sink_lt {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : ¬n.numbering t < n.numbering v

@[simp]

theorem SimpleGraph.STNumbering.lt_numbering_sink_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} : n.numbering v < n.numbering t ↔ v ≠ t

A vertex has strictly smaller number than t if and only if it is distinct from t.

Endpoint copy, reversal, supergraph transport, and isomorphism transport

def SimpleGraph.STNumbering.copy {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {s' t' : V} (hs : s = s') (ht : t = t') : G.STNumbering s' t'

Copy an st-numbering across equalities of its source and sink vertices.

@[simp]

theorem SimpleGraph.STNumbering.copy_numbering {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {s' t' : V} (hs : s = s') (ht : t = t') : (n.copy hs ht).numbering = n.numbering

@[simp]

theorem SimpleGraph.STNumbering.copy_rfl {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : n.copy ⋯ ⋯ = n

def SimpleGraph.STNumbering.symm {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : G.STNumbering t s

Reverse an st-numbering via Fin.revPerm, exchanging the source s and the sink t.

@[simp]

theorem SimpleGraph.STNumbering.symm_numbering_apply {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : n.symm.numbering v = (n.numbering v).rev

theorem SimpleGraph.STNumbering.val_symm_numbering {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (v : V) : ↑(n.symm.numbering v) = Fintype.card V - 1 - ↑(n.numbering v)

Explicit natural-number formula for the reversed st-numbering.

@[simp]

theorem SimpleGraph.STNumbering.symm_symm {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : n.symm.symm = n

@[simp]

theorem SimpleGraph.STNumbering.symm_copy {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {s' t' : V} (hs : s = s') (ht : t = t') : (n.copy hs ht).symm = n.symm.copy ht hs

def SimpleGraph.STNumbering.symmEquiv {V : Type u} [Fintype V] (G : SimpleGraph V) (s t : V) : G.STNumbering s t ≃ G.STNumbering t s

Reversing the order on Fin (Fintype.card V) identifies st-numberings with ts-numberings.

@[simp]

theorem SimpleGraph.STNumbering.symmEquiv_apply {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : (symmEquiv G s t) n = n.symm

@[simp]

theorem SimpleGraph.STNumbering.symmEquiv_symm {V : Type u} [Fintype V] (G : SimpleGraph V) (s t : V) : (symmEquiv G s t).symm = symmEquiv G t s

def SimpleGraph.STNumbering.mapLe {V : Type u} [Fintype V] {G H : SimpleGraph V} {s t : V} (hGH : G ≤ H) (n : G.STNumbering s t) : H.STNumbering s t

Transport an st-numbering to a supergraph on the same vertex type.

@[simp]

theorem SimpleGraph.STNumbering.mapLe_numbering {V : Type u} [Fintype V] {G H : SimpleGraph V} {s t : V} (hGH : G ≤ H) (n : G.STNumbering s t) : (mapLe hGH n).numbering = n.numbering

@[simp]

theorem SimpleGraph.STNumbering.mapLe_refl {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : mapLe ⋯ n = n

@[simp]

theorem SimpleGraph.STNumbering.mapLe_mapLe {V : Type u} [Fintype V] {G H : SimpleGraph V} {s t : V} {K : SimpleGraph V} (hGH : G ≤ H) (hHK : H ≤ K) (n : G.STNumbering s t) : mapLe hHK (mapLe hGH n) = mapLe ⋯ n

Supergraph transport of st-numberings composes transitively.

@[simp]

theorem SimpleGraph.STNumbering.symm_mapLe {V : Type u} [Fintype V] {G H : SimpleGraph V} {s t : V} (hGH : G ≤ H) (n : G.STNumbering s t) : (mapLe hGH n).symm = mapLe hGH n.symm

def SimpleGraph.STNumbering.map {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {W : Type u_1} [Fintype W] {G' : SimpleGraph W} (n : G.STNumbering s t) (e : G ≃g G') : G'.STNumbering (e s) (e t)

Transport an st-numbering along a graph isomorphism.

@[simp]

theorem SimpleGraph.STNumbering.val_map_numbering {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {W : Type u_1} [Fintype W] {G' : SimpleGraph W} (n : G.STNumbering s t) (e : G ≃g G') (w : W) : ↑((n.map e).numbering w) = ↑(n.numbering (e.symm w))

theorem SimpleGraph.STNumbering.val_map_numbering_apply {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {W : Type u_1} [Fintype W] {G' : SimpleGraph W} (n : G.STNumbering s t) (e : G ≃g G') (v : V) : ↑((n.map e).numbering (e v)) = ↑(n.numbering v)

Evaluating n.map e at e v recovers the natural-number index of v.

@[simp]

theorem SimpleGraph.STNumbering.map_refl {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : n.map Iso.refl = n

theorem SimpleGraph.STNumbering.map_trans {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {W : Type u_1} {X : Type u_2} [Fintype W] [Fintype X] {G' : SimpleGraph W} {G'' : SimpleGraph X} (n : G.STNumbering s t) (e₁ : G ≃g G') (e₂ : G' ≃g G'') : (n.map e₁).map e₂ = n.map (RelIso.trans e₁ e₂)

Transport of st-numberings along graph isomorphisms composes functorially.

@[simp]

theorem SimpleGraph.STNumbering.symm_map {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} {W : Type u_1} [Fintype W] {G' : SimpleGraph W} (n : G.STNumbering s t) (e : G ≃g G') : (n.map e).symm = n.symm.map e

def SimpleGraph.Iso.stNumberingEquiv {V : Type u} [Fintype V] {W : Type u_1} [Fintype W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (s t : V) : G.STNumbering s t ≃ H.STNumbering (e s) (e t)

A graph isomorphism induces an equivalence of st-numberings.

@[simp]

theorem SimpleGraph.Iso.stNumberingEquiv_apply {V : Type u} [Fintype V] {W : Type u_1} [Fintype W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (s t : V) (n : G.STNumbering s t) : (e.stNumberingEquiv s t) n = n.map e

@[simp]

theorem SimpleGraph.Iso.val_stNumberingEquiv_symm_numbering {V : Type u} [Fintype V] {W : Type u_1} [Fintype W] {G : SimpleGraph V} {H : SimpleGraph W} (e : G ≃g H) (s t : V) (m : H.STNumbering (e s) (e t)) (v : V) : ↑(((e.stNumberingEquiv s t).symm m).numbering v) = ↑(m.numbering (e v))

Induced bipolar orientation and quiver transport

def SimpleGraph.STNumbering.toOrientation {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : TauCeti.DoubledQuiver.Orientation G

The orientation induced by an st-numbering, directing every edge from its lower-numbered endpoint to its higher-numbered endpoint.

@[simp]

theorem SimpleGraph.STNumbering.mem_toOrientation {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (d : G.Dart) : d ∈ n.toOrientation ↔ n.numbering d.toProd.1 < n.numbering d.toProd.2

A dart belongs to n.toOrientation exactly when its first endpoint has a strictly smaller number than its second endpoint.

@[simp]

theorem SimpleGraph.STNumbering.toOrientation_copy {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {s' t' : V} (hs : s = s') (ht : t = t') : (n.copy hs ht).toOrientation = n.toOrientation

theorem SimpleGraph.STNumbering.mem_symm_toOrientation {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (d : G.Dart) : d ∈ n.symm.toOrientation ↔ d.symm ∈ n.toOrientation

Reversing an st-numbering reverses every dart of its induced orientation.

def SimpleGraph.STNumbering.arrow {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {u v : V} (h : G.Adj u v) (hlt : n.numbering u < n.numbering v) : TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation u ⟶ TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v

Construct the oriented-quiver arrow over an edge directed toward its higher-numbered endpoint.

def SimpleGraph.STNumbering.homEquiv {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (u v : V) : (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation u ⟶ TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v) ≃ { x : G.Adj u v // n.numbering u < n.numbering v }

Transport arrows of OrientedQuiver G n.toOrientation across OrientedQuiver.homEquiv to pairs of an adjacency proof and a strict numbering inequality.

@[simp]

theorem SimpleGraph.STNumbering.homEquiv_arrow {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {u v : V} (h : G.Adj u v) (hlt : n.numbering u < n.numbering v) : (n.homEquiv u v) (n.arrow h hlt) = ⟨h, hlt⟩

@[simp]

theorem SimpleGraph.STNumbering.homEquiv_symm_apply {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {u v : V} (h : G.Adj u v) (hlt : n.numbering u < n.numbering v) : (n.homEquiv u v).symm ⟨h, hlt⟩ = n.arrow h hlt

theorem SimpleGraph.STNumbering.nonempty_hom_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {u v : V} : Nonempty (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation u ⟶ TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v) ↔ G.Adj u v ∧ n.numbering u < n.numbering v

An arrow from u to v exists in OrientedQuiver G n.toOrientation if and only if u and v are adjacent with n.numbering u < n.numbering v.

theorem SimpleGraph.STNumbering.isEmpty_hom_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {u v : V} : IsEmpty (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation u ⟶ TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v) ↔ ¬(G.Adj u v ∧ n.numbering u < n.numbering v)

There is no arrow from u to v in OrientedQuiver G n.toOrientation if and only if u and v are not adjacent with n.numbering u < n.numbering v.

theorem SimpleGraph.STNumbering.isAcyclic_toOrientation {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : TauCeti.Quiver.IsAcyclic (TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation)

The orientation induced by an st-numbering is acyclic.

theorem SimpleGraph.STNumbering.numbering_le_of_path {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {x y : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation} (p : Quiver.Path x y) : n.numbering ((TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv G n.toOrientation).symm x) ≤ n.numbering ((TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv G n.toOrientation).symm y)

Along any directed path in OrientedQuiver G n.toOrientation, vertex numbers are monotone.

theorem SimpleGraph.STNumbering.numbering_lt_of_path_of_length_pos {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {x y : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation} (p : Quiver.Path x y) (hp : 0 < p.length) : n.numbering ((TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv G n.toOrientation).symm x) < n.numbering ((TauCeti.DoubledQuiver.OrientedQuiver.vertexEquiv G n.toOrientation).symm y)

Along any positive-length directed path in OrientedQuiver G n.toOrientation, the endpoint number is strictly greater than the start number.

Monotone walks, source, sink, and directed reachability

theorem SimpleGraph.STNumbering.exists_walk_from_source_of_ne_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} (hvt : v ≠ t) : ∃ (p : G.Walk s v), ∀ x ∈ p.support, n.numbering x ≤ n.numbering v

Every vertex v ≠ t is joined from s by a walk in G whose vertices all have numbers at most n.numbering v.

theorem SimpleGraph.STNumbering.exists_walk_to_sink_of_ne_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} (hvs : v ≠ s) : ∃ (p : G.Walk v t), ∀ x ∈ p.support, n.numbering v ≤ n.numbering x

Every vertex v ≠ s is joined to t by a walk in G whose vertices all have numbers at least n.numbering v.

theorem SimpleGraph.STNumbering.preconnected_of_reachable {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hst : G.Reachable s t) : G.Preconnected

If t is reachable from s, any graph admitting an st-numbering is preconnected.

theorem SimpleGraph.STNumbering.connected_of_reachable {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hst : G.Reachable s t) : G.Connected

If t is reachable from s, any graph admitting an st-numbering is connected.

theorem SimpleGraph.STNumbering.preconnected_of_adj {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hst : G.Adj s t) : G.Preconnected

If s and t are adjacent, any graph admitting an st-numbering is preconnected.

theorem SimpleGraph.STNumbering.connected_of_adj {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hst : G.Adj s t) : G.Connected

If s and t are adjacent, any graph admitting an st-numbering is connected.

theorem SimpleGraph.STNumbering.preconnected_of_three_le_card {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (h3 : 3 ≤ Fintype.card V) : G.Preconnected

On at least three vertices, any graph admitting an st-numbering is preconnected, even if s and t are not adjacent.

theorem SimpleGraph.STNumbering.connected_of_three_le_card {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (h3 : 3 ≤ Fintype.card V) : G.Connected

On at least three vertices, any graph admitting an st-numbering is connected.

theorem SimpleGraph.STNumbering.isSource_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : TauCeti.Quiver.IsSource (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation s)

The vertex s is a quiver source of OrientedQuiver G n.toOrientation.

theorem SimpleGraph.STNumbering.isSink_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) : TauCeti.Quiver.IsSink (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation t)

The vertex t is a quiver sink of OrientedQuiver G n.toOrientation.

theorem SimpleGraph.STNumbering.nonempty_path_from_source_of_ne_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} (hvt : v ≠ t) : Nonempty (Quiver.Path (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation s) (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v))

Every vertex v ≠ t is reachable from s in OrientedQuiver G n.toOrientation (with no connectedness hypothesis on G).

theorem SimpleGraph.STNumbering.nonempty_path_to_sink_of_ne_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) {v : V} (hvs : v ≠ s) : Nonempty (Quiver.Path (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation v) (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation t))

Every vertex v ≠ s can reach t in OrientedQuiver G n.toOrientation (with no connectedness hypothesis on G).

theorem SimpleGraph.STNumbering.nonempty_path_source_sink_of_preconnected {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) : Nonempty (Quiver.Path (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation s) (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation t))

When G is preconnected, OrientedQuiver G n.toOrientation has a directed path from s to t.

theorem SimpleGraph.STNumbering.nonempty_path_from_source {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) (x : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation) : Nonempty (Quiver.Path (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation s) x)

When G is preconnected, every vertex of OrientedQuiver G n.toOrientation is reachable from s.

theorem SimpleGraph.STNumbering.nonempty_path_to_sink {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) (x : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation) : Nonempty (Quiver.Path x (TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation t))

When G is preconnected, every vertex of OrientedQuiver G n.toOrientation can reach t.

theorem SimpleGraph.STNumbering.isSource_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) {x : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation} : TauCeti.Quiver.IsSource x ↔ x = TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation s

When G is preconnected, s is the unique source of OrientedQuiver G n.toOrientation.

theorem SimpleGraph.STNumbering.isSink_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) {x : TauCeti.DoubledQuiver.OrientedQuiver G n.toOrientation} : TauCeti.Quiver.IsSink x ↔ x = TauCeti.DoubledQuiver.OrientedQuiver.vertex G n.toOrientation t

When G is preconnected, t is the unique sink of OrientedQuiver G n.toOrientation.

theorem SimpleGraph.STNumbering.forall_not_adj_and_numbering_lt_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) {v : V} : (∀ (u : V), ¬(G.Adj u v ∧ n.numbering u < n.numbering v)) ↔ v = s

When G is preconnected, s is the unique vertex with no lower-numbered neighbour.

theorem SimpleGraph.STNumbering.forall_not_adj_and_lt_numbering_iff {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (hG : G.Preconnected) {v : V} : (∀ (w : V), ¬(G.Adj v w ∧ n.numbering v < n.numbering w)) ↔ v = t

When G is preconnected, t is the unique vertex with no higher-numbered neighbour.

2-vertex-connectivity from an st-numbering

theorem SimpleGraph.STNumbering.isVertexConnected_two_sup_edge {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (h3 : 3 ≤ Fintype.card V) : (G ⊔ edge s t).IsVertexConnected 2

On at least three vertices, admitting an st-numbering makes G ⊔ SimpleGraph.edge s t 2-vertex-connected.

theorem SimpleGraph.STNumbering.isVertexConnected_two {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (n : G.STNumbering s t) (h3 : 3 ≤ Fintype.card V) (hst : G.Adj s t) : G.IsVertexConnected 2

On at least three vertices with G.Adj s t, admitting an st-numbering makes G itself 2-vertex-connected.

Existence of st-numberings via open-ear insertion

theorem SimpleGraph.nonempty_stNumbering_of_isVertexConnected_two_sup_edge {V : Type u} [Fintype V] {G : SimpleGraph V} {s t : V} (hst : s ≠ t) (hG : (G ⊔ edge s t).IsVertexConnected 2) : Nonempty (G.STNumbering s t)

Lempel–Even–Cederbaum theorem (existence). Let s ≠ t be distinct vertices of a finite simple graph G such that G ⊔ SimpleGraph.edge s t is 2-vertex-connected. Then G admits an st-numbering.

theorem SimpleGraph.IsVertexConnected.nonempty_stNumbering_of_ne {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : G.IsVertexConnected 2) {s t : V} (hst : s ≠ t) : Nonempty (G.STNumbering s t)

Any 2-vertex-connected finite simple graph admits an st-numbering between any two distinct vertices s ≠ t.

theorem SimpleGraph.IsVertexConnected.nonempty_stNumbering {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : G.IsVertexConnected 2) {s t : V} (hst : G.Adj s t) : Nonempty (G.STNumbering s t)

Any 2-vertex-connected finite simple graph admits an st-numbering across any chosen edge G.Adj s t.

theorem SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two_sup_edge {V : Type u} [Fintype V] {G : SimpleGraph V} (h3 : 3 ≤ Fintype.card V) {s t : V} (hst : s ≠ t) : Nonempty (G.STNumbering s t) ↔ (G ⊔ edge s t).IsVertexConnected 2

Lempel–Even–Cederbaum theorem. On a finite vertex type with at least three vertices, a simple graph G admits an st-numbering for distinct vertices s ≠ t if and only if G ⊔ SimpleGraph.edge s t is 2-vertex-connected.

theorem SimpleGraph.nonempty_stNumbering_iff_isVertexConnected_two {V : Type u} [Fintype V] {G : SimpleGraph V} (h3 : 3 ≤ Fintype.card V) {s t : V} (hst : G.Adj s t) : Nonempty (G.STNumbering s t) ↔ G.IsVertexConnected 2

Lempel–Even–Cederbaum theorem for adjacent endpoints. On a finite vertex type with at least three vertices, a simple graph G with G.Adj s t admits an st-numbering if and only if G is 2-vertex-connected.