mk_radius

Mathlib.Geometry.Euclidean.Sphere.Basic

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

English

The radius of a sphere is the second coordinate that defines it.

Русский

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

LaTeX

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

Lean4

theorem mk_radius (c : P) (r : ℝ) : (⟨c, r⟩ : Sphere P).radius = r :=
  rfl

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

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

Разделы

Аффилиация

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