mono_of_iso

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.mono_of_iso

← MathLib Explorer

English

If f is an isomorphism, then f is a monomorphism.

Русский

Если f является изоморфизмом, то он монооморфизм.

LaTeX

$$Mono f$$

Lean4

instance (priority := 100) mono_of_iso (f : X ⟶ Y) [IsIso f] : Mono f where
  right_cancellation g h
    w := by rw [← Category.comp_id g, ← Category.comp_id h, ← IsIso.hom_inv_id f, ← Category.assoc, w, ← Category.assoc]

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

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

Разделы

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

Аффилиация

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