nonzero_image_of_nonzero

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

English

If f ≠ 0, then image.ι f ≠ 0 (has image).

Русский

Если f ≠ 0, тогда image.ι f ≠ 0 (существует образ).

LaTeX

$$$f \\neq 0 \\Rightarrow \\mathrm{image.ι}(f) \\neq 0$$$

Lean4

theorem nonzero_image_of_nonzero {X Y : C} {f : X ⟶ Y} [HasImage f] (w : f ≠ 0) : image.ι f ≠ 0 := fun h =>
  w (eq_zero_of_image_eq_zero h)

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

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

Разделы

Аффилиация

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