Commit 2024-11-05 13:38 808d4291

View on Github →

chore(Topology): miscellaneous renames (#18398) A bunch of lemma name improvements that were missed in the prerequisites to #15993

Estimated changes

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

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

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

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

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/CategoryTheory/Galois/Topology.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

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

Modified Mathlib/Topology/Bases.lean

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

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

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

added theorem TopCat.isOpenEmbedding_of_pullback

deleted theorem TopCat.isOpenEmbedding_of_pullback_open_embeddings

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

Modified Mathlib/Topology/Clopen.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

Modified Mathlib/Topology/Connected/PathConnected.lean

Modified Mathlib/Topology/Constructions.lean

added theorem IsClosedEmbedding.inl

added theorem IsClosedEmbedding.inr

added theorem IsClosedEmbedding.sigmaMk

added theorem IsClosedEmbedding.uliftDown

added theorem IsOpenEmbedding.sigmaMk

deleted theorem ULift.isClosedEmbedding_down

deleted theorem isClosedEmbedding_inl

deleted theorem isClosedEmbedding_inr

deleted theorem isClosedEmbedding_sigmaMk

deleted theorem isOpenEmbedding_inl

deleted theorem isOpenEmbedding_inr

added theorem isOpenEmbedding_sigmaMap

deleted theorem isOpenEmbedding_sigmaMk

deleted theorem isOpenEmbedding_sigma_map

modified theorem isOpen_range_inl

modified theorem isOpen_range_inr

Modified Mathlib/Topology/DenseEmbedding.lean

added theorem IsDenseEmbedding.isDenseInducing

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Instances/CantorSet.lean

Modified Mathlib/Topology/Instances/RatLemmas.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/JacobsonSpace.lean

Modified Mathlib/Topology/LocalAtTarget.lean

Modified Mathlib/Topology/Maps/Basic.lean

deleted theorem IsClosedEmbedding.of_continuous_injective_isClosedMap

deleted theorem IsInducing.IsClosedEmbedding.closed_iff_image_closed

deleted theorem IsInducing.IsClosedEmbedding.closed_iff_preimage_closed

added theorem IsInducing.IsClosedEmbedding.isClosed_iff_image_isClosed

added theorem IsInducing.IsClosedEmbedding.isClosed_iff_preimage_isClosed

added theorem IsInducing.IsClosedEmbedding.of_continuous_injective_isClosedMap

added theorem IsInducing.IsOpenEmbedding.isOpen_iff_image_isOpen

added theorem IsInducing.IsOpenEmbedding.isOpen_iff_preimage_isOpen

modified theorem IsInducing.IsOpenEmbedding.of_comp

added theorem IsInducing.IsOpenEmbedding.of_continuous_injective_isOpenMap

deleted theorem IsInducing.IsOpenEmbedding.open_iff_image_open

deleted theorem IsInducing.IsOpenEmbedding.open_iff_preimage_open

deleted theorem IsInducing.isOpenEmbedding_id

added theorem IsInducing.isOpenEmbedding_iff_continuous_injective_isOpenMap

deleted theorem IsInducing.isOpenEmbedding_iff_continuous_injective_open

deleted theorem IsInducing.isOpenEmbedding_of_continuous_injective_open

deleted theorem isClosedEmbedding_id

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Topology/SeparatedMap.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/UniformSpace/CompleteSeparated.lean

added theorem IsUniformEmbedding.isClosedEmbedding

deleted theorem IsUniformEmbedding.toIsClosedEmbedding

Modified Mathlib/Topology/UniformSpace/Completion.lean