epi_iff_surjective

Mathlib.Algebra.Category.ModuleCat.EpiMono

URI: https://scilib.ai/kg/mathlib#ModuleCat.epi_iff_surjective

English

An epimorphism f is equivalent to being surjective on the underlying set.

Русский

Эпиморфизм эквивалент тому, что отображение сюръективно по множеству элементов.

LaTeX

$$$\\text{Epi}(f) \\iff \\text{Function.Surjective}(f)$$$

Lean4

theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

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

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

Разделы

Аффилиация

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