English
Let E be a real normed space and r ≠ 0. The boundary of the sphere of radius r around x is the sphere itself.
Русский
Пусть E — нормированное пространство над ℝ и r ≠ 0. Граница сферы радиуса r вокруг x совпадает с самой сферой.
LaTeX
$$$$ \forall x \in E, \forall r \in \mathbb{R}, r \neq 0 \Rightarrow \partial S(x,r) = S(x,r). $$$$
Lean4
theorem frontier_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (sphere x r) = sphere x r := by
rw [isClosed_sphere.frontier_eq, interior_sphere x hr, diff_empty]