Erdős problem 1121 · problems.science

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

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1121.lean

Retained formal statement2 of 2

The proof of Goodman and Goodman [GoGo45] also generalises to higher dimensions: if $B_1,\ldots,B_n$ are balls in $\mathbb{R}^d$ with radii $r_1,\ldots,r_n$ such that no hyperplane disjoint from all the balls divides them into two non-empty sets then the balls can be covered by a ball of radius $r=\sum r_i$ .

FormalConjectures/ErdosProblems/1121.leanErdos1121.erdos_1121.variants.higher_dimension7 linesExact file

1∀ {d n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin d)) (r : Fin n → ℝ),2  (∀ (i : Fin n), 0 < r i) →3    (∀ (v : EuclideanSpace ℝ (Fin d)) (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)

SolvedStatement only, no proof

Sources

Search problems.science