Commit 2024-10-28 15:52 91c49567

View on Github →

feat(Topology) define jacobson spaces (#18243)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/JacobsonSpace.lean

added theorem IsClosedEmbedding.preimage_closedPoints

added theorem IsOpenEmbedding.preimage_closedPoints

added theorem JacobsonSpace.discreteTopology

added theorem JacobsonSpace.of_isClosedEmbedding

added theorem JacobsonSpace.of_isOpenEmbedding

added def closedPoints

added theorem closedPoints_eq_univ

added theorem closure_closedPoints

added theorem isClosed_singleton_of_isLocallyClosed_singleton

added theorem jacobsonSpace_iff_locallyClosed

added theorem jacobsonSpace_iff_of_iSup_eq_top

added theorem mem_closedPoints_iff

added theorem nonempty_inter_closedPoints

added theorem preimage_closedPoints_subset

Modified scripts/noshake.json