faceOpposite — Mathlib

English

For a simplex s of dimension n and a vertex index i, the faceOpposite i is the face of s obtained by removing the i-th vertex.

Русский

Для симплекса s размерности n грань opposite i — грань, полученная из s удалением i-й вершины.

LaTeX

$$$\\mathrm{faceOpposite}(s,i) = s.face(\\text{fs} := {i}^{c})$$$

Lean4

/-- The face of a simplex with all but one point. -/
def faceOpposite {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) : Simplex k P (n - 1) :=
  s.face (fs := { i }ᶜ) (by simp [card_compl, NeZero.one_le])

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