isIso_counit_app_of_iso — Mathlib

English

If R is faithful and full, then h.unit.app Y is an isomorphism whenever there exists an iso Y ≅ R.obj X.

Русский

Если R верен и полный, то h.unit.app Y — изоморфизм при некотором изоморфизме Y ≅ R.obj X.

LaTeX

$$$\forall Y:\ C,\forall X:\ D,\ (Y \cong R.obj X) \Rightarrow IsIso(h.unit.app Y)$$$

Lean4

theorem isIso_counit_app_of_iso [L.Faithful] [L.Full] {X : D} {Y : C} (e : X ≅ L.obj Y) : IsIso (h.counit.app X) :=
  (isIso_counit_app_iff_mem_essImage h).mpr ⟨Y, ⟨e.symm⟩⟩

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