surjective_mk — Mathlib

English

Let X be a topological space and π: X → SeparationQuotient X be the canonical quotient map. Then π is surjective.

Русский

Пусть X — топологическое пространство и π: X → SeparationQuotient X — каноническое отображение. Тогда π сюръективно.

LaTeX

$$$\\forall y \\in \\mathrm{SeparationQuotient}(X), \\exists x \\in X, \\pi(x) = y$$$

Lean4

theorem surjective_mk : Surjective (mk : X → SeparationQuotient X) :=
  Quot.mk_surjective

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