Erdős Problem 599

References:

• erdosproblems.com/599
• [AhBe09] Aharoni, Ron and Berger, Eli, Menger's theorem for infinite graphs, Invent. Math. 176 (2009), 1--62.

theorem Erdos599.erdos_599 : True ↔ ∀ (V : Type) (G : SimpleGraph V) (A B : Set V), Disjoint A B → G.IsIndepSet A → G.IsIndepSet B → ∃ (ι : Type) (a : ι → V) (b : ι → V) (p : (i : ι) → G.Walk (a i) (b i)) (S : Set V), (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun (i j : ι) => Disjoint {v : V | v ∈ (p i).support} {v : V | v ∈ (p j).support}) ∧ S ⊆ {v : V | ∃ (i : ι), v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v : V, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

Erdős Problem 599 (the Erdős–Menger conjecture).

Let $G$ be a (possibly infinite) graph and let $A, B$ be disjoint independent sets of vertices. Must there exist a family $P$ of pairwise vertex-disjoint paths from $A$ to $B$, and a set $S$ of vertices containing exactly one vertex from each path in $P$, such that every path from $A$ to $B$ contains at least one vertex of $S$?

For finite $G$ this is equivalent to Menger's theorem. The answer is yes, proved by Aharoni and Berger [AhBe09].

theorem Erdos599.erdos_599.variants.aharoni_berger (V : Type) (G : SimpleGraph V) (A B : Set V) : ∃ (ι : Type) (a : ι → V) (b : ι → V) (p : (i : ι) → G.Walk (a i) (b i)) (S : Set V), (∀ (i : ι), a i ∈ A) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun (i j : ι) => Disjoint {v : V | v ∈ (p i).support} {v : V | v ∈ (p j).support}) ∧ S ⊆ {v : V | ∃ (i : ι), v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v : V, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

Menger's theorem for infinite graphs (Aharoni–Berger [AhBe09]).

The theorem actually proved by Aharoni and Berger holds for arbitrary vertex sets $A$ and $B$: in any (possibly infinite) graph $G$ there is a family $P$ of pairwise vertex-disjoint $A$--$B$ paths together with an $A$--$B$ separator $S$ consisting of the choice of exactly one vertex from each path in $P$. The disjointness and independence hypotheses of erdos_599 are not needed.

theorem Erdos599.erdos_599.test.empty_A (V : Type) (G : SimpleGraph V) (B : Set V) : ∃ (ι : Type) (a : ι → V) (b : ι → V) (p : (i : ι) → G.Walk (a i) (b i)) (S : Set V), (∀ (i : ι), a i ∈ ∅) ∧ (∀ (i : ι), b i ∈ B) ∧ (∀ (i : ι), (p i).IsPath) ∧ (Pairwise fun (i j : ι) => Disjoint {v : V | v ∈ (p i).support} {v : V | v ∈ (p j).support}) ∧ S ⊆ {v : V | ∃ (i : ι), v ∈ (p i).support} ∧ (∀ (i : ι), ∃! v : V, v ∈ S ∧ v ∈ (p i).support) ∧ ∀ a' ∈ ∅, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

Sanity check: when $A = \varnothing$ the conclusion of erdos_599 holds trivially, with the empty family of paths and $S = \varnothing$ (the covering condition is vacuous since there is no path starting in $\varnothing$).