toSimplexCategory_obj_mk — Mathlib

English

For every n, the object map sends mk n to the same mk n, i.e., it preserves the mk-objects.

Русский

Для каждого n отображение объектов сохраняет mk n, то есть отображение объектов сохраняет структуры mk.

LaTeX

$$$\mathrm{toSimplexCategory.obj}(\mathrm{mk}(n)) = \mathrm{mk}(n)$$$

Lean4

@[simp]
theorem toSimplexCategory_obj_mk (n : ℕ) : toSimplexCategory.obj (mk n) = .mk n :=
  rfl

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