frontier_closedBall — Mathlib

English

Let E be a real normed space and x ∈ E. If r ≠ 0, then the boundary of the closed ball of radius r around x is the sphere of radius r around x.

Русский

Пусть E — нормированное пространство над ℝ и X ∈ E. Если r ≠ 0, то граница замкнутого шара радиуса r с центром в x совпадает с шаром радиуса r с центром в x.

LaTeX

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

Lean4

theorem frontier_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) : frontier (closedBall x r) = sphere x r := by
  rw [frontier, closure_closedBall, interior_closedBall x hr, closedBall_diff_ball]

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