imageSubobjectIso — Mathlib

English

The underlying object of imageSubobject f is isomorphic to the chosen object image f.

Русский

Базовый объект imageSubobject f изоморфен выбранному объекту image f.

LaTeX

$$$(\mathrm{imageSubobject} f : C) \cong \mathrm{image} f$$$

Lean4

/-- The underlying object of `imageSubobject f` is (up to isomorphism!)
the same as the chosen object `image f`. -/
def imageSubobjectIso : (imageSubobject f : C) ≅ image f :=
  Subobject.underlyingIso (image.ι f)

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