The fan lemma

Let G be a simple graph, x a vertex and U a finite set of vertices not containing x. A fan from x to U is a family of paths, the i-th from x to a vertex u i ∈ U, whose other vertices lie outside U, and any two of which share only the vertex x; in particular their ends u i are distinct. This file proves the fan form of Menger's theorem on a finite vertex type: the largest fan from x to U has as many paths as the least number of vertices other than x that meet every walk from x to a vertex of U.

The fan lemma follows: in a k-vertex-connected graph on a finite vertex type, a vertex x outside a set U of at least k vertices is joined to U by a fan of k paths. More generally, it suffices that x be k-vertex-reachable from every vertex of U. Fans are the tool by which cycles through prescribed vertices and open ears are built in highly connected graphs.

Main results

• SimpleGraph.card_le_card_of_fan: weak duality: a fan from x to U has at most as many paths as any set of vertices other than x meeting every walk from x to U. No finiteness is needed.
• SimpleGraph.exists_fan_separator_card_eq: the fan form of Menger's theorem, in witness form: some fan and some such separator have the same size.
• SimpleGraph.forall_exists_walk_iff_exists_fan: its predicate form: deleting fewer than k vertices other than x always leaves a walk from x to U exactly when there is a fan of k paths from x to U.
• SimpleGraph.exists_fan_of_forall_isVertexReachable and SimpleGraph.IsVertexConnected.exists_fan: the fan lemma.
• SimpleGraph.IsVertexConnected.exists_open_ear_of_sup_edge and SimpleGraph.IsVertexConnected.exists_open_ear_through: existence of an open ear in G through x ∉ U between two distinct vertices of U when G ⊔ SimpleGraph.edge s t (for distinct s, t ∈ U) or G itself is 2-vertex-connected.

Implementation notes

The witness form is derived from the vertex-capacitated set-to-set form of Menger's theorem, SimpleGraph.exists_paths_setSeparator_sum_eq, between the neighbours of x and U, with capacity 0 at x and 1 at every other vertex. The capacities make the paths pairwise vertex-disjoint and keep them away from x, so prefixing each with its first edge from x gives a fan; a path that already starts in U is replaced by that single edge. A separator of this capacitated problem, with x removed, meets every walk from x to U: such a walk contains a path from x to U, whose part after its first edge is a walk from a neighbour of x to U avoiding x.

References

• R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Corollary 3.3.4.

theorem SimpleGraph.card_le_card_of_fan {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} {ι : Type u_1} [Fintype ι] {u : ι → V} {P : (i : ι) → G.Walk x (u i)} (hu : ∀ (i : ι), u i ∈ U) (hP : Pairwise fun (i j : ι) => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x) {X : Finset V} (hxX : x ∉ X) (hX : ∀ y ∈ U, ∀ (p : G.Walk x y), ∃ v ∈ p.support, v ∈ X) : Fintype.card ι ≤ X.card

Weak duality for fans. A family of walks, the i-th from x to u i ∈ U, any two of which share only the vertex x, has at most #X members, for every set X of vertices not containing x that meets every walk from x to a vertex of U. No finiteness assumption on V is needed.

theorem SimpleGraph.exists_fan_separator_card_eq {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] (hx : x ∉ U) : ∃ (k : ℕ) (u : Fin k → V) (P : (i : Fin k) → G.Walk x (u i)) (X : Finset V), Function.Injective u ∧ (∀ (i : Fin k), u i ∈ U) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧ (Pairwise fun (i j : Fin k) => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x) ∧ x ∉ X ∧ (∀ y ∈ U, ∀ (p : G.Walk x y), ∃ v ∈ p.support, v ∈ X) ∧ X.card = k

Menger's theorem for fans. Let x be a vertex outside a set U of vertices of a simple graph on a finite vertex type. Some family of k paths, the i-th from x to u i ∈ U with its other vertices outside U, any two of which share only the vertex x, and some set of k vertices other than x meeting every walk from x to a vertex of U exist. By SimpleGraph.card_le_card_of_fan, the fan is then largest and the separator smallest.

theorem SimpleGraph.forall_exists_walk_iff_exists_fan {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] (hx : x ∉ U) (k : ℕ) : (∀ (X : Finset V), X.card < k → x ∉ X → ∃ y ∈ U, ∃ (p : G.Walk x y), ∀ v ∈ p.support, v ∉ X) ↔ ∃ (u : Fin k → V) (P : (i : Fin k) → G.Walk x (u i)), Function.Injective u ∧ (∀ (i : Fin k), u i ∈ U) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧ Pairwise fun (i j : Fin k) => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x

Menger's theorem for fans, predicate form. Let x be a vertex outside a set U of vertices of a simple graph on a finite vertex type. For every set X of fewer than k vertices other than x, some walk from x to a vertex of U avoids X, exactly when there are k paths, the i-th from x to u i ∈ U with its other vertices outside U, any two of which share only the vertex x.

theorem SimpleGraph.exists_fan_of_forall_isVertexReachable {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] {k : ℕ} (hx : x ∉ U) (hU : k ≤ U.card) (h : ∀ y ∈ U, G.IsVertexReachable (↑k) x y) : ∃ (u : Fin k → V) (P : (i : Fin k) → G.Walk x (u i)), Function.Injective u ∧ (∀ (i : Fin k), u i ∈ U) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧ Pairwise fun (i j : Fin k) => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x

The fan lemma. Let x be a vertex outside a set U of at least k vertices of a simple graph on a finite vertex type, and suppose that x is k-vertex-reachable from every vertex of U. Then there are k paths, the i-th from x to u i ∈ U with its other vertices outside U, any two of which share only the vertex x.

theorem SimpleGraph.IsVertexConnected.exists_fan {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] {k : ℕ} (h : G.IsVertexConnected ↑k) (hx : x ∉ U) (hU : k ≤ U.card) : ∃ (u : Fin k → V) (P : (i : Fin k) → G.Walk x (u i)), Function.Injective u ∧ (∀ (i : Fin k), u i ∈ U) ∧ (∀ (i : Fin k), (P i).IsPath) ∧ (∀ (i : Fin k), ∀ v ∈ (P i).support, v ≠ u i → v ∉ U) ∧ Pairwise fun (i j : Fin k) => ∀ v ∈ (P i).support, v ∈ (P j).support → v = x

The fan lemma. In a k-vertex-connected simple graph on a finite vertex type, a vertex x outside a set U of at least k vertices is joined to U by k paths, the i-th from x to u i ∈ U with its other vertices outside U, any two of which share only the vertex x.

theorem SimpleGraph.IsVertexConnected.exists_open_ear_of_sup_edge {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] {s t : V} (h : (G ⊔ edge s t).IsVertexConnected 2) (hst : s ≠ t) (hsU : s ∈ U) (htU : t ∈ U) (hx : x ∉ U) : ∃ (u₀ : V) (u₁ : V) (R : G.Walk u₀ u₁), u₀ ∈ U ∧ u₁ ∈ U ∧ u₀ ≠ u₁ ∧ R.IsPath ∧ x ∈ R.support ∧ ∀ v ∈ R.support, v ≠ u₀ → v ≠ u₁ → v ∉ U

Given distinct vertices s ≠ t in U and a vertex x ∉ U on a finite vertex type, 2-vertex-connectivity of G ⊔ SimpleGraph.edge s t produces an open ear in G itself passing through x between two distinct endpoints in U, with all internal vertices outside U.

theorem SimpleGraph.IsVertexConnected.exists_open_ear_through {V : Type u} {G : SimpleGraph V} {x : V} {U : Finset V} [Finite V] (h : G.IsVertexConnected 2) (hx : x ∉ U) (hU : 2 ≤ U.card) : ∃ (u₀ : V) (u₁ : V) (R : G.Walk u₀ u₁), u₀ ∈ U ∧ u₁ ∈ U ∧ u₀ ≠ u₁ ∧ R.IsPath ∧ x ∈ R.support ∧ ∀ v ∈ R.support, v ≠ u₀ → v ≠ u₁ → v ∉ U

In a 2-vertex-connected simple graph on a finite vertex type, any vertex x outside a set U of at least two vertices lies on an open ear in G between two distinct endpoints in U, with all internal vertices outside U.