isoOfEq — Mathlib

English

Equality of mk-factors yields an isomorphism between the corresponding subobject images.

Русский

Равенство mk-факторов порождает изоморфизм соответствующих образов подобъектов.

LaTeX

$$$\text{isoOfEqMk } \;X:\ Subobject B \to A : (X = mk f) \Rightarrow (X : C) \cong A$$$

Lean4

/-- An equality of subobjects gives an isomorphism of the corresponding objects.
(One could use `underlying.mapIso (eqToIso h))` here, but this is more readable.) -/
@[simps]
def isoOfEq {B : C} (X Y : Subobject B) (h : X = Y) : (X : C) ≅ (Y : C)
    where
  hom := ofLE _ _ h.le
  inv := ofLE _ _ h.ge

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