[Merged by Bors] - feat: add IsEmbedding.sumElim_of_separatingNhds

[grunweg]

Characterise when the Sum.elim of two inducing maps resp. embeddings is an embedding,
and deduce that the ranges of the two maps lying in separated neighbourhoods suffices.

This is used in my bordism theory project.

Co-authored by: @plp127

---

This PR was manually re-created (and migrated to a fork at the same time) from #22137, since that seemed easiest.

[github-actions]

PR summary 9a749a69c4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Constructions.SumProd	592	594	+2 (+0.34%)

Import changes for all files

Files	Import difference
48 files Mathlib.Data.Analysis.Topology Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.Topology.AlexandrovDiscrete Mathlib.Topology.Algebra.Indicator Mathlib.Topology.Bases Mathlib.Topology.Clopen Mathlib.Topology.Coherent Mathlib.Topology.Compactness.Bases Mathlib.Topology.Compactness.Compact Mathlib.Topology.Compactness.CompactlyCoherentSpace Mathlib.Topology.Compactness.Exterior Mathlib.Topology.Compactness.Lindelof Mathlib.Topology.Compactness.LocallyCompact Mathlib.Topology.Compactness.LocallyFinite Mathlib.Topology.Compactness.NhdsKer Mathlib.Topology.Compactness.SigmaCompact Mathlib.Topology.Connected.Basic Mathlib.Topology.Connected.Clopen Mathlib.Topology.Connected.LocallyConnected Mathlib.Topology.Connected.TotallyDisconnected Mathlib.Topology.Constructions Mathlib.Topology.ContinuousOn Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.Exterior Mathlib.Topology.Hom.ContinuousEvalConst Mathlib.Topology.Hom.ContinuousEval Mathlib.Topology.Inseparable Mathlib.Topology.Irreducible Mathlib.Topology.List Mathlib.Topology.LocallyClosed Mathlib.Topology.LocallyFinite Mathlib.Topology.MetricSpace.BundledFun Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.NhdsKer Mathlib.Topology.Order.LeftRight Mathlib.Topology.Order.LocalExtr Mathlib.Topology.Order.Priestley Mathlib.Topology.Piecewise Mathlib.Topology.PreorderRestrict Mathlib.Topology.UniformSpace.Basic Mathlib.Topology.UniformSpace.Compact Mathlib.Topology.UniformSpace.DiscreteUniformity Mathlib.Topology.UniformSpace.Ultra.Basic	1
5 files Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Group.Defs Mathlib.Topology.Algebra.Monoid.Defs Mathlib.Topology.Constructions.SumProd Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle	2

---

Declarations diff

+ IsInducing.sumSwap
+ IsOpenEmbedding.sumSwap
+ Topology.IsEmbedding.sumElim
+ Topology.IsEmbedding.sumElim_left
+ Topology.IsEmbedding.sumElim_of_separatedNhds
+ Topology.IsEmbedding.sumElim_right
+ Topology.IsInducing.disjoint_of_sumElim_aux
+ Topology.IsInducing.sumElim
+ Topology.IsInducing.sumElim_left
+ Topology.IsInducing.sumElim_of_separatedNhds
+ Topology.IsInducing.sumElim_right
+ elim_swap
+ isEmbedding_sumElim
+ isInducing_sumElim

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Thanks for the golfs! This is ready for review again.

[ADedecker]

Thanks!

maintainer delegate

[github-actions]

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

[PatrickMassot]

bors merge

[mathlib-bors]

Build failed (retrying...):

• CI Success

[bryangingechen]

bors r+

[mathlib-bors]

Build failed:

• CI Success

[bryangingechen]

Thanks!
bors d+

[mathlib-bors]

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

[grunweg]

CI passes, so let's try again
bors merge

[bryangingechen]

This fell off the queue
bors r+

[bryangingechen]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success

[grunweg]

Thank you for the reviews, and the patient help with re-borsing.