English
If y lies inside the ball centered at x with radius ε, then there exists a radius ε' > 0 such that the ball centered at y with radius ε' is contained in the ball centered at x with radius ε.
Русский
Если y лежит внутри шара с центром x и радиусом ε, то существует ε' > 0 такое, что шар вокруг y радиуса ε' содержится в шаре вокруг x радиуса ε.
LaTeX
$$$y \\in \\mathrm{ball}(x,\\varepsilon) \\Rightarrow \\exists \\varepsilon' > 0, \\ \\mathrm{ball}(y,\\varepsilon') \\subseteq \\mathrm{ball}(x,\\varepsilon)$$$
Lean4
theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε :=
by
have : 0 < ε - edist y x := by simpa using h
refine ⟨ε - edist y x, this, ball_subset ?_ (ne_top_of_lt h)⟩
exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le
