touchpoint_eq_point_rev — Mathlib

English

In the one-dimensional case, the touchpoint equals the corresponding vertex in reversed order.

Русский

В одномерном случае touchpoint равен вершине с обращённой нумерацией.

LaTeX

$$s.touchpoint(signs,i) = s.points i.rev$$

Lean4

theorem touchpoint_eq_point_rev (s : Simplex ℝ P 1) (signs : Finset (Fin 2)) (i : Fin 2) :
    s.touchpoint signs i = s.points i.rev :=
  s.orthogonalProjectionSpan_faceOpposite_eq_point_rev _ _

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