instFintypePointsWithCircumcenterIndex

Mathlib.Geometry.Euclidean.Circumcenter

URI: https://scilib.ai/kg/mathlib#Affine.Simplex.instFintypePointsWithCircumcenterIndex

English

There exists a finite type indexing the circumcenter points of a simplex.

Русский

Существует конечный тип, индексирующий точки circumcenter для простого многогранника.

LaTeX

$$$\text{The set }(\mathrm{PointsWithCircumcenterIndex}\,n)\text{ is finite}$$$

Lean4

instance {n✝} : Fintype✝ (@Affine.Simplex.PointsWithCircumcenterIndex✝ n✝) :=
  derive_fintype% _

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

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

Разделы

Аффилиация

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