theorem AlgebraicGeometry.exists_maximal_extension_of_irreducible_separated {X Y : Scheme} [IrreducibleSpace ↥X] [IsReduced X] [Y.IsSeparated] (f : X.PartialMap Y) : ∃ (g : X.PartialMap Y), g.equiv f ∧ ∀ (h : X.PartialMap Y), h.equiv f → h.domain ≤ g.domain

For X irreducible reduced and Y separated, every partial map f : U → Y extends to a maximal partial map g : V → Y with U ⊆ V, i.e. any partial map in the same equivalence class is dominated by g (Cor 14, Lec 7).