mono_hasImage

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.mono_hasImage

English

If f is mono, then HasImage f holds (via the canonical construction).

Русский

Если f моно, то существует образ f (через каноническую конструкцию).

LaTeX

$$$\text{If } f \text{ is mono, then HasImage } f.$$$

Lean4

instance (priority := 100) mono_hasImage (f : X ⟶ Y) [Mono f] : HasImage f :=
  HasImage.mk ⟨_, IsImage.self f⟩

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

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

Разделы

Аффилиация

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