Commit 2025-06-13 16:19 503e5273

View on Github →

feat(AlgebraicGeometry): inverse limit of nonempty quasicompact closeds is nonempty (#25105)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

added theorem exists_mem_of_isClosed_of_nonempty'

added theorem exists_mem_of_isClosed_of_nonempty

Modified Mathlib/AlgebraicGeometry/Morphisms/Separated.lean

added theorem AlgebraicGeometry.IsAffineHom.comp_iff

added theorem AlgebraicGeometry.IsAffineHom.of_comp

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

added theorem CategoryTheory.Over.forall_iff

added theorem CategoryTheory.Under.forall_iff