ofSimplex_yonedaEquiv_δ — Mathlib

English

For i, the simplex δ[i] corresponds to the complement face δ i via Yoneda; Subcomplex.ofSimplex(yonedaEquiv(stdSimplex.δ i)) equals the complement face.

Русский

Для i симплекс δ[i] соответствует грани- complements через Yoneda; Subcomplex.ofSimplex(yonedaEquiv(stdSimplex.δ i)) = face.ᶜ(i).

LaTeX

$$Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.δ i)) = face.{u} { i }ᶜ$$

Lean4

theorem ofSimplex_yonedaEquiv_δ {n : ℕ} (i : Fin (n + 2)) :
    Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.δ i)) = face.{u} { i }ᶜ :=
  (face_eq_ofSimplex _ _ (Fin.succAboveOrderIso i)).symm

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