feat(Topology) define jacobson spaces

[erdOne]

---

[github-actions[bot]]

PR summary c7b1fee561

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.JacobsonSpace	688

---

Declarations diff

+ IsClosedEmbedding.preimage_closedPoints + IsOpenEmbedding.preimage_closedPoints + JacobsonSpace + JacobsonSpace.discreteTopology + JacobsonSpace.of_isClosedEmbedding + JacobsonSpace.of_isOpenEmbedding + closedPoints + closedPoints_eq_univ + closure_closedPoints + instance (priority := 100) [Finite X] [JacobsonSpace X] : DiscreteTopology X + instance (priority := 100) [T2Space X] : JacobsonSpace X + isClosed_singleton_of_isLocallyClosed_singleton + jacobsonSpace_iff_locallyClosed + jacobsonSpace_iff_of_iSup_eq_top + mem_closedPoints_iff + nonempty_inter_closedPoints + preimage_closedPoints_subset

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib-bors[bot]]

:v: erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

bors merge

[mathlib-bors[bot]]

Build failed (retrying...):

• Build

[mathlib-bors[bot]]

Canceled.

[erdOne]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style