mono_of_mono

Mathlib.CategoryTheory.Category.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.mono_of_mono

← MathLib Explorer

English

If the composite f ≫ g is mono, then f is mono.

Русский

Если композиция f ≫ g является моно, то f — моно.

LaTeX

$$$ \\text{Mono}(f) \\quad\\text{provided } \\text{Mono}(f\\circ g)$$$

Lean4

theorem mono_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono (f ≫ g)] : Mono f :=
  ⟨fun _ _ w => (cancel_mono (f ≫ g)).1 <| by simp only [← Category.assoc, w]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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