strongMono_of_mono

Mathlib.CategoryTheory.Limits.Shapes.StrongEpi

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

English

In a StrongMonoCategory, every mono morphism is a strong mono.

Русский

В категории с StrongMonoCategory каждый моно-морфизм является сильным моно.

LaTeX

$$$\\forall f:\\, P \\to Q,\\ [\\mathrm{Mono}(f)]\\Rightarrow \\mathrm{StrongMono}(f).$$$

Lean4

theorem strongMono_of_mono [StrongMonoCategory C] (f : P ⟶ Q) [Mono f] : StrongMono f :=
  StrongMonoCategory.strongMono_of_mono _

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

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

Разделы

Аффилиация

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