English
Let s be an n-simplex in an affine space, and let fs be a Finset of the index set {0,…,n} with |fs| = m+1. Then the list of vertices of the face corresponding to fs is obtained by taking those vertices of s in the order prescribed by the inclusion fs → {0,…,n}. In particular, (s.face h).points = s.points ∘ (fs.orderEmbOfFin h).
Русский
Пусть s — n-симплекс в аффинном пространстве, пусть fs ⊆ {0,…,n} и |fs| = m+1. Тогда вершины грани, соответствующей fs, получаются из вершин s по включению fs → {0,…,n} в том же порядке: (s.face h).points = s.points ∘ fs.orderEmbOfFin h.
LaTeX
$$$ (s.face(h)).points = s.points \\circ \\mathrm{orderEmbOfFin}(h) $$$
Lean4
/-- The points of a face of a simplex are given by `mono_of_fin`. -/
theorem face_points' {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) :
(s.face h).points = s.points ∘ fs.orderEmbOfFin h :=
rfl
