kernel_not_epi_of_nonzero

Mathlib.CategoryTheory.Limits.Shapes.Kernels

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

English

If f ≠ 0, then kernel.ι f is not epi.

Русский

Если f не ноль, то kernel.ι f не эпиморфизм.

LaTeX

$$$f \\neq 0 \\Rightarrow \\lnot \\operatorname{Epi}(\\ker f)$$$

Lean4

theorem kernel_not_epi_of_nonzero (w : f ≠ 0) : ¬Epi (kernel.ι f) := fun _ => w (eq_zero_of_epi_kernel f)

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

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

Разделы

Аффилиация

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