Erdős problem 599

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

599.lean

Retained formal statement3 of 3

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.

FormalConjectures/ErdosProblems/599.leanErdos599.erdos_599.variants.aharoni_berger9 linesExact file

1∀ (V : Type) (G : SimpleGraph V) (A B : Set V),2  ∃ ι a b p S,3    (∀ (i : ι), a i ∈ A) ∧4      (∀ (i : ι), b i ∈ B) ∧5        (∀ (i : ι), (p i).IsPath) ∧6          (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧7            S ⊆ {v | ∃ i, v ∈ (p i).support} ∧8              (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧9                ∀ a' ∈ A, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

SolvedStatement only, no proof