toRationalMap_surjective — Mathlib

English

Every rational map from X to Y arises from a partial map; the map toRationalMap is surjective.

Русский

Каждая рациональная карта от X к Y порождается частичной картой; отображение toRationalMap сюрьективно.

LaTeX

$$$\text{Surjective}\,(\text{toRationalMap}: X.PartialMap Y \to X.RationalMap Y)$$$

Lean4

theorem toRationalMap_surjective : Function.Surjective (@toRationalMap X Y) :=
  Quotient.exists_rep

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