faceOpposite_point_eq_point_succAbove

English

There is a precise index relation between the j-th vertex of the opposite face and the corresponding vertex of s obtained via the successor-above indexing.

Русский

Существует точное соответствие индексов между j-й вершиной противоположной грани и соответствующей вершиной s через операцию successor-above.

LaTeX

$$$ (s.faceOpposite(i)).points(j) = s.points\\bigl(\\mathrm{succAbove}(i,\\mathrm{cast}(\\mathrm{Nat}.sub\\_one\\_add\_one(\\mathrm{NeZero}.ne\\_\\_)))\\;j\\bigr) $$$

Lean4

theorem faceOpposite_point_eq_point_succAbove {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1))
    (j : Fin (n - 1 + 1)) :
    (s.faceOpposite i).points j = s.points (Fin.succAbove i (Fin.cast (Nat.sub_one_add_one (NeZero.ne _)) j)) := by
  simp_rw [faceOpposite, face, comp_apply, Finset.orderEmbOfFin_compl_singleton_apply]

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