From a8ae1b3f7979249a0af6bc7cf20c1f6bf656ca73 Mon Sep 17 00:00:00 2001
From: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Date: Wed, 26 Oct 2022 07:42:19 +0000
Subject: [PATCH] fix(algebraic_geometry/morphisms/universally_closed): Fix
 docstring. (#17135)

---
 src/algebraic_geometry/morphisms/universally_closed.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/algebraic_geometry/morphisms/universally_closed.lean b/src/algebraic_geometry/morphisms/universally_closed.lean
index 6a70e992d04cf..036ff1844d1d9 100644
--- a/src/algebraic_geometry/morphisms/universally_closed.lean
+++ b/src/algebraic_geometry/morphisms/universally_closed.lean
@@ -31,8 +31,8 @@ open category_theory.morphism_property
 open algebraic_geometry.morphism_property (topologically)
 
 /--
-A morphism of schemes `f : X ⟶ Y` is locally of finite type if for each affine `U ⊆ Y` and
-`V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
+A morphism of schemes `f : X ⟶ Y` is universally closed if the base change `X ×[Y] Y' ⟶ Y'`
+along any morphism `Y' ⟶ Y` is (topologically) a closed map.
 -/
 @[mk_iff]
 class universally_closed (f : X ⟶ Y) : Prop :=