English
If a closed set s is contained in a ball centered at x with radius r, there exists r' < r such that s is contained in the ball of radius r' around x.
Русский
Если замкнутая множество s содержится в шаре с центром x и радиусом r, существует r' < r такой что s содержится в шаре радиуса r'.
LaTeX
$$$\exists r' < r, s \subseteq B(x,r')$$$
Lean4
/-- If a ball in a proper space includes a closed set `s`, then there exists a ball with the same
center and a strictly smaller radius that includes `s`. -/
theorem exists_lt_subset_ball (hs : IsClosed s) (h : s ⊆ ball x r) : ∃ r' < r, s ⊆ ball x r' :=
by
rcases le_or_gt r 0 with hr | hr
· rw [ball_eq_empty.2 hr, subset_empty_iff] at h
subst s
exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩
· exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩
