English
Let x be an element of a normed space F and s ⊆ F. Then the closed ball with center x and radius equal to the distance from x to the complement of s is contained in the closure of s; i.e., closedBall(x, infDist(x, s^c)) ⊆ closure(s).
Русский
Пусть x — элемент нормированного пространства, a s ⊆ F. Тогда замкнутый шар с центром в x и радиусом, равным расстоянию от x до множества дополнения s, содержится в замыкании s: closedBall(x, infDist(x, s^c)) ⊆ closure(s).
LaTeX
$$$\text{Let } x \in F \text{ and } s\subset F.\; \text{Then } \overline{\mathbb B}(x,\,\infDist(x, s^{c})) \subseteq \overline{s}.$$$
Lean4
theorem closedBall_infDist_compl_subset_closure {x : F} {s : Set F} (hx : x ∈ s) :
closedBall x (infDist x sᶜ) ⊆ closure s :=
by
rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀
· rw [h₀, closedBall_zero']
exact closure_mono (singleton_subset_iff.2 hx)
· rw [← closure_ball x h₀]
exact closure_mono ball_infDist_compl_subset
