mkOfObjOfMapSucc_obj — Mathlib

English

The underlying object function of the constructed ComposableArrows equals the given obj on every index.

Русский

Функция объектов для сконструированного ComposableArrows совпадает с заданной obj на каждом индексе.

LaTeX

$$$\forall i, (mkOfObjOfMapSucc obj mapSucc).obj i = obj i$$$

Lean4

@[simp]
theorem mkOfObjOfMapSucc_obj (i : Fin (n + 1)) : (mkOfObjOfMapSucc obj mapSucc).obj i = obj i :=
  rfl

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