face — Mathlib

English

A face of a simplex is obtained by choosing a subset of its vertices.

Русский

Грань симплекса получается выбрав подмножество вершин.

LaTeX

$$$\\text{face } s\\ h \\, fs = \\text{Simplex } k P m$$$

Lean4

/-- A face of a simplex is a simplex with the given subset of
points. -/
def face {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) : Simplex k P m :=
  ⟨s.points ∘ fs.orderEmbOfFin h, s.independent.comp_embedding (fs.orderEmbOfFin h).toEmbedding⟩

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