Theorem exists_mem_of_isClosed_of_nonempty

Modification history

2025-09-27 10:51
Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean
feat(AlgebraicGeometry): inverse limits and schemes of finite type (#25941) …
Deleted exists_mem_of_isClosed_of_nonemptyView on Github →
2025-06-13 16:19
Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean
feat(AlgebraicGeometry): inverse limit of nonempty quasicompact closeds is nonempty (#25105)
Added exists_mem_of_isClosed_of_nonemptyView on Github →