instIsDominantOfSurjective

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsDominantOfSurjective

English

If f: X → Y is a surjective morphism, then f is dominant.

Русский

Пусть f: X → Y — сюръективный морфизм; тогда f является доминантным.

LaTeX

$$$\\mathrm{Surjective}(f) \\Rightarrow \\mathrm{IsDominant}(f)$$$

Lean4

instance (priority := 100) [Surjective f] : IsDominant f :=
  ⟨f.surjective.denseRange⟩

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

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

Разделы

Аффилиация

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