mk_center_radius

Mathlib.Geometry.Euclidean.Sphere.Basic

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

English

The sphere determined by a center and a radius equals the original sphere.

Русский

Сфера, заданная центром и радиусом, совпадает с исходной сферой.

LaTeX

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

Lean4

@[simp]
theorem mk_center_radius (s : Sphere P) : (⟨s.center, s.radius⟩ : Sphere P) = s := by ext <;> rfl

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

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

Разделы

Аффилиация

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