ofCoconeObjIso — Mathlib

English

There is an isomorphism between the top extended object (at j) and the cocone’s vertex point c.pt.

Русский

Существует изоморфизм между верхним расширенным объектом (при j) и вершиной кокона c.pt.

LaTeX

$$$(\\mathrm{ofCocone} \\ c).\\mathrm{obj} \\langle j, -\\rangle \\cong c.\\mathrmpt$$$

Lean4

/-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`. -/
def ofCoconeObjIso (i : J) (hi : i < j) : (ofCocone c).obj ⟨i, hi.le⟩ ≅ F.obj ⟨i, hi⟩ :=
  ofCocone.objIso c _ _

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