interior_sphere — Mathlib

English

Let E be a real normed space. For every x ∈ E and r ≠ 0, the interior of the sphere of radius r around x is empty.

Русский

Пусть E — нормированное пространство над ℝ. Для любых x ∈ E и r ≠ 0 interior сферы радиуса r вокруг x пуст.

LaTeX

$$$$ \forall x \in E, \forall r \in \mathbb{R}, r \neq 0 \Rightarrow \operatorname{int}(S(x,r)) = \emptyset. $$$$

Lean4

theorem interior_sphere (x : E) {r : ℝ} (hr : r ≠ 0) : interior (sphere x r) = ∅ := by
  rw [← frontier_closedBall x hr, interior_frontier isClosed_closedBall]

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