frontier_sphere — Mathlib

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]

Похожие утверждения