subset

Mathlib.Geometry.Euclidean.Sphere.Basic

URI: https://scilib.ai/kg/mathlib#EuclideanGeometry.Concyclic.subset

← MathLib Explorer

English

The set of points on a sphere is cospherical.

Русский

Множество точек на сфере косферично.

LaTeX

$$$$ \text{Cospherical}((\text{Sphere } P) : Set P). $$$$

Lean4

/-- A subset of a concyclic set is concyclic. -/
theorem subset {ps₁ ps₂ : Set P} (hs : ps₁ ⊆ ps₂) (h : Concyclic ps₂) : Concyclic ps₁ :=
  ⟨h.1.subset hs, h.2.subset hs⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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