Erdős problem 1121

If $C_1,\ldots,C_n$ are circles in $\mathbb{R}^2$ with radii $r_1,\ldots,r_n$ such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius $r=\sum r_i$ .

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1121.lean

Retained formal statement1 of 2

If $C_1,\ldots,C_n$ are circles in $\mathbb{R}^2$ with radii $r_1,\ldots,r_n$ such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius $r=\sum r_i$ .

This is true, and was proved by Goodman and Goodman [GoGo45] (whose proof also generalises to higher dimensions). A generalisation to convex bodies was proved by Hadwiger [Ha47].

An alternative proof is given by Bezdek and Litvak [BeLi16].

FormalConjectures/ErdosProblems/1121.leanErdos1121.erdos_11217 linesExact file

1∀ {n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin 2)) (r : Fin n → ℝ),2  (∀ (i : Fin n), 0 < r i) →3    (∀ (v : EuclideanSpace ℝ (Fin 2)) (t : ℝ),4        v ≠ 0 →5          (∀ (i : Fin n), ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) →6            (∀ (i : Fin n), inner ℝ v (c i) < t) ∨ ∀ (i : Fin n), t < inner ℝ v (c i)) →7      ∃ z, ⋃ i, Metric.closedBall (c i) (r i) ⊆ Metric.closedBall z (∑ i, r i)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.