nonempty_iff — Mathlib

English

In a nontrivial normed space, the sphere is nonempty iff its radius is nonnegative.

Русский

В невырожденном нормированном пространстве сфера непустая тогда и только тогда, когда её радиус неотрицателен.

LaTeX

$$$$ (\text{Nonempty } V) \Rightarrow (s : Sphere P).Nonempty \iff 0 \le s.radius. $$$$

Lean4

theorem nonempty_iff [Nontrivial V] {s : Sphere P} : (s : Set P).Nonempty ↔ 0 ≤ s.radius :=
  by
  refine ⟨fun ⟨p, hp⟩ ↦ radius_nonneg_of_mem hp, fun h ↦ ?_⟩
  obtain ⟨v, hv⟩ := (NormedSpace.sphere_nonempty (x := (0 : V)) (r := s.radius)).2 h
  refine ⟨v +ᵥ s.center, ?_⟩
  simpa [mem_sphere] using hv

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