sphere_nonempty — Mathlib

English

In a nontrivial real normed space, the sphere S(x,r) is nonempty if and only if r ≥ 0.

Русский

В ненулевом вещественном нормированном пространстве сфера S(x,r) непустая тогда и только тогда, когда r неотрицательно.

LaTeX

$$$$ (S(x,r)).\text{Nonempty} \iff 0 \le r. $$$$

Lean4

/-- In a nontrivial real normed space, a sphere is nonempty if and only if its radius is
nonnegative. -/
@[simp]
theorem sphere_nonempty {x : E} {r : ℝ} : (sphere x r).Nonempty ↔ 0 ≤ r :=
  by
  refine ⟨fun h => nonempty_closedBall.1 (h.mono sphere_subset_closedBall), fun hr => ?_⟩
  obtain ⟨y, hy⟩ := exists_norm_eq E hr
  exact ⟨x + y, by simpa using hy⟩

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