πObj_ιIteration_app_right — Mathlib

English

The projection πObj composed with the right component of ιIteration app equals the iteration object’s hom; i.e., πObj ∘ ((ιIteration).app f).right = ((iteration).obj (Arrow.mk f)).hom.

Русский

Составление πObj с правой частью приложения ιIteration равно гомоморфизму объекта итерации: πObj ∘ ((ιIteration).app f).right = ((iteration).obj (Arrow.mk f)).hom.

LaTeX

$$$\\pi_{\\mathrm{Obj}} \\circ ((\\iotaIteration I κ).app f).{\\mathrm{right}} = ((\\mathrm{iteration}(I,\\kappa)).{\\mathrm{obj}}(\\mathrm{Arrow.mk} f)).{\\mathrm{hom}}$$$

Lean4

@[reassoc (attr := simp)]
theorem πObj_ιIteration_app_right :
    πObj I κ f ≫ ((ιIteration I κ).app f).right = ((iteration I κ).obj (Arrow.mk f)).hom := by simp [πObj]

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