mkFunctorRight — Mathlib

English

There is a canonical isomorphism between inclRight ⋙ mkFunctor F G α and G, given by identity.

Русский

Существует канонический изоморфизм между inclRight ⋙ mkFunctor F G α и G, заданный единичным изоморфизмом.

LaTeX

$$$ (\mathrm{inclRight} C D) \circ \mathrm{mkFunctor} F G α \cong G $$$

Lean4

/-- Precomposing `mkFunctor F G α` with the right inclusion gives back `G`. -/
@[simps!]
def mkFunctorRight : inclRight C D ⋙ mkFunctor F G α ≅ G :=
  Iso.refl _

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