[Merged by Bors] - chore(Topology): Namespace Inducing, Embedding...#15993
[Merged by Bors] - chore(Topology): Namespace Inducing, Embedding...#15993YaelDillies wants to merge 2 commits intomasterfrom
Inducing, Embedding...#15993Conversation
PR summary 648e2527c8Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
ddc146a to
ecd9391
Compare
ecd9391 to
5b82c0e
Compare
101a6ad to
1c15450
Compare
f1e6eef to
b350e1a
Compare
b350e1a to
e417d5e
Compare
`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 neighborhing declarations (which `DenseInducing` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
7276276 to
d63d4a5
Compare
bb82428 to
ef5bdea
Compare
ef5bdea to
f8ef322
Compare
`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 neighborhing declarations (which `OpenEmbedding` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
`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 neighborhing declarations (which `OpenEmbedding` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
`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 neighborhing declarations (which `OpenEmbedding` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
`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 neighborhing declarations (which `ClosedEmbedding` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context.
f8ef322 to
ecaa2b3
Compare
| @[deprecated (since := "2024-10-20")] | ||
| alias ClosedEmbedding.measurableEmbedding := IsClosedEmbedding.measurableEmbedding |
There was a problem hiding this comment.
Do we now need another alias for IsClosedEmbedding.measurableEmbedding → Topology.IsClosedEmbedding.measurableEmbedding? And similarly everywhere else. Or do you claim that the renames are close enough together in time that we only need the one already present?
There was a problem hiding this comment.
It is really really timetaking to write deprecated aliases manually and in that case the renames were indeed pretty close in time, so I'm of the opinion to stick to whatever scripts/add_deprecations.sh generated
|
Please add |
|
Thanks! 🎉 |
|
Build failed: |
|
As this PR is labelled bors merge |
|
Pull request successfully merged into master. Build succeeded: |
We don't add deprecated aliases because definitions only gained a namespace and the presence of both namespaced and unnamespaced declarations would confuse Lean. Furthermore,
_root_.IsInducing,_root_.IsEmbedding, etc... only existed for a short while.Moves:
IsInducing→Topology.IsInducingIsEmbedding→Topology.IsEmbeddingIsOpenEmbedding→Topology.IsOpenEmbeddingIsClosedEmbedding→Topology.IsClosedEmbeddingIsQuotientMap→Topology.IsQuotientMapIsClosedEmbedding.LindelofSpace→Topology.IsClosedEmbedding.LindelofSpaceIsClosedEmbedding.compactSpace→Topology.IsClosedEmbedding.compactSpaceIsClosedEmbedding.inl→Topology.IsClosedEmbedding.inlIsClosedEmbedding.inr→Topology.IsClosedEmbedding.inrIsClosedEmbedding.isCompact_preimage→Topology.IsClosedEmbedding.isCompact_preimageIsClosedEmbedding.isLindelof_preimage→Topology.IsClosedEmbedding.isLindelof_preimageIsClosedEmbedding.isProperMap→Topology.IsClosedEmbedding.isProperMapIsClosedEmbedding.locallyCompactSpace→Topology.IsClosedEmbedding.locallyCompactSpaceIsClosedEmbedding.measurableEmbedding→Topology.IsClosedEmbedding.measurableEmbeddingIsClosedEmbedding.nonLindelofSpace→Topology.IsClosedEmbedding.nonLindelofSpaceIsClosedEmbedding.noncompactSpace→Topology.IsClosedEmbedding.noncompactSpaceIsClosedEmbedding.normalSpace→Topology.IsClosedEmbedding.normalSpaceIsClosedEmbedding.paracompactSpace→Topology.IsClosedEmbedding.paracompactSpaceIsClosedEmbedding.preimage_closedPoints→Topology.IsClosedEmbedding.preimage_closedPointsIsClosedEmbedding.quasiSober→Topology.IsClosedEmbedding.quasiSoberIsClosedEmbedding.restrictPreimage→Topology.IsClosedEmbedding.restrictPreimageIsClosedEmbedding.sigmaCompactSpace→Topology.IsClosedEmbedding.sigmaCompactSpaceIsClosedEmbedding.sigmaMk→Topology.IsClosedEmbedding.sigmaMkIsClosedEmbedding.subtypeVal→Topology.IsClosedEmbedding.subtypeValIsClosedEmbedding.t4Space→Topology.IsClosedEmbedding.t4SpaceIsClosedEmbedding.tendsto_coLindelof→Topology.IsClosedEmbedding.tendsto_coLindelofIsClosedEmbedding.tendsto_cocompact→Topology.IsClosedEmbedding.tendsto_cocompactIsClosedEmbedding.uliftDown→Topology.IsClosedEmbedding.uliftDownIsClosedEmbedding.weaklyLocallyCompactSpace→Topology.IsClosedEmbedding.weaklyLocallyCompactSpaceIsEmbedding.codRestrict→Topology.IsEmbedding.codRestrictIsEmbedding.comapMetricSpace→Topology.IsEmbedding.comapMetricSpaceIsEmbedding.comapUniformSpace→Topology.IsEmbedding.comapUniformSpaceIsEmbedding.completelyNormalSpace→Topology.IsEmbedding.completelyNormalSpaceIsEmbedding.continuousOn_iff→Topology.IsEmbedding.continuousOn_iffIsEmbedding.inclusion→Topology.IsEmbedding.inclusionIsEmbedding.inl→Topology.IsEmbedding.inlIsEmbedding.inr→Topology.IsEmbedding.inrIsEmbedding.isCompact_iff→Topology.IsEmbedding.isCompact_iffIsEmbedding.isLindelof_iff→Topology.IsEmbedding.isLindelof_iffIsEmbedding.isLocallyClosed_iff→Topology.IsEmbedding.isLocallyClosed_iffIsEmbedding.isSigmaCompact_iff→Topology.IsEmbedding.isSigmaCompact_iffIsEmbedding.isTotallyDisconnected→Topology.IsEmbedding.isTotallyDisconnectedIsEmbedding.isTotallyDisconnected_image→Topology.IsEmbedding.isTotallyDisconnected_imageIsEmbedding.isTotallyDisconnected_range→Topology.IsEmbedding.isTotallyDisconnected_rangeIsEmbedding.map_nhdsWithin_eq→Topology.IsEmbedding.map_nhdsWithin_eqIsEmbedding.measurableEmbedding→Topology.IsEmbedding.measurableEmbeddingIsEmbedding.prodMap→Topology.IsEmbedding.prodMapIsEmbedding.restrictPreimage→Topology.IsEmbedding.restrictPreimageIsEmbedding.secondCountableTopology→Topology.IsEmbedding.secondCountableTopologyIsEmbedding.separableSpace→Topology.IsEmbedding.separableSpaceIsEmbedding.sigmaMk→Topology.IsEmbedding.sigmaMkIsEmbedding.subtypeVal→Topology.IsEmbedding.subtypeValIsEmbedding.t0Space→Topology.IsEmbedding.t0SpaceIsEmbedding.t1Space→Topology.IsEmbedding.t1SpaceIsEmbedding.t25Space→Topology.IsEmbedding.t25SpaceIsEmbedding.t2Space→Topology.IsEmbedding.t2SpaceIsEmbedding.t3Space→Topology.IsEmbedding.t3SpaceIsEmbedding.t5Space→Topology.IsEmbedding.t5SpaceIsEmbedding.toPullbackDiag→Topology.IsEmbedding.toPullbackDiagIsEmbedding.to_isometry→Topology.IsEmbedding.to_isometryIsEmbedding.uliftDown→Topology.IsEmbedding.uliftDownIsInducing.alexandrovDiscrete→Topology.IsInducing.alexandrovDiscreteIsInducing.codRestrict→Topology.IsInducing.codRestrictIsInducing.comapPseudoMetricSpace→Topology.IsInducing.comapPseudoMetricSpaceIsInducing.continuousConstSMul→Topology.IsInducing.continuousConstSMulIsInducing.continuousInv→Topology.IsInducing.continuousInvIsInducing.continuousMul→Topology.IsInducing.continuousMulIsInducing.continuousOn_iff→Topology.IsInducing.continuousOn_iffIsInducing.continuousSMul→Topology.IsInducing.continuousSMulIsInducing.continuousWithinAt_iff→Topology.IsInducing.continuousWithinAt_iffIsInducing.frechetUrysohnSpace→Topology.IsInducing.frechetUrysohnSpaceIsInducing.generalizingMap→Topology.IsInducing.generalizingMapIsInducing.hasProd_iff→Topology.IsInducing.hasProd_iffIsInducing.injective→Topology.IsInducing.injectiveIsInducing.inseparable_iff→Topology.IsInducing.inseparable_iffIsInducing.isClosedMap→Topology.IsInducing.isClosedMapIsInducing.isCompact_iff→Topology.IsInducing.isCompact_iffIsInducing.isCompact_preimage→Topology.IsInducing.isCompact_preimageIsInducing.isCompact_preimage'→Topology.IsInducing.isCompact_preimage'IsInducing.isCompact_preimage_iff→Topology.IsInducing.isCompact_preimage_iffIsInducing.isEmbedding→Topology.IsInducing.isEmbeddingIsInducing.isLindelof_iff→Topology.IsInducing.isLindelof_iffIsInducing.isLindelof_preimage→Topology.IsInducing.isLindelof_preimageIsInducing.isLocallyClosed_iff→Topology.IsInducing.isLocallyClosed_iffIsInducing.isOpenMap→Topology.IsInducing.isOpenMapIsInducing.isPathConnected_iff→Topology.IsInducing.isPathConnected_iffIsInducing.isPreconnected_image→Topology.IsInducing.isPreconnected_imageIsInducing.isSigmaCompact_iff→Topology.IsInducing.isSigmaCompact_iffIsInducing.joinedIn_image→Topology.IsInducing.joinedIn_imageIsInducing.locallyCompactSpace→Topology.IsInducing.locallyCompactSpaceIsInducing.multipliable_iff_tprod_comp_mem_range→Topology.IsInducing.multipliable_iff_tprod_comp_mem_rangeIsInducing.of_codRestrict→Topology.IsInducing.of_codRestrictIsInducing.prodMap→Topology.IsInducing.prodMapIsInducing.r0Space→Topology.IsInducing.r0SpaceIsInducing.r1Space→Topology.IsInducing.r1SpaceIsInducing.regularSpace→Topology.IsInducing.regularSpaceIsInducing.restrictPreimage→Topology.IsInducing.restrictPreimageIsInducing.secondCountableTopology→Topology.IsInducing.secondCountableTopologyIsInducing.specializes_iff→Topology.IsInducing.specializes_iffIsInducing.specializingMap→Topology.IsInducing.specializingMapIsInducing.subtypeVal→Topology.IsInducing.subtypeValIsInducing.topologicalGroup→Topology.IsInducing.topologicalGroupIsInducing.withSeminorms→Topology.IsInducing.withSeminormsIsOpenEmbedding.coborder_preimage→Topology.IsOpenEmbedding.coborder_preimageIsOpenEmbedding.compatiblePreserving→Topology.IsOpenEmbedding.compatiblePreservingIsOpenEmbedding.functor_isContinuous→Topology.IsOpenEmbedding.functor_isContinuousIsOpenEmbedding.functor_obj_injective→Topology.IsOpenEmbedding.functor_obj_injectiveIsOpenEmbedding.inl→Topology.IsOpenEmbedding.inlIsOpenEmbedding.inr→Topology.IsOpenEmbedding.inrIsOpenEmbedding.isLocalHomeomorph→Topology.IsOpenEmbedding.isLocalHomeomorphIsOpenEmbedding.isQuasiSeparated_iff→Topology.IsOpenEmbedding.isQuasiSeparated_iffIsOpenEmbedding.locPathConnectedSpace→Topology.IsOpenEmbedding.locPathConnectedSpaceIsOpenEmbedding.locallyCompactSpace→Topology.IsOpenEmbedding.locallyCompactSpaceIsOpenEmbedding.locallyConnectedSpace→Topology.IsOpenEmbedding.locallyConnectedSpaceIsOpenEmbedding.map_nhdsWithin_preimage_eq→Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eqIsOpenEmbedding.measurableEmbedding→Topology.IsOpenEmbedding.measurableEmbeddingIsOpenEmbedding.preimage_closedPoints→Topology.IsOpenEmbedding.preimage_closedPointsIsOpenEmbedding.prodMap→Topology.IsOpenEmbedding.prodMapIsOpenEmbedding.quasiSober→Topology.IsOpenEmbedding.quasiSoberIsOpenEmbedding.restrictPreimage→Topology.IsOpenEmbedding.restrictPreimageIsOpenEmbedding.sigmaMk→Topology.IsOpenEmbedding.sigmaMkIsOpenEmbedding.singleton_smoothManifoldWithCorners→Topology.IsOpenEmbedding.singleton_smoothManifoldWithCornersIsQuotientMap.continuousOn_isOpen_iff→Topology.IsQuotientMap.continuousOn_isOpen_iffIsQuotientMap.continuous_lift_prod_left→Topology.IsQuotientMap.continuous_lift_prod_leftIsQuotientMap.continuous_lift_prod_right→Topology.IsQuotientMap.continuous_lift_prod_rightIsQuotientMap.image_connectedComponent→Topology.IsQuotientMap.image_connectedComponentIsQuotientMap.isClopen_preimage→Topology.IsQuotientMap.isClopen_preimageIsQuotientMap.preimage_connectedComponent→Topology.IsQuotientMap.preimage_connectedComponentIsQuotientMap.restrictPreimage_isOpen→Topology.IsQuotientMap.restrictPreimage_isOpenIsQuotientMap.sequentialSpace→Topology.IsQuotientMap.sequentialSpaceisEmbedding_sigmaMap→Topology.isEmbedding_sigmaMapisInducing_const_prod→+ Topology.isInducing_const_prodisInducing_prod_const→+ Topology.isInducing_prod_constisInducing_sigmaMap→+ Topology.isInducing_sigmaMapisOpenEmbedding_sigmaMap→+ Topology.isOpenEmbedding_sigmaMapIsClosedEmbedding.integral_map→+ Topology.IsClosedEmbedding.integral_mapIsClosedEmbedding.polishSpace→Topology.IsClosedEmbedding.polishSpaceIsClosedEmbedding.setIntegral_map→Topology.IsClosedEmbedding.setIntegral_mapIsEmbedding.aestronglyMeasurable_comp_iff→Topology.IsEmbedding.aestronglyMeasurable_comp_iffIsEmbedding.firstCountableTopology→Topology.IsEmbedding.firstCountableTopologyIsEmbedding.metrizableSpace→Topology.IsEmbedding.metrizableSpaceIsEmbedding.toHomeomorph_of_surjective→Topology.IsEmbedding.toHomeomorph_of_surjectiveIsInducing.firstCountableTopology→Topology.IsInducing.firstCountableTopologyIsInducing.noetherianSpace→Topology.IsInducing.noetherianSpaceIsInducing.pseudoMetrizableSpace→Topology.IsInducing.pseudoMetrizableSpaceIsQuotientMap.secondCountableTopology→Topology.IsQuotientMap.secondCountableTopologyIsQuotientMap.separableSpace→Topology.IsQuotientMapTopology.RestrictGenTopologytoTopology.RestrictGen#16087DenseInducingtoIsDenseInducing#17208DenseEmbeddingtoIsDenseEmbedding#17247UniformEmbeddingtoIsUniformEmbedding#17295UniformInducingtoIsUniformInducing#17398OpenEmbeddingtoIsOpenEmbedding#17898ClosedEmbeddingtoIsClosedEmbedding#17937QuotientMaptoIsQuotientMap#18062EmbeddingtoIsEmbedding#18133InducingtoIsInducing#18330