nonempty

Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

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

English

There exists a nonempty 0-simplex in the affine setting.

Русский

Существует непустой 0-мерный простой многогранник.

LaTeX

$$$\\text{Nonempty }(\\text{Simplex } k P 0)$$$

Lean4

instance nonempty : Nonempty (Simplex k P 0) :=
  ⟨mkOfPoint k <| AddTorsor.nonempty.some⟩

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

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

Разделы

Аффилиация

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