[Merged by Bors] - feat(Topology/Inseparable): Define specializing maps between topological spaces

[erdOne]

A port of leanprover-community/mathlib3#17113

---

[github-actions]

PR summary b023c877be

Import changes

No significant changes to the import graph

---

Declarations diff

+ Fibration.isLowerSet_image
+ Fibration.isUpperSet_image
+ GeneralizingMap
+ GeneralizingMap.stableUnderGeneralization_image
+ GeneralizingMap.stableUnderGeneralization_range
+ GeneralizingMap_iff_stableUnderGeneralization_image
+ Inducing.generalizingMap
+ Inducing.specializingMap
+ IsClosed.stableUnderSpecialization
+ IsClosedMap.specializingMap
+ IsOpen.stableUnderGeneralization
+ OpenEmbedding.generalizingMap
+ SpecializingMap
+ SpecializingMap.stableUnderSpecialization_image
+ SpecializingMap.stableUnderSpecialization_range
+ StableUnderGeneralization
+ StableUnderGeneralization.image
+ StableUnderGeneralization.preimage
+ StableUnderSpecialization
+ StableUnderSpecialization.image
+ StableUnderSpecialization.preimage
+ Union_closure_singleton_eq_iff
+ _root_.IsLowerSet.image_fibration
+ _root_.IsUpperSet.image_fibration
+ closure_singleton_eq_Iic
+ fibration_iff_image_Ici
+ fibration_iff_image_Iic
+ fibration_iff_isLowerSet_image
+ fibration_iff_isLowerSet_image_Iic
+ fibration_iff_isUpperSet_image
+ fibration_iff_isUpperSet_image_Ici
+ lowerClosure_eq
+ specializingMap_iff_closure_singleton
+ specializingMap_iff_closure_singleton_subset
+ specializingMap_iff_isClosed_image_closure_singleton
+ specializingMap_iff_stableUnderSpecialization_image
+ specializingMap_iff_stableUnderSpecialization_image_singleton
+ stableUnderGeneralization_compl_iff
+ stableUnderGeneralization_empty
+ stableUnderGeneralization_iInter
+ stableUnderGeneralization_iUnion
+ stableUnderGeneralization_iff_exists_sInter_eq
+ stableUnderGeneralization_sInter
+ stableUnderGeneralization_sUnion
+ stableUnderGeneralization_univ
+ stableUnderSpecialization_compl_iff
+ stableUnderSpecialization_empty
+ stableUnderSpecialization_iInter
+ stableUnderSpecialization_iUnion
+ stableUnderSpecialization_iff_Union_eq
+ stableUnderSpecialization_iff_exists_sUnion_eq
+ stableUnderSpecialization_sInter
+ stableUnderSpecialization_sUnion
+ stableUnderSpecialization_univ
+ upperClosure_eq
+ ⟨SpecializingMap.closure_singleton_subset,
+ ⟨StableUnderSpecialization.Union_eq,
++ ⟨_,

You can run this locally as follows

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

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

[alreadydone]

Since I approved the mathlib3 PR, I'd approve this too once indentation is fixed.

[alreadydone]

You're close, just four are remaining!

[alreadydone]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[kim-em]

bors merge

[mathlib-bors]

Build failed:

• Build

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style