face_map — Mathlib

English

For a simplex, reversing index order yields the same correspondence between a vertex and its opposite-face vertex via the rev map.

Русский

У симплекса обратный порядок индексов сохраняет соответствие между вершиной и её противоположной вершине через операцию rev.

LaTeX

$$$(s.faceOpposite(i)).points(n) = s.points(i^{\\mathrm{rev}})$$$

Lean4

@[simp]
theorem face_map {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective f) {fs : Finset (Fin (n + 1))}
    {m : ℕ} (h : #fs = m + 1) : (s.map f hf).face h = (s.face h).map f hf :=
  rfl

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