toSimplexCategory_map_δ — Mathlib

English

The map of δ under the toSimplexCategory functor is preserved: toSimplexCategory.map(δ_i) = δ_i.

Русский

Образ δ через отображение functor toSimplexCategory сохраняется: toSimplexCategory.map(δ_i) = δ_i.

LaTeX

$$$\mathrm{toSimplexCategory.map}(\delta_i) = \mathrm{SimplexCategory}.\delta_i$$$

Lean4

@[simp]
theorem toSimplexCategory_map_δ {n : ℕ} (i : Fin (n + 2)) : toSimplexCategory.map (δ i) = SimplexCategory.δ i :=
  rfl

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