mem_essImage_of_unit_isIso — Mathlib

English

If there exists an iso X ≅ L.obj Y, then h.counit.app X is an isomorphism.

Русский

Если существует изоморфизм X ≅ L.obj Y, то h.counit.app X — изоморфизм.

LaTeX

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

Lean4

/-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`. -/
theorem mem_essImage_of_unit_isIso (A : C) [IsIso (h.unit.app A)] : R.essImage A :=
  ⟨L.obj A, ⟨(asIso (h.unit.app A)).symm⟩⟩

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