extendToSuccObjIso — Mathlib

English

Canonical iso between extendToSucc.obj and F.obj on eligible indices.

Русский

Канонический изоморфизм между extendToSucc.obj и F.obj на допустимых индексах.

LaTeX

$$$\\text{extendToSuccObjIso} \\; hj\\; F\\; X\\; ⟨i, hi⟩ : \\text{obj} \\; F \\; X \\; ⟨i, hi⟩ \\cong F.obj ⟨i, hi⟩$$$

Lean4

/-- The isomorphism `(extendToSucc hj F τ).obj ⟨i, _⟩ ≅ F.obj i` when `i ≤ j` -/
def extendToSuccObjIso (i : J) (hi : i ≤ j) :
    (extendToSucc hj F τ).obj ⟨i, hi.trans (Order.le_succ j)⟩ ≅ F.obj ⟨i, hi⟩ :=
  extendToSucc.objIso F X ⟨i, hi⟩

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