Commit 2024-01-25 16:42 e7170d39

View on Github →

feat(Topology/Basic): add TopologicalSpace.ext_isClosed (#9963) Use it to golf PrimeSpectrum.localization_comap_inducing.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

Modified Mathlib/Topology/Basic.lean

added theorem TopologicalSpace.ext_iff_isClosed