instIsIsoLeftDiscretePUnit — Mathlib

English

For A, B in MonoOver X, an arrow f: A ⟶ B is an isomorphism iff its left component is an isomorphism.

Русский

Для $A,B$ в MonoOver X стрелка $f$ изоморфизм тогда и только тогда, когда левая часть $f.left$ исоморфизм.

LaTeX

$$IsIso f ↔ IsIso f.left$$

Lean4

instance {A B : MonoOver X} (f : A ⟶ B) [IsIso f] : IsIso f.left :=
  inferInstanceAs (IsIso ((MonoOver.forget _ ⋙ Over.forget _).map f))

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