frontier_sphere' — Mathlib

English

For all x ∈ E and r ∈ ℝ, the frontier of the closed ball equals the sphere with the same center and radius.

Русский

Для всех x ∈ E и r ∈ ℝ граница замкнутого шара совпадает со сферой с тем же центром и радиусом.

LaTeX

$$$$ \forall x \in E, \forall r \in \mathbb{R}, \partial \overline{B}(x,r) = S(x,r). $$$$

Lean4

@[simp]
theorem frontier_sphere' (x : E) (r : ℝ) : frontier (sphere x r) = sphere x r := by
  rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]

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