Commit 2024-07-20 19:55 7c3b2120

View on Github →

feat(AlgebraicGeometry): Morphism properties local at the source. (#14946)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

added theorem AlgebraicGeometry.IsLocalAtSource.comp

added theorem AlgebraicGeometry.IsLocalAtSource.iff_of_iSup_eq_top

added theorem AlgebraicGeometry.IsLocalAtSource.iff_of_openCover

added theorem AlgebraicGeometry.IsLocalAtSource.isLocalAtTarget

added theorem AlgebraicGeometry.IsLocalAtSource.of_iSup_eq_top

added theorem AlgebraicGeometry.IsLocalAtSource.of_isOpenImmersion

added theorem AlgebraicGeometry.IsLocalAtSource.of_openCover