face_eq_mkOfPoint — Mathlib

English

A face consisting of a single vertex of a simplex is exactly the 0-simplex at that vertex.

Русский

Грань, состоящая из одной вершины симплекса, является нулевой симплексной гранью в этой вершине.

LaTeX

$$$ (s.face(\\mathrm{Finset.card\\_singleton}(i))) = \\mathrm{mkOfPoint}\\,k\\,(s.points\\,i) $$$

Lean4

/-- A single-point face equals the 0-simplex constructed with
`mkOfPoint`. -/
@[simp]
theorem face_eq_mkOfPoint {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :
    s.face (Finset.card_singleton i) = mkOfPoint k (s.points i) :=
  by
  ext
  simp [Affine.Simplex.mkOfPoint_points, Affine.Simplex.face_points, Finset.orderEmbOfFin_singleton]

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