[Merged by Bors] - chore: Rename Embedding to IsEmbedding

[YaelDillies]

Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards

1. renaming Embedding to IsEmbedding and similarly for neighboring declarations
2. namespacing it inside Topology

---

[github-actions]

PR summary 92a89f313f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Inducing.isEmbedding
+ IsEmbedding
+ IsEmbedding.codRestrict
+ IsEmbedding.comapMetricSpace
+ IsEmbedding.comapUniformSpace
+ IsEmbedding.completelyNormalSpace
+ IsEmbedding.continuousOn_iff
+ IsEmbedding.inclusion
+ IsEmbedding.isCompact_iff
+ IsEmbedding.isLindelof_iff
+ IsEmbedding.isLocallyClosed_iff
+ IsEmbedding.isOpenEmbedding_of_surjective
+ IsEmbedding.isSigmaCompact_iff
+ IsEmbedding.isTotallyDisconnected
+ IsEmbedding.isTotallyDisconnected_image
+ IsEmbedding.isTotallyDisconnected_range
+ IsEmbedding.map_nhdsWithin_eq
+ IsEmbedding.measurableEmbedding
+ IsEmbedding.prodMap
+ IsEmbedding.restrictPreimage
+ IsEmbedding.secondCountableTopology
+ IsEmbedding.separableSpace
+ IsEmbedding.sigmaMk
+ IsEmbedding.subtypeVal
+ IsEmbedding.t0Space
+ IsEmbedding.t1Space
+ IsEmbedding.t25Space
+ IsEmbedding.t2Space
+ IsEmbedding.t3Space
+ IsEmbedding.t5Space
+ IsEmbedding.toPullbackDiag
+ IsEmbedding.to_isometry
+ IsEmbedding.uliftDown
+ IsOpenEmbedding.inducing
+ IsOpenEmbedding.isEmbedding
+ IsOpenEmbedding.of_isEmbedding
+ IsOpenEmbedding.of_isEmbedding_isOpenMap
+ IsQuasiSeparated.image_of_isEmbedding
+ IsUniformEmbedding.isEmbedding
+ Nobeling.isClosedEmbedding
+ PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks
+ PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux
+ Scheme.Hom.isEmbedding
+ Set.restrictPreimage_isEmbedding
+ StrictMono.isEmbedding_of_ordConnected
+ Units.isEmbedding_val
+ Units.isEmbedding_val₀
+ _root_.Function.Injective.isEmbedding_induced
+ _root_.Function.LeftInverse.embedding
+ _root_.Function.LeftInverse.isEmbedding
+ _root_.IsEmbedding.aestronglyMeasurable_comp_iff
+ _root_.IsEmbedding.firstCountableTopology
+ _root_.IsEmbedding.isSeparable_preimage
+ _root_.IsEmbedding.metrizableSpace
+ _root_.IsEmbedding.toHomeomorph_of_surjective
+ antilipschitz_of_isEmbedding
+ closure_eq_preimage_closure_image
+ comp
+ continuous_iff
+ discreteTopology
+ fst_isEmbedding_of_right
+ id
+ inducing
+ instance : (topologically IsEmbedding).RespectsIso
+ instance : PolishSpace EReal := ENNReal.logOrderIso.symm.toHomeomorph.isClosedEmbedding.polishSpace
+ instance [R0Space R] : R0Space C(X, R)₀ := isEmbedding_toContinuousMap.r0Space
+ instance [R1Space R] : R1Space C(X, R)₀ := isEmbedding_toContinuousMap.r1Space
+ instance [RegularSpace R] : RegularSpace C(X, R)₀ := isEmbedding_toContinuousMap.regularSpace
+ instance [T0Space R] : T0Space C(X, R)₀ := isEmbedding_toContinuousMap.t0Space
+ instance [T1Space R] : T1Space C(X, R)₀ := isEmbedding_toContinuousMap.t1Space
+ instance [T2Space R] : T2Space C(X, R)₀ := isEmbedding_toContinuousMap.t2Space
+ instance [T3Space R] : T3Space C(X, R)₀ := isEmbedding_toContinuousMap.t3Space
+ isEmbedding_coe_ennreal
+ isEmbedding_coe_real
+ isEmbedding_diracProba
+ isEmbedding_embedProduct
+ isEmbedding_graph
+ isEmbedding_iff_inducing
+ isEmbedding_iff_of_iSup_eq_top
+ isEmbedding_inclusion
+ isEmbedding_inducingFn
+ isEmbedding_isLocalAtTarget
+ isEmbedding_mk
+ isEmbedding_mk_symm
+ isEmbedding_natCast
+ isEmbedding_of_pullback
+ isEmbedding_outCLM
+ isEmbedding_postcomp
+ isEmbedding_prodMap
+ isEmbedding_prodMk
+ isEmbedding_pullback_to_prod
+ isEmbedding_sigmaMap
+ isEmbedding_sigmaMk_comp
+ isEmbedding_toContinuousMultilinearMap
+ isEmbedding_toUniformOnFun
+ isEmbedding_toWeakDualBCNN
+ isEmbedding_val_mk'
+ isHomeomorph_iff_isEmbedding_surjective
+ isOpenEmbedding_iff_isEmbedding_isOpenMap
+ localization_comap_isEmbedding
+ map_nhds_eq
+ map_nhds_of_mem
+ mk'
+ ofIsEmbedding
+ of_comp
+ of_isEmbedding_isClosedMap
+ of_leftInverse
+ of_subsingleton
+ productOfMemOpens_isEmbedding
+ pullback_map_isEmbedding
+ snd_isEmbedding_of_left
+ t25Space
+ t5Space
+ toFiniteMeasure_isEmbedding
+ totalSpaceMk_isEmbedding
++ IsEmbedding.inl
++ IsEmbedding.inr
++ isEmbedding_coeFn
++ isEmbedding_toContinuousMap
+++ isEmbedding_coe
+++ isEmbedding_restrictScalars
++++++++ isEmbedding
++++++------ embedding
+++--- embedding_coe
+++--- embedding_restrictScalars
++- Embedding.of_comp_iff
++- continuous
++- of_comp_iff
++- tendsto_nhds_iff
++-- embedding_coeFn
++-- embedding_inclusion
++-- embedding_inr
++-- embedding_toContinuousMap
+-+-+- t2Space
+-- embedding_inl
+--++- instT2Space
- Embedding.continuous
- Embedding.secondCountableTopology
- Embedding.separableSpace
- Embedding.tendsto_nhds_iff
- Function.LeftInverse.embedding
- PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux
- embedding_isLocalAtTarget
- instance : (topologically Embedding).RespectsIso
- instance : PolishSpace EReal
- instance [R0Space R] : R0Space C(X, R)₀ := embedding_toContinuousMap.r0Space
- instance [R1Space R] : R1Space C(X, R)₀ := embedding_toContinuousMap.r1Space
- instance [RegularSpace R] : RegularSpace C(X, R)₀ := embedding_toContinuousMap.regularSpace
- instance [T0Space R] : T0Space C(X, R)₀ := embedding_toContinuousMap.t0Space
- instance [T1Space R] : T1Space C(X, R)₀ := embedding_toContinuousMap.t1Space
- instance [T2Space R] : T2Space C(X, R)₀ := embedding_toContinuousMap.t2Space
- instance [T3Space R] : T3Space C(X, R)₀ := embedding_toContinuousMap.t3Space
- openEmbedding_mk_symm
-+-+ instT3Space

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.

[jcommelin]

bors d+

[mathlib-bors]

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

[YaelDillies]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style