face_points — Mathlib

English

The points of a face correspond to the original points via the order embedding.

Русский

Точки грани соответствуют исходным точкам через порядок вложения.

LaTeX

$$$(s.face h).points i = s.points (fs.orderEmbOfFin h i)$$$

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)
    (i : Fin (m + 1)) : (s.face h).points i = s.points (fs.orderEmbOfFin h i) :=
  rfl

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