extendToSuccObjSuccIso — Mathlib

English

The map at le_succ is the composite of objIso, F.map, and objSuccIso.

Русский

Отображение на le_succ есть композиция из objIso, F.map и objSuccIso.

LaTeX

$$$\\text{extendToSuccMapLeSucc} : \\text{map} (Order.le_succ j) = (\\text{objIso}\\; j) \\circ F.map (homOfLE) \\circ (\\text{objSuccIso}\\; j)^{-1}$$$

Lean4

/-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`. -/
def extendToSuccObjSuccIso : (extendToSucc hj F τ).obj ⟨Order.succ j, by simp⟩ ≅ X :=
  extendToSucc.objSuccIso hj F X

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