cospherical_singleton

Mathlib.Geometry.Euclidean.Sphere.Basic

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

English

A singleton set is cospherical.

Русский

Множество из одного элемента косферично.

LaTeX

$$$$ Cospherical(\{p\} : Set P). $$$$

Lean4

/-- A single point is cospherical. -/
theorem cospherical_singleton (p : P) : Cospherical ({ p } : Set P) :=
  by
  use p
  simp

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

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

Разделы

Аффилиация

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