of_comp

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Surjective.of_comp

English

If the composition f ≫ g is surjective, then g is surjective.

Русский

Если композиция f ≫ g сюръективна, то g сюръективен.

LaTeX

$$$\mathrm{Surjective}(g_{\mathrm{base}})$$$

Lean4

theorem of_comp [Surjective (f ≫ g)] : Surjective g where
  surj := Function.Surjective.of_comp (g := f.base) (f ≫ g).surjective

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

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

Разделы

Аффилиация

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