Erdős problem 599 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

599.lean

Retained formal statement2 of 3

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$ ).

FormalConjectures/ErdosProblems/599.leanErdos599.erdos_599.test.empty_A9 linesExact file

1∀ (V : Type) (G : SimpleGraph V) (B : Set V),2  ∃ ι a b p S,3    (∀ (i : ι), a i ∈ ∅) ∧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' ∈ ∅, ∀ b' ∈ B, ∀ (q : G.Walk a' b'), q.IsPath → ∃ v ∈ q.support, v ∈ S

TestStatement only, no proof

Sources

Search problems.science