mono_iff_mono_right

Mathlib.CategoryTheory.Limits.Over

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.mono_iff_mono_right

English

Under the pullback setting, h is mono iff h.right is mono.

Русский

При наличии пуллбака, h моно тогда и только тогда, когда h.right моно.

LaTeX

$$$ \\text{Mono}(h) \\iff \\text{Mono}(h.right). $$$

Lean4

theorem mono_iff_mono_right [HasPullbacks C] {f g : Under X} (h : f ⟶ g) : Mono h ↔ Mono h.right :=
  StructuredArrow.mono_iff_mono_right _

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

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

Разделы

Аффилиация

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