mkOfPoint

Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

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

← MathLib Explorer

English

From a single point p, form the 0-simplex (a single-point simplex).

Русский

Из точки p строится 0-элемент simplex.

LaTeX

$$$\\text{mkOfPoint } k p = \\text{Simplex } k P 0$$$

Lean4

/-- Construct a 0-simplex from a point. -/
def mkOfPoint (p : P) : Simplex k P 0 :=
  have : Subsingleton (Fin (1 + 0)) := by rw [add_zero]; infer_instance
  ⟨fun _ => p, affineIndependent_of_subsingleton k _⟩

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

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

Разделы

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

Аффилиация

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