English
In a proper space, for any center x and radius r > 0, any closed set s contained in the closed ball around x of radius r is contained in a smaller ball with some radius r' in (0,r).
Русский
В допустимом пространстве для любого центра x и радиуса r>0 любая замкнутая множество s, содержащаяся в замкнутом шаре с центром x радиуса r, содержится внутри меньшего шара радиуса r'∈(0,r).
LaTeX
$$$\forall x\in α, \forall r>0, \forall s\subseteq \overline{B}(x,r)\text{ IsClosed}(s) \Rightarrow \exists r'\in (0,r), s\subseteq B(x,r')$$$
Lean4
/-- If a nonempty ball in a proper space includes a closed set `s`, then there exists a nonempty
ball with the same center and a strictly smaller radius that includes `s`. -/
theorem exists_pos_lt_subset_ball (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ ball x r) : ∃ r' ∈ Ioo 0 r, s ⊆ ball x r' :=
by
rcases eq_empty_or_nonempty s with (rfl | hne)
· exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩
have : IsCompact s := (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall)
obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
this.exists_isMaxOn (β := α) (α := ℝ) hne (continuous_id.dist continuous_const).continuousOn
have hyr : dist y x < r := h hys
rcases exists_between hyr with ⟨r', hyr', hrr'⟩
exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩
