faceOpposite_map — Mathlib

English

In a 1-simplex, the opposite-face point to 0 is the 1-point: the two endpoints correspond.

Русский

В 1-симплексe противоположная точка к 0-й вершине — это вторая вершина.

LaTeX

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

Lean4

@[simp]
theorem faceOpposite_map {n : ℕ} [NeZero n] (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective f)
    (i : Fin (n + 1)) : (s.map f hf).faceOpposite i = (s.faceOpposite i).map f hf :=
  rfl

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