range_face_points — Mathlib

English

The set of vertices of a face is precisely the image of the index set fs under the vertex map of the simplex.

Русский

Множество вершин грани ровно есть образ множества индексов fs под отображением вершин симплекса.

LaTeX

$$$\\mathrm{Set.range}((s.face(h)).points) = s.points''\\;\\uparrow fs$$$

Lean4

/-- The set of points of a face. -/
@[simp]
theorem range_face_points {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : #fs = m + 1) :
    Set.range (s.face h).points = s.points '' ↑fs := by rw [face_points', Set.range_comp, Finset.range_orderEmbOfFin]

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