Commit 2024-11-11 19:06 aef008c6
View on Github →chore(Topology): Namespace Inducing, Embedding... (#15993)
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.IsQuotientMap