instMembershipSphere

Mathlib.Geometry.Euclidean.Sphere.Basic

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

English

Membership in a sphere is determined by the usual distance condition to its center.

Русский

Принадлежность точке сфере определяется обычным условием расстояния до центра сферы.

LaTeX

$$$p \in (\text{Sphere}(P)) \iff \operatorname{dist}(p, \text{center}) = \text{radius}$$$

Lean4

instance : Membership P (Sphere P) :=
  ⟨fun s p => p ∈ (s : Set P)⟩

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

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

Разделы

Аффилиация

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