concyclic_empty

Mathlib.Geometry.Euclidean.Sphere.Basic

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

English

In any Euclidean setting, the empty set of points is concyclic.

Русский

В любой евклидовой геометрии пустое множество точек конциклично.

LaTeX

$$$\\Concyclic(\\emptyset)$$$

Lean4

/-- The empty set is concyclic. -/
theorem concyclic_empty : Concyclic (∅ : Set P) :=
  ⟨cospherical_empty, coplanar_empty ℝ P⟩

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

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

Разделы

Аффилиация

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