English
The interior of a nondegenerate closed ball of radius r is the standard open ball of the same radius.
Русский
interior(замкнутый шар) совпадает с открытым шаром того же радиуса при r ≠ 0.
LaTeX
$$$\\operatorname{interior}(\\overline{B}(x,r)) = B(x,r)\\quad\\text{for } r \\neq 0$$$
Lean4
theorem closure_ball (x : E) {r : ℝ} (hr : r ≠ 0) : closure (ball x r) = closedBall x r :=
by
refine Subset.antisymm closure_ball_subset_closedBall fun y hy => ?_
have : ContinuousWithinAt (fun c : ℝ => c • (y - x) + x) (Ico 0 1) 1 :=
((continuous_id.smul continuous_const).add continuous_const).continuousWithinAt
convert this.mem_closure _ _
· rw [one_smul, sub_add_cancel]
· simp [closure_Ico zero_ne_one, zero_le_one]
· rintro c ⟨hc0, hc1⟩
rw [mem_ball, dist_eq_norm, add_sub_cancel_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg hc0, mul_comm, ←
mul_one r]
rw [mem_closedBall, dist_eq_norm] at hy
replace hr : 0 < r := ((norm_nonneg _).trans hy).lt_of_ne hr.symm
apply mul_lt_mul' <;> assumption
