mk_center

Mathlib.Geometry.Euclidean.Sphere.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.Sphere.mk_center

English

The center of a sphere is the first coordinate that defines it.

Русский

Центр сферы — это первый координат, который её задаёт.

LaTeX

$$$(\langle c, r\rangle : \text{Sphere}(P)).center = c$$$

Lean4

theorem mk_center (c : P) (r : ℝ) : (⟨c, r⟩ : Sphere P).center = c :=
  rfl

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

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

Разделы

Аффилиация

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