Commit 2023-07-01 05:38 b9ff2228

View on Github →

feat: port AlgebraicGeometry.Morphisms.UniversallyClosed (#5637)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean

added theorem AlgebraicGeometry.UniversallyClosed.openCover_iff

added theorem AlgebraicGeometry.morphismRestrict_base

added theorem AlgebraicGeometry.universallyClosed_eq

added theorem AlgebraicGeometry.universallyClosed_is_local_at_target

added theorem AlgebraicGeometry.universallyClosed_respectsIso

added theorem AlgebraicGeometry.universallyClosed_stableUnderBaseChange

added theorem AlgebraicGeometry.universallyClosed_stableUnderComposition