surjective — Mathlib

English

Let X and Y be schemes and f: X → Y a morphism which is surjective. Then the induced map on the underlying topological spaces f_base: |X| → |Y| is surjective.

Русский

Пусть X и Y — схемы, f: X → Y — морфизм, который сюръективен. Тогда отображение f_base между фундаментальными топологическими пространствами |X| и |Y| сюръективно.

LaTeX

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

Lean4

theorem surjective (f : X.Hom Y) [Surjective f] : Function.Surjective f.base :=
  Surjective.surj

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