instNonemptySphere

Mathlib.Geometry.Euclidean.Sphere.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.instNonemptySphere

English

In any nonempty metric space P, the sphere with center any point and radius 0 is a nonempty set.

Русский

В любой непустой метрическом пространстве есть сфера с произвольным центром и радиусом 0.

LaTeX

$$$\exists s:\, \text{Sphere}(P)$$$

Lean4

instance [Nonempty P] : Nonempty (Sphere P) :=
  ⟨⟨Classical.arbitrary P, 0⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru