range_faceOpposite_points — Mathlib

English

The set of vertices of the opposite face to vertex i is the image of the complement of {i} under the original vertex map.

Русский

Множество вершин противоположной грани к вершине i есть образ комплемента {i} под отображением вершин исходного симплекса.

LaTeX

$$$\\mathrm{Set.range}((s.faceOpposite(i)).points) = s.points''\\,{i}^{c}$$$

Lean4

@[simp]
theorem range_faceOpposite_points {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :
    Set.range (s.faceOpposite i).points = s.points '' { i }ᶜ := by simp [faceOpposite]

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