frontier_closedBall' — Mathlib

English

For every x ∈ E and r ∈ ℝ, the frontier of the closed ball equals the sphere of radius r around x.

Русский

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

LaTeX

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

Lean4

theorem frontier_closedBall' (x : E) (r : ℝ) : frontier (closedBall x r) = sphere x r := by
  rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]

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