faceOpposite_point_eq_point_one — Mathlib

English

In a 1-simplex, the opposite vertex to the 0-th vertex has its single point equal to the 1-st vertex.

Русский

У 1-симплекса противоположная вершина нулевой вершине имеет единственную точку равную второй вершине.

LaTeX

$$$ (s.faceOpposite 0).points(\\,\\text{Fin 1}) = s.points(1) $$$

Lean4

@[simp]
theorem faceOpposite_point_eq_point_one (s : Simplex k P 1) (n : Fin 1) : (s.faceOpposite 0).points n = s.points 1 :=
  s.faceOpposite_point_eq_point_rev _ _

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