Skip to content

Erdős problem 599

Start work

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 statement2 of 3

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

FormalConjectures/ErdosProblems/599.leanErdos599.erdos_599.test.empty_A9 linesExact file
∀ (V : Type) (G : SimpleGraph V) (B : Set V),  ∃ ι a b p S,    (∀ (i : ι), a i ∈ ∅) ∧      (∀ (i : ι), b i ∈ B) ∧        (∀ (i : ι), (p i).IsPath) ∧          (Pairwise fun i j => Disjoint {v | v ∈ (p i).support} {v | v ∈ (p j).support}) ∧            S ⊆ {v | ∃ i, v ∈ (p i).support} ∧              (∀ (i : ι), ∃! v, v ∈ S ∧ v ∈ (p i).support) ∧                ∀ a' ∈ ∅, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S
TestStatement only, no proof