[Merged by Bors] - feat(Topology/LocallyClosed): Define locally closed sets

[erdOne]

---

[github-actions]

PR summary dd9ad5240f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.LocallyClosed	686

---

Declarations diff

+ Continuous.preimage_coborder_subset
+ Embedding.isLocallyClosed_iff
+ Inducing.isLocallyClosed_iff
+ IsClosed.coborder_eq
+ IsClosed.isLocallyClosed
+ IsLocallyClosed
+ IsLocallyClosed.image
+ IsLocallyClosed.inter
+ IsLocallyClosed.isOpen_coborder
+ IsLocallyClosed.isOpen_preimage_val_closure
+ IsLocallyClosed.preimage
+ IsOpen.coborder_eq
+ IsOpen.isLocallyClosed
+ IsOpenMap.coborder_preimage_subset
+ OpenEmbedding.coborder_preimage
+ closure_inter_coborder
+ coborder
+ coborder_eq_compl_frontier_iff
+ coborder_eq_union_frontier_compl
+ coborder_eq_univ_iff
+ coborder_inter_closure
+ coborder_preimage
+ disjoint_frontier_iff_isOpen
+ frontier_subset_iff_isClosed
+ isClosed_preimage_val
+ isClosed_preimage_val_coborder
+ isLocallyClosed_iff_coe_preimage_of_iSup_eq_top
+ isLocallyClosed_iff_isOpen_coborder
+ isLocallyClosed_tfae
+ subset_coborder
++++ _

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>

[fpvandoorn]

Looks mostly good to me.

Please open the Set namespace and remove Set. prefixes.

[fpvandoorn]

One more comments, otherwise LGTM

bors d+

[mathlib-bors]

✌️ 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]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style