Commit 2024-10-28 08:46 a9ecf75b

View on Github →

chore: Rename Embedding to IsEmbedding (#18133) 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

renaming Embedding to IsEmbedding and similarly for neighboring declarations (which Embedding is)
namespacing it inside Topology

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

deleted theorem AlgebraicGeometry.Scheme.Hom.embedding

added theorem AlgebraicGeometry.Scheme.Hom.isEmbedding

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

deleted theorem PrimeSpectrum.localization_comap_embedding

added theorem PrimeSpectrum.localization_comap_isEmbedding

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean

deleted theorem PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks

deleted theorem PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux

added theorem PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks

added theorem PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/ResidueField.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

deleted theorem UpperHalfPlane.embedding_coe

added theorem UpperHalfPlane.isEmbedding_coe

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/Normed/Module/WeakDual.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

added theorem LinearIsometry.isEmbedding

Modified Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean

deleted theorem ContinuousLinearMapWOT.embedding_inducingFn

added theorem ContinuousLinearMapWOT.isEmbedding_inducingFn

Modified Mathlib/Analysis/Normed/Ring/Units.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean

deleted theorem ContinuousLinearMap.antilipschitz_of_embedding

added theorem ContinuousLinearMap.antilipschitz_of_isEmbedding

Modified Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Galois/Topology.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

deleted theorem Embedding.aestronglyMeasurable_comp_iff

added theorem IsEmbedding.aestronglyMeasurable_comp_iff

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Measure/DiracProba.lean

deleted theorem MeasureTheory.embedding_diracProba

added theorem MeasureTheory.isEmbedding_diracProba

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

deleted theorem MeasureTheory.FiniteMeasure.embedding_toWeakDualBCNN

added theorem MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN

Modified Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

deleted theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_embedding

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding

Modified Mathlib/Topology/Algebra/Constructions.lean

deleted theorem Units.embedding_embedProduct

deleted theorem Units.embedding_val_mk'

added theorem Units.isEmbedding_embedProduct

added theorem Units.isEmbedding_val_mk'

Modified Mathlib/Topology/Algebra/Constructions/DomMulAct.lean

deleted theorem DomMulAct.embedding_mk

deleted theorem DomMulAct.embedding_mk_symm

added theorem DomMulAct.isEmbedding_mk

added theorem DomMulAct.isEmbedding_mk_symm

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

deleted theorem ContinuousMonoidHom.embedding_toContinuousMap

added theorem ContinuousMonoidHom.isEmbedding_toContinuousMap

Modified Mathlib/Topology/Algebra/Group/Basic.lean

deleted theorem Units.embedding_val

added theorem Units.isEmbedding_val

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

deleted theorem Units.embedding_val₀

added theorem Units.isEmbedding_val₀

Modified Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

deleted theorem ContinuousAlternatingMap.embedding_restrictScalars

deleted theorem ContinuousAlternatingMap.embedding_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.isEmbedding_restrictScalars

added theorem ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

deleted theorem ContinuousMultilinearMap.embedding_restrictScalars

deleted theorem ContinuousMultilinearMap.embedding_toUniformOnFun

added theorem ContinuousMultilinearMap.isEmbedding_restrictScalars

added theorem ContinuousMultilinearMap.isEmbedding_toUniformOnFun

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

deleted theorem ContinuousLinearMap.embedding_restrictScalars

added theorem ContinuousLinearMap.isEmbedding_restrictScalars

deleted theorem UniformConvergenceCLM.embedding_coeFn

added theorem UniformConvergenceCLM.isEmbedding_coeFn

Modified Mathlib/Topology/Algebra/Module/WeakBilin.lean

deleted theorem WeakBilin.embedding

added theorem WeakBilin.isEmbedding

Modified Mathlib/Topology/Algebra/Module/WeakDual.lean

Modified Mathlib/Topology/Algebra/ProperAction/Basic.lean

Modified Mathlib/Topology/Algebra/SeparationQuotient/Section.lean

added theorem SeparationQuotient.isEmbedding_outCLM

deleted theorem SeparationQuotient.outCLM_embedding

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean

deleted theorem StarSubalgebra.embedding_inclusion

added theorem StarSubalgebra.isEmbedding_inclusion

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

deleted theorem Profinite.Nobeling.embedding

added theorem Profinite.Nobeling.isClosedEmbedding

Modified Mathlib/Topology/Category/Stonean/Limits.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

deleted theorem TopCat.embedding_prod_map

added theorem TopCat.isEmbedding_prodMap

Modified Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean

deleted theorem TopCat.embedding_of_pullback_embeddings

deleted theorem TopCat.embedding_pullback_to_prod

deleted theorem TopCat.fst_embedding_of_right_embedding

added theorem TopCat.fst_isEmbedding_of_right

added theorem TopCat.isEmbedding_of_pullback

added theorem TopCat.isEmbedding_pullback_to_prod

deleted theorem TopCat.pullback_map_embedding_of_embeddings

added theorem TopCat.pullback_map_isEmbedding

deleted theorem TopCat.snd_embedding_of_left_embedding

added theorem TopCat.snd_isEmbedding_of_left

modified theorem TopCat.snd_iso_of_left_embedding_range_subset

Modified Mathlib/Topology/Category/TopCat/Opens.lean

Modified Mathlib/Topology/CompactOpen.lean

deleted theorem ContinuousMap.embedding_postcomp

added theorem ContinuousMap.isEmbedding_postcomp

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem Embedding.isCompact_iff

added theorem IsEmbedding.isCompact_iff

Modified Mathlib/Topology/Compactness/Lindelof.lean

deleted theorem Embedding.isLindelof_iff

added theorem IsEmbedding.isLindelof_iff

Modified Mathlib/Topology/Compactness/LocallyCompact.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

deleted theorem Embedding.isSigmaCompact_iff

added theorem IsEmbedding.isSigmaCompact_iff

Modified Mathlib/Topology/Connected/Clopen.lean

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

deleted theorem Embedding.isTotallyDisconnected

deleted theorem Embedding.isTotallyDisconnected_image

deleted theorem Embedding.isTotallyDisconnected_range

added theorem IsEmbedding.isTotallyDisconnected

added theorem IsEmbedding.isTotallyDisconnected_image

added theorem IsEmbedding.isTotallyDisconnected_range

Modified Mathlib/Topology/Constructions.lean

deleted theorem Embedding.codRestrict

deleted theorem Embedding.prodMap

added theorem IsEmbedding.prodMap

added theorem IsEmbedding.sigmaMk

added theorem IsEmbedding.subtypeVal

added theorem IsEmbedding.uliftDown

deleted theorem embedding_graph

deleted theorem embedding_inclusion

deleted theorem embedding_inl

deleted theorem embedding_inr

deleted theorem embedding_prod_mk

deleted theorem embedding_sigmaMk

deleted theorem embedding_sigma_map

deleted theorem embedding_subtype_val

deleted theorem embedding_uLift_down

added theorem isEmbedding_graph

added theorem isEmbedding_prodMk

added theorem isEmbedding_sigmaMap

Modified Mathlib/Topology/ContinuousMap/Bounded.lean

deleted theorem BoundedContinuousFunction.embedding_coeFn

added theorem BoundedContinuousFunction.isEmbedding_coeFn

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

deleted theorem ContinuousMapZero.embedding_toContinuousMap

added theorem ContinuousMapZero.isEmbedding_toContinuousMap

Modified Mathlib/Topology/ContinuousMap/Sigma.lean

deleted theorem ContinuousMap.embedding_sigmaMk_comp

added theorem ContinuousMap.isEmbedding_sigmaMk_comp

Modified Mathlib/Topology/ContinuousMap/T0Sierpinski.lean

deleted theorem TopologicalSpace.productOfMemOpens_embedding

added theorem TopologicalSpace.productOfMemOpens_isEmbedding

Modified Mathlib/Topology/ContinuousOn.lean

deleted theorem Embedding.continuousOn_iff

deleted theorem Embedding.map_nhdsWithin_eq

added theorem IsEmbedding.continuousOn_iff

added theorem IsEmbedding.map_nhdsWithin_eq

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/Defs/Induced.lean

deleted structure Embedding

modified structure IsClosedEmbedding

added structure IsEmbedding

modified structure IsOpenEmbedding

Modified Mathlib/Topology/DenseEmbedding.lean

added theorem IsDenseEmbedding.isEmbedding

deleted theorem IsDenseEmbedding.to_embedding

Modified Mathlib/Topology/FiberBundle/Basic.lean

deleted theorem FiberBundle.totalSpaceMk_embedding

added theorem FiberBundle.totalSpaceMk_isEmbedding

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Homeomorph.lean

added theorem Homeomorph.isEmbedding

added theorem IsHomeomorph.isEmbedding

deleted theorem isHomeomorph_iff_embedding_surjective

added theorem isHomeomorph_iff_isEmbedding_surjective

Modified Mathlib/Topology/Instances/ENNReal.lean

deleted theorem ENNReal.embedding_coe

added theorem ENNReal.isEmbedding_coe

Modified Mathlib/Topology/Instances/ENat.lean

deleted theorem ENat.embedding_natCast

added theorem ENat.isEmbedding_natCast

Modified Mathlib/Topology/Instances/EReal.lean

deleted theorem EReal.embedding_coe

deleted theorem EReal.embedding_coe_ennreal

added theorem EReal.isEmbedding_coe

added theorem EReal.isEmbedding_coe_ennreal

Modified Mathlib/Topology/Instances/Rat.lean

deleted theorem Rat.embedding_coe_real

added theorem Rat.isEmbedding_coe_real

Modified Mathlib/Topology/Instances/TrivSqZeroExt.lean

added theorem TrivSqZeroExt.IsEmbedding.inl

added theorem TrivSqZeroExt.IsEmbedding.inr

deleted theorem TrivSqZeroExt.embedding_inl

deleted theorem TrivSqZeroExt.embedding_inr

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/LocalAtTarget.lean

deleted theorem Set.restrictPreimage_embedding

added theorem Set.restrictPreimage_isEmbedding

deleted theorem embedding_iff_embedding_of_iSup_eq_top

added theorem isEmbedding_iff_of_iSup_eq_top

Modified Mathlib/Topology/LocallyClosed.lean

deleted theorem Embedding.isLocallyClosed_iff

added theorem IsEmbedding.isLocallyClosed_iff

Modified Mathlib/Topology/Maps/Basic.lean

deleted theorem Embedding.closure_eq_preimage_closure_image

deleted theorem Embedding.continuous

deleted theorem Embedding.continuous_iff

deleted theorem Embedding.discreteTopology

deleted theorem Embedding.map_nhds_eq

deleted theorem Embedding.map_nhds_of_mem

deleted theorem Embedding.mk'

deleted theorem Embedding.of_comp_iff

deleted theorem Embedding.of_subsingleton

deleted theorem Embedding.tendsto_nhds_iff

deleted theorem Embedding.toIsOpenEmbedding_of_surjective

deleted theorem Function.Injective.embedding_induced

added theorem Function.Injective.isEmbedding_induced

modified theorem IsClosedEmbedding.continuous

added theorem IsClosedEmbedding.inducing

modified theorem IsClosedEmbedding.isClosedMap

added theorem IsClosedEmbedding.isEmbedding

modified theorem IsClosedEmbedding.of_comp_iff

deleted theorem IsClosedEmbedding.of_embedding_closed

added theorem IsClosedEmbedding.of_isEmbedding_isClosedMap

modified theorem IsClosedEmbedding.tendsto_nhds_iff

added theorem IsEmbedding.closure_eq_preimage_closure_image

added theorem IsEmbedding.continuous

added theorem IsEmbedding.continuous_iff

added theorem IsEmbedding.discreteTopology

added theorem IsEmbedding.isOpenEmbedding_of_surjective

added theorem IsEmbedding.map_nhds_eq

added theorem IsEmbedding.map_nhds_of_mem

added theorem IsEmbedding.mk'

added theorem IsEmbedding.of_comp_iff

added theorem IsEmbedding.of_leftInverse

added theorem IsEmbedding.of_subsingleton

added theorem IsEmbedding.tendsto_nhds_iff

added theorem IsOpenEmbedding.inducing

added theorem IsOpenEmbedding.isEmbedding

modified theorem IsOpenEmbedding.isOpenMap

added theorem IsOpenEmbedding.of_isEmbedding_isOpenMap

deleted theorem embedding_id

deleted theorem embedding_of_embedding_compose

deleted theorem isOpenEmbedding_iff_embedding_open

added theorem isOpenEmbedding_iff_isEmbedding_isOpenMap

deleted theorem isOpenEmbedding_of_embedding_open

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

Modified Mathlib/Topology/MetricSpace/Closeds.lean

Modified Mathlib/Topology/MetricSpace/Dilation.lean

added theorem Dilation.isEmbedding

Modified Mathlib/Topology/MetricSpace/Isometry.lean

deleted theorem Embedding.to_isometry

added theorem IsEmbedding.to_isometry

added theorem Isometry.isEmbedding

Modified Mathlib/Topology/MetricSpace/Polish.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

Modified Mathlib/Topology/Metrizable/Basic.lean

deleted theorem Embedding.metrizableSpace

added theorem IsEmbedding.metrizableSpace

Modified Mathlib/Topology/Metrizable/Urysohn.lean

modified theorem TopologicalSpace.exists_embedding_l_infty

Modified Mathlib/Topology/NoetherianSpace.lean

Modified Mathlib/Topology/Order/Basic.lean

deleted theorem StrictMono.embedding_of_ordConnected

added theorem StrictMono.isEmbedding_of_ordConnected

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Topology/QuasiSeparated.lean

deleted theorem IsQuasiSeparated.image_of_embedding

added theorem IsQuasiSeparated.image_of_isEmbedding

Modified Mathlib/Topology/SeparatedMap.lean

deleted theorem embedding_toPullbackDiag

Modified Mathlib/Topology/Separation/Basic.lean

deleted theorem Embedding.completelyNormalSpace

deleted theorem Embedding.t25Space

deleted theorem Embedding.t2Space

deleted theorem Embedding.t5Space

added theorem IsEmbedding.completelyNormalSpace

added theorem IsEmbedding.t25Space

added theorem IsEmbedding.t2Space

added theorem IsEmbedding.t5Space

deleted theorem embedding_iff_inducing

added theorem isEmbedding_iff_inducing

Modified Mathlib/Topology/Sets/Opens.lean

Modified Mathlib/Topology/Sober.lean

Modified Mathlib/Topology/Support.lean

Modified Mathlib/Topology/TietzeExtension.lean

Modified Mathlib/Topology/UniformSpace/CompleteSeparated.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean

deleted def Embedding.comapUniformSpace

added def IsEmbedding.comapUniformSpace

Modified scripts/no_lints_prime_decls.txt