mono

Mathlib.CategoryTheory.Subobject.MonoOver

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoOver.mono

English

If f: A ⟶ B in MonoOver X is an isomorphism, then its left component is an isomorphism.

Русский

Если стрелка в MonoOver X является изоморфизмом, то левая составляющая тоже изоморфизм.

LaTeX

$$If $f: A\to B$ in MonoOver X with IsIso f, then IsIso f.left.$$

Lean4

instance mono (f : MonoOver X) : Mono f.arrow :=
  f.property

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru