From a9ecf75bdf24171c43fcf1e49db31c4d3a2e9fdc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 28 Oct 2024 08:46:37 +0000 Subject: [PATCH] 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 1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Embedding` is) 2. namespacing it inside `Topology` --- .../Morphisms/ClosedImmersion.lean | 2 +- .../Morphisms/Immersion.lean | 6 +- .../AlgebraicGeometry/Morphisms/IsIso.lean | 2 +- .../Morphisms/Preimmersion.lean | 23 ++- .../Morphisms/QuasiSeparated.lean | 4 +- .../Morphisms/UnderlyingMap.lean | 14 +- .../PrimeSpectrum/Basic.lean | 17 +- .../PrimeSpectrum/TensorProduct.lean | 16 +- Mathlib/AlgebraicGeometry/Properties.lean | 8 +- Mathlib/AlgebraicGeometry/ResidueField.lean | 3 +- .../Restrict.lean | 12 +- .../Analysis/Calculus/FDeriv/Analytic.lean | 2 +- .../Complex/UpperHalfPlane/Topology.lean | 9 +- Mathlib/Analysis/LocallyConvex/Bounded.lean | 2 +- Mathlib/Analysis/Normed/Module/WeakDual.lean | 2 +- .../Normed/Operator/LinearIsometry.lean | 5 +- .../Normed/Operator/WeakOperatorTopology.lean | 11 +- Mathlib/Analysis/Normed/Ring/Units.lean | 2 +- .../NormedSpace/Multilinear/Basic.lean | 2 +- .../NormedSpace/OperatorNorm/NormedSpace.lean | 5 +- .../SpecialFunctions/Log/ENNRealLogExp.lean | 6 +- Mathlib/CategoryTheory/Extensive.lean | 8 +- Mathlib/CategoryTheory/Galois/Topology.lean | 2 +- .../Manifold/SmoothManifoldWithCorners.lean | 6 +- .../Geometry/RingedSpace/OpenImmersion.lean | 4 +- .../Constructions/BorelSpace/Basic.lean | 15 +- Mathlib/MeasureTheory/Function/LpSpace.lean | 2 +- .../Function/StronglyMeasurable/Basic.lean | 9 +- .../Function/StronglyMeasurable/Lemmas.lean | 2 +- .../Integral/IntegralEqImproper.lean | 8 +- Mathlib/MeasureTheory/Measure/DiracProba.lean | 11 +- .../MeasureTheory/Measure/FiniteMeasure.lean | 10 +- .../Measure/LevyProkhorovMetric.lean | 2 +- .../Measure/ProbabilityMeasure.lean | 12 +- Mathlib/Topology/Algebra/Constructions.lean | 34 ++-- .../Algebra/Constructions/DomMulAct.lean | 43 ++-- .../Topology/Algebra/ContinuousMonoidHom.lean | 11 +- Mathlib/Topology/Algebra/Group/Basic.lean | 11 +- Mathlib/Topology/Algebra/GroupWithZero.lean | 7 +- .../Algebra/Module/Alternating/Topology.lean | 30 +-- .../Algebra/Module/FiniteDimension.lean | 2 +- .../Algebra/Module/Multilinear/Topology.lean | 22 +- .../Algebra/Module/StrongTopology.lean | 44 ++-- .../Topology/Algebra/Module/WeakBilin.lean | 11 +- Mathlib/Topology/Algebra/Module/WeakDual.lean | 4 +- .../Topology/Algebra/ProperAction/Basic.lean | 2 +- .../Algebra/SeparationQuotient/Section.lean | 9 +- Mathlib/Topology/Algebra/StarSubalgebra.lean | 14 +- Mathlib/Topology/Bases.lean | 15 +- .../Topology/Category/Profinite/Nobeling.lean | 9 +- Mathlib/Topology/Category/Stonean/Limits.lean | 2 +- .../Category/TopCat/Limits/Products.lean | 13 +- .../Category/TopCat/Limits/Pullbacks.lean | 75 ++++--- Mathlib/Topology/Category/TopCat/Opens.lean | 4 +- Mathlib/Topology/CompactOpen.lean | 9 +- .../Topology/Compactification/OnePoint.lean | 2 +- Mathlib/Topology/Compactness/Compact.lean | 7 +- Mathlib/Topology/Compactness/Lindelof.lean | 7 +- .../Topology/Compactness/LocallyCompact.lean | 2 +- .../Topology/Compactness/SigmaCompact.lean | 9 +- Mathlib/Topology/Connected/Clopen.lean | 2 +- .../Connected/TotallyDisconnected.lean | 23 ++- Mathlib/Topology/Constructions.lean | 101 ++++++---- Mathlib/Topology/ContinuousMap/Bounded.lean | 7 +- .../ContinuousMap/ContinuousMapZero.lean | 25 ++- Mathlib/Topology/ContinuousMap/Sigma.lean | 13 +- .../Topology/ContinuousMap/T0Sierpinski.lean | 7 +- Mathlib/Topology/ContinuousOn.lean | 14 +- Mathlib/Topology/Covering.lean | 2 +- Mathlib/Topology/Defs/Induced.lean | 10 +- Mathlib/Topology/DenseEmbedding.lean | 11 +- Mathlib/Topology/FiberBundle/Basic.lean | 9 +- Mathlib/Topology/Gluing.lean | 2 +- Mathlib/Topology/Homeomorph.lean | 61 +++--- Mathlib/Topology/Instances/ENNReal.lean | 19 +- Mathlib/Topology/Instances/ENat.lean | 9 +- Mathlib/Topology/Instances/EReal.lean | 30 +-- Mathlib/Topology/Instances/Rat.lean | 7 +- Mathlib/Topology/Instances/TrivSqZeroExt.lean | 14 +- Mathlib/Topology/IsLocalHomeomorph.lean | 12 +- Mathlib/Topology/LocalAtTarget.lean | 27 ++- Mathlib/Topology/LocallyClosed.lean | 7 +- Mathlib/Topology/Maps/Basic.lean | 190 +++++++++++------- .../Topology/MetricSpace/Antilipschitz.lean | 2 +- Mathlib/Topology/MetricSpace/Basic.lean | 7 +- Mathlib/Topology/MetricSpace/Closeds.lean | 2 +- Mathlib/Topology/MetricSpace/Dilation.lean | 9 +- Mathlib/Topology/MetricSpace/Isometry.lean | 13 +- Mathlib/Topology/MetricSpace/Polish.lean | 9 +- .../Topology/MetricSpace/Pseudo/Basic.lean | 7 +- Mathlib/Topology/Metrizable/Basic.lean | 9 +- Mathlib/Topology/Metrizable/Urysohn.lean | 6 +- Mathlib/Topology/NoetherianSpace.lean | 2 +- Mathlib/Topology/Order/Basic.lean | 7 +- Mathlib/Topology/PartialHomeomorph.lean | 2 +- Mathlib/Topology/QuasiSeparated.lean | 11 +- Mathlib/Topology/SeparatedMap.lean | 15 +- Mathlib/Topology/Separation/Basic.lean | 102 ++++++---- Mathlib/Topology/Sets/Opens.lean | 10 +- Mathlib/Topology/Sober.lean | 2 +- Mathlib/Topology/Support.lean | 2 +- Mathlib/Topology/TietzeExtension.lean | 2 +- .../UniformSpace/CompleteSeparated.lean | 2 +- .../UniformSpace/UniformEmbedding.lean | 25 ++- scripts/no_lints_prime_decls.txt | 2 +- 105 files changed, 910 insertions(+), 582 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean index c95fb9628853a..52833da5d26b8 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean @@ -63,7 +63,7 @@ lemma eq_inf : @IsClosedImmersion = (topologically IsClosedEmbedding) ⊓ lemma iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} : IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range f.base) := by rw [and_comm, isClosedImmersion_iff, isPreimmersion_iff, ← and_assoc, isClosedEmbedding_iff, - @and_comm (Embedding _)] + @and_comm (IsEmbedding _)] lemma of_isPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] (hf : IsClosed (Set.range f.base)) : IsClosedImmersion f := diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean index 3dde16b8057b3..9097372c8b837 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean @@ -76,7 +76,7 @@ instance [IsImmersion f] : IsClosedImmersion f.liftCoborder := by have : IsPreimmersion f.liftCoborder := .of_comp f.liftCoborder f.coborderRange.ι refine .of_isPreimmersion _ ?_ convert isClosed_preimage_val_coborder - apply Set.image_injective.mpr f.coborderRange.ι.embedding.inj + apply Set.image_injective.mpr f.coborderRange.ι.isEmbedding.inj rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.comp_base, f.liftCoborder_ι] exact (Set.image_preimage_eq_of_subset (by simpa using subset_coborder)).symm @@ -121,7 +121,7 @@ instance : MorphismProperty.IsMultiplicative @IsImmersion where comp_mem {X Y Z} f g hf hg := by refine { __ := inferInstanceAs (IsPreimmersion (f ≫ g)), isLocallyClosed_range := ?_ } simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] - exact f.isLocallyClosed_range.image g.embedding.toInducing g.isLocallyClosed_range + exact f.isLocallyClosed_range.image g.isEmbedding.toInducing g.isLocallyClosed_range instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion f] [IsImmersion g] : IsImmersion (f ≫ g) := @@ -141,7 +141,7 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion g] [IsImmersion (f ≫ g)] : IsImmersion f where __ := IsPreimmersion.of_comp f g isLocallyClosed_range := by - rw [← Set.preimage_image_eq (Set.range _) g.embedding.inj] + rw [← Set.preimage_image_eq (Set.range _) g.isEmbedding.inj] have := (f ≫ g).isLocallyClosed_range.preimage g.base.2 simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] using this diff --git a/Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean b/Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean index 41f31c85bebb9..6f9ee9c19b6e8 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean @@ -30,7 +30,7 @@ lemma isomorphisms_eq_stalkwise : congr 1 ext X Y f exact ⟨fun H ↦ inferInstanceAs (IsIso (TopCat.isoOfHomeo - (H.1.1.toHomeomeomorph_of_surjective H.2)).hom), fun (_ : IsIso f.base) ↦ + (H.1.1.toHomeomorph_of_surjective H.2)).hom), fun (_ : IsIso f.base) ↦ let e := (TopCat.homeoOfIso <| asIso f.base); ⟨e.isOpenEmbedding, e.surjective⟩⟩ instance : IsLocalAtTarget (isomorphisms Scheme) := diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean index f504cc230196f..1cf0aeb9c2a52 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean @@ -34,18 +34,21 @@ namespace AlgebraicGeometry topological spaces is an embedding and the induced morphisms of stalks are all surjective. -/ @[mk_iff] class IsPreimmersion {X Y : Scheme} (f : X ⟶ Y) : Prop where - base_embedding : Embedding f.base + base_embedding : IsEmbedding f.base surj_on_stalks : ∀ x, Function.Surjective (f.stalkMap x) -lemma Scheme.Hom.embedding {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] : Embedding f.base := +lemma Scheme.Hom.isEmbedding {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] : IsEmbedding f.base := IsPreimmersion.base_embedding +@[deprecated (since := "2024-10-26")] +alias Scheme.Hom.embedding := Scheme.Hom.isEmbedding + lemma Scheme.Hom.stalkMap_surjective {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] (x) : Function.Surjective (f.stalkMap x) := IsPreimmersion.surj_on_stalks x lemma isPreimmersion_eq_inf : - @IsPreimmersion = topologically Embedding ⊓ stalkwise (Function.Surjective ·) := by + @IsPreimmersion = topologically IsEmbedding ⊓ stalkwise (Function.Surjective ·) := by ext rw [isPreimmersion_iff] rfl @@ -61,7 +64,7 @@ instance : IsLocalAtTarget @IsPreimmersion := isPreimmersion_eq_inf ▸ inferInstance instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsPreimmersion f where - base_embedding := f.isOpenEmbedding.toEmbedding + base_embedding := f.isOpenEmbedding.isEmbedding surj_on_stalks _ := (ConcreteCategory.bijective_of_isIso _).2 instance : MorphismProperty.IsMultiplicative @IsPreimmersion where @@ -79,14 +82,14 @@ instance (priority := 900) {X Y} (f : X ⟶ Y) [IsPreimmersion f] : Mono f := by refine (Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_ apply SheafedSpace.mono_of_base_injective_of_stalk_epi - · exact f.embedding.inj + · exact f.isEmbedding.inj · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x) theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] [IsPreimmersion (f ≫ g)] : IsPreimmersion f where base_embedding := by - have h := (f ≫ g).embedding - rwa [← g.embedding.of_comp_iff] + have h := (f ≫ g).isEmbedding + rwa [← g.isEmbedding.of_comp_iff] surj_on_stalks x := by have h := (f ≫ g).stalkMap_surjective x rw [Scheme.stalkMap_comp] at h @@ -97,7 +100,7 @@ theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩ lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) : - IsPreimmersion (Spec.map f) ↔ Embedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by + IsPreimmersion (Spec.map f) ↔ IsEmbedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by rw [← RingHom.toMorphismProperty_respectsIso_iff] exact RingHom.surjective_respectsIso @@ -111,7 +114,7 @@ lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) : exact h₂ x.asIdeal x.isPrime lemma mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S} - (h₁ : Embedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) : + (h₁ : IsEmbedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) : IsPreimmersion (Spec.map f) := (Spec_map_iff f).mpr ⟨h₁, h₂⟩ @@ -119,7 +122,7 @@ lemma of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing [Algebra R S] [IsLocalization M S] : IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) := IsPreimmersion.mk_Spec_map - (PrimeSpectrum.localization_comap_embedding (R := R) S M) + (PrimeSpectrum.localization_comap_isEmbedding (R := R) S M) (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S) end IsPreimmersion diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean index fffb3c4c1f9e1..76731289cf0e1 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean @@ -85,7 +85,7 @@ theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAf let g : pullback U.1.ι V.1.ι ⟶ X := pullback.fst _ _ ≫ U.1.ι -- Porting note: `inferInstance` does not work here have : IsOpenImmersion g := PresheafedSpace.IsOpenImmersion.comp _ _ - have e := Homeomorph.ofEmbedding _ this.base_open.toEmbedding + have e := Homeomorph.ofIsEmbedding _ this.base_open.isEmbedding rw [IsOpenImmersion.range_pullback_to_base_of_left] at e erw [Subtype.range_coe, Subtype.range_coe] at e rw [isCompact_iff_compactSpace] @@ -94,7 +94,7 @@ theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAf let g : pullback f₁ f₂ ⟶ X := pullback.fst _ _ ≫ f₁ -- Porting note: `inferInstance` does not work here have : IsOpenImmersion g := PresheafedSpace.IsOpenImmersion.comp _ _ - have e := Homeomorph.ofEmbedding _ this.base_open.toEmbedding + have e := Homeomorph.ofIsEmbedding _ this.base_open.isEmbedding rw [IsOpenImmersion.range_pullback_to_base_of_left] at e simp_rw [isCompact_iff_compactSpace] at H exact diff --git a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean index aa7ef919ab2b8..eb093308cb69e 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean @@ -17,7 +17,7 @@ of the underlying map of topological spaces, including - `Surjective` - `IsOpenMap` - `IsClosedMap` -- `Embedding` +- `IsEmbedding` - `IsOpenEmbedding` - `IsClosedEmbedding` - `DenseRange` (`IsDominant`) @@ -105,15 +105,15 @@ instance isClosedMap_isLocalAtTarget : IsLocalAtTarget (topologically IsClosedMa end IsClosedMap -section Embedding +section IsEmbedding -instance : (topologically Embedding).RespectsIso := - topologically_respectsIso _ (fun e ↦ e.embedding) (fun _ _ hf hg ↦ hg.comp hf) +instance : (topologically IsEmbedding).RespectsIso := + topologically_respectsIso _ (fun e ↦ e.isEmbedding) (fun _ _ hf hg ↦ hg.comp hf) -instance embedding_isLocalAtTarget : IsLocalAtTarget (topologically Embedding) := - topologically_isLocalAtTarget' _ fun _ _ _ ↦ embedding_iff_embedding_of_iSup_eq_top +instance isEmbedding_isLocalAtTarget : IsLocalAtTarget (topologically IsEmbedding) := + topologically_isLocalAtTarget' _ fun _ _ _ ↦ isEmbedding_iff_of_iSup_eq_top -end Embedding +end IsEmbedding section IsOpenEmbedding diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean index 2ad92e90d3efa..85f9834657ba0 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean @@ -260,10 +260,13 @@ theorem localization_comap_injective [Algebra R S] (M : Submonoid R) [IsLocaliza Function.Injective (comap (algebraMap R S)) := fun _ _ h => localization_specComap_injective S M h -theorem localization_comap_embedding [Algebra R S] (M : Submonoid R) [IsLocalization M S] : - Embedding (comap (algebraMap R S)) := +theorem localization_comap_isEmbedding [Algebra R S] (M : Submonoid R) [IsLocalization M S] : + IsEmbedding (comap (algebraMap R S)) := ⟨localization_comap_inducing S M, localization_comap_injective S M⟩ +@[deprecated (since := "2024-10-26")] +alias localization_comap_embedding := localization_comap_isEmbedding + theorem localization_comap_range [Algebra R S] (M : Submonoid R) [IsLocalization M S] : Set.range (comap (algebraMap R S)) = { p | Disjoint (M : Set R) p.asIdeal } := localization_specComap_range .. @@ -462,11 +465,11 @@ theorem localization_away_comap_range (S : Type v) [CommSemiring S] [Algebra R S exact h₁ (x.2.mem_of_pow_mem _ h₃) theorem localization_away_isOpenEmbedding (S : Type v) [CommSemiring S] [Algebra R S] (r : R) - [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S)) := - { toEmbedding := localization_comap_embedding S (Submonoid.powers r) - isOpen_range := by - rw [localization_away_comap_range S r] - exact isOpen_basicOpen } + [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S)) where + toIsEmbedding := localization_comap_isEmbedding S (Submonoid.powers r) + isOpen_range := by + rw [localization_away_comap_range S r] + exact isOpen_basicOpen @[deprecated (since := "2024-10-18")] alias localization_away_openEmbedding := localization_away_isOpenEmbedding diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean index c13845fdd8fb9..457e6d0a254f5 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean @@ -11,7 +11,7 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic # Lemmas regarding the prime spectrum of tensor products ## Main result -- `PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks`: +- `PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks`: If `R →+* T` is surjective on stalks (see Mathlib/RingTheory/SurjectiveOnStalks.lean), then `Spec(S ⊗[R] T) → Spec S × Spec T` is a topological embedding (where `Spec S × Spec T` is the cartesian product with the product topology). @@ -34,7 +34,7 @@ lemma PrimeSpectrum.continuous_tensorProductTo : Continuous (tensorProductTo R S variable (hRT : (algebraMap R T).SurjectiveOnStalks) include hRT -lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux +lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux (p₁ p₂ : PrimeSpectrum (S ⊗[R] T)) (h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂) : p₁ ≤ p₂ := by @@ -55,11 +55,11 @@ lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux rwa [show p₁.asIdeal.comap (algebraMap S (S ⊗[R] T)) = p₂.asIdeal.comap _ from congr($h.1.1)] exact p₁.asIdeal.primeCompl.mul_mem h₄ h₃ h₁ -lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks : - Embedding (tensorProductTo R S T) := by +lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks : + IsEmbedding (tensorProductTo R S T) := by refine ⟨?_, fun p₁ p₂ e ↦ - (embedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm - (embedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩ + (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₁ p₂ e).antisymm + (isEmbedding_tensorProductTo_of_surjectiveOnStalks_aux R S T hRT p₂ p₁ e.symm)⟩ let g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom refine ⟨(continuous_tensorProductTo ..).le_induced.antisymm (isBasis_basic_opens.le_iff.mpr ?_)⟩ rintro _ ⟨f, rfl⟩ @@ -77,3 +77,7 @@ lemma PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks : rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e] exact J.asIdeal.primeCompl.mul_mem ht hJ rwa [J.isPrime.mul_mem_iff_mem_or_mem.not, not_or] at this + +@[deprecated (since := "2024-10-26")] +alias PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks := + PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean index 84f113a767c02..4fb6a8f489f90 100644 --- a/Mathlib/AlgebraicGeometry/Properties.lean +++ b/Mathlib/AlgebraicGeometry/Properties.lean @@ -31,16 +31,16 @@ variable (X : Scheme) instance : T0Space X := T0Space.of_open_cover fun x => ⟨_, X.affineCover.covers x, - (X.affineCover.map x).opensRange.2, Embedding.t0Space (Y := PrimeSpectrum _) - (isAffineOpen_opensRange (X.affineCover.map x)).isoSpec.schemeIsoToHomeo.embedding⟩ + (X.affineCover.map x).opensRange.2, IsEmbedding.t0Space (Y := PrimeSpectrum _) + (isAffineOpen_opensRange (X.affineCover.map x)).isoSpec.schemeIsoToHomeo.isEmbedding⟩ instance : QuasiSober X := by apply (config := { allowSynthFailures := true }) quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.map x).base) · rintro ⟨_, i, rfl⟩; exact (X.affineCover.IsOpen i).base_open.isOpen_range · rintro ⟨_, i, rfl⟩ - exact @IsOpenEmbedding.quasiSober _ _ _ _ _ (Homeomorph.ofEmbedding _ - (X.affineCover.IsOpen i).base_open.toEmbedding).symm.isOpenEmbedding PrimeSpectrum.quasiSober + exact @IsOpenEmbedding.quasiSober _ _ _ _ _ (Homeomorph.ofIsEmbedding _ + (X.affineCover.IsOpen i).base_open.isEmbedding).symm.isOpenEmbedding PrimeSpectrum.quasiSober · rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall] intro x; exact ⟨_, ⟨_, rfl⟩, X.affineCover.covers x⟩ diff --git a/Mathlib/AlgebraicGeometry/ResidueField.lean b/Mathlib/AlgebraicGeometry/ResidueField.lean index fd0360bc3bc0c..4b64608218fcd 100644 --- a/Mathlib/AlgebraicGeometry/ResidueField.lean +++ b/Mathlib/AlgebraicGeometry/ResidueField.lean @@ -52,7 +52,8 @@ def residue (X : Scheme.{u}) (x) : X.presheaf.stalk x ⟶ X.residueField x := `Spec.map (X.residue x)` is a closed immersion. -/ instance {X : Scheme.{u}} (x) : IsPreimmersion (Spec.map (X.residue x)) := IsPreimmersion.mk_Spec_map - (PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective).embedding + (PrimeSpectrum.isClosedEmbedding_comap_of_surjective _ _ + Ideal.Quotient.mk_surjective).isEmbedding (RingHom.surjectiveOnStalks_of_surjective (Ideal.Quotient.mk_surjective)) @[simp] diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean index ac2ac678b6bee..195b717b64044 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean @@ -160,9 +160,9 @@ lemma cfc_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) simp [Function.comp, Subtype.val_injective.extend_apply] · have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (spectrum S a) := by refine fun hg' ↦ hg ?_ - rw [halg.embedding.continuousOn_iff] - simpa [halg.embedding.continuousOn_iff, Function.comp_def, h.left_inv _] using - hg'.comp halg.embedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S) + rw [halg.isEmbedding.continuousOn_iff] + simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using + hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ spectrum.algebraMap_mem S) rw [cfc_apply_of_not_continuousOn a hg, cfc_apply_of_not_continuousOn a this] end SpectrumRestricts @@ -312,9 +312,9 @@ lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R obtain (hg | hg) := hg · have : ¬ ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (σₙ S a) := by refine fun hg' ↦ hg ?_ - rw [halg.embedding.continuousOn_iff] - simpa [halg.embedding.continuousOn_iff, Function.comp_def, h.left_inv _] using - hg'.comp halg.embedding.continuous.continuousOn + rw [halg.isEmbedding.continuousOn_iff] + simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using + hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ quasispectrum.algebraMap_mem S) rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn a this] · rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])] diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean index 4947d3460259a..4a3807f990caf 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean @@ -333,7 +333,7 @@ theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt let F' := UniformSpace.Completion F let a : F →L[𝕜] F' := UniformSpace.Completion.toComplL let b : (E →L[𝕜] F) →ₗᵢ[𝕜] (E →L[𝕜] F') := UniformSpace.Completion.toComplₗᵢ.postcomp - rw [← b.embedding.hasSum_iff] + rw [← b.isEmbedding.hasSum_iff] have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r := a.comp_hasFPowerSeriesWithinOnBall h have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_eq_coe_nnnorm] using hy) diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean index 8aec80774131b..c2fe2e71fcdfa 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean @@ -36,11 +36,14 @@ theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℍ → ℂ) := @[deprecated (since := "2024-10-18")] alias openEmbedding_coe := isOpenEmbedding_coe -theorem embedding_coe : Embedding ((↑) : ℍ → ℂ) := - embedding_subtype_val +theorem isEmbedding_coe : IsEmbedding ((↑) : ℍ → ℂ) := + IsEmbedding.subtypeVal + +@[deprecated (since := "2024-10-26")] +alias embedding_coe := isEmbedding_coe theorem continuous_coe : Continuous ((↑) : ℍ → ℂ) := - embedding_coe.continuous + isEmbedding_coe.continuous theorem continuous_re : Continuous re := Complex.continuous_re.comp continuous_coe diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean index 1fbe648d3d553..8f324581a6270 100644 --- a/Mathlib/Analysis/LocallyConvex/Bounded.lean +++ b/Mathlib/Analysis/LocallyConvex/Bounded.lean @@ -199,7 +199,7 @@ theorem IsVonNBounded.image {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) : IsVonNBounded 𝕜₂ (f '' s) := by have σ_iso : Isometry σ := AddMonoidHomClass.isometry_of_norm σ fun x => RingHomIsometric.is_iso have : map σ (𝓝 0) = 𝓝 0 := by - rw [σ_iso.embedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero] + rw [σ_iso.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero] have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f) simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢ simpa only [comp_def, image_smul_setₛₗ _ _ σ f] using hf₀.image_smallSets.comp hs diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean index 9eceea12586f7..a5798eaf704c2 100644 --- a/Mathlib/Analysis/Normed/Module/WeakDual.lean +++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean @@ -198,7 +198,7 @@ theorem isClosed_image_coe_of_bounded_of_closed {s : Set (WeakDual 𝕜 E)} theorem isCompact_of_bounded_of_closed [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)} (hb : IsBounded (Dual.toWeakDual ⁻¹' s)) (hc : IsClosed s) : IsCompact s := - (Embedding.isCompact_iff DFunLike.coe_injective.embedding_induced).mpr <| + DFunLike.coe_injective.isEmbedding_induced.isCompact_iff.mpr <| ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image hb <| isClosed_image_coe_of_bounded_of_closed hb hc diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean index efae1765145f5..41a382610b103 100644 --- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean +++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean @@ -200,7 +200,10 @@ theorem nnnorm_map (x : E) : ‖f x‖₊ = ‖x‖₊ := protected theorem isometry : Isometry f := AddMonoidHomClass.isometry_of_norm f.toLinearMap (norm_map _) -protected lemma embedding (f : F →ₛₗᵢ[σ₁₂] E₂) : Embedding f := f.isometry.embedding +lemma isEmbedding (f : F →ₛₗᵢ[σ₁₂] E₂) : IsEmbedding f := f.isometry.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding -- Should be `@[simp]` but it doesn't fire due to `lean4#3107`. theorem isComplete_image_iff [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} : diff --git a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean index 202618cf94cd6..52bae3c5d3cee 100644 --- a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean +++ b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean @@ -172,11 +172,14 @@ lemma continuous_of_dual_apply_continuous {α : Type*} [TopologicalSpace α] {g (h : ∀ x (y : F⋆), Continuous fun a => y (g a x)) : Continuous g := continuous_induced_rng.2 (continuous_pi_iff.mpr fun p => h p.1 p.2) -lemma embedding_inducingFn : Embedding (inducingFn 𝕜 E F) := by - refine Function.Injective.embedding_induced fun A B hAB => ?_ +lemma isEmbedding_inducingFn : IsEmbedding (inducingFn 𝕜 E F) := by + refine Function.Injective.isEmbedding_induced fun A B hAB => ?_ rw [ContinuousLinearMapWOT.ext_dual_iff] simpa [funext_iff] using hAB +@[deprecated (since := "2024-10-26")] +alias embedding_inducingFn := isEmbedding_inducingFn + open Filter in /-- The defining property of the weak operator topology: a function `f` tends to `A : E →WOT[𝕜] F` along filter `l` iff `y (f a x)` tends to `y (A x)` along the same filter. -/ @@ -186,14 +189,14 @@ lemma tendsto_iff_forall_dual_apply_tendsto {α : Type*} {l : Filter α} {f : α have hmain : (∀ x (y : F⋆), Tendsto (fun a => y (f a x)) l (𝓝 (y (A x)))) ↔ ∀ (p : E × F⋆), Tendsto (fun a => p.2 (f a p.1)) l (𝓝 (p.2 (A p.1))) := ⟨fun h p => h p.1 p.2, fun h x y => h ⟨x, y⟩⟩ - rw [hmain, ← tendsto_pi_nhds, Embedding.tendsto_nhds_iff embedding_inducingFn] + rw [hmain, ← tendsto_pi_nhds, isEmbedding_inducingFn.tendsto_nhds_iff] rfl lemma le_nhds_iff_forall_dual_apply_le_nhds {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} : l ≤ 𝓝 A ↔ ∀ x (y : F⋆), l.map (fun T => y (T x)) ≤ 𝓝 (y (A x)) := tendsto_iff_forall_dual_apply_tendsto (f := id) -instance instT3Space : T3Space (E →WOT[𝕜] F) := embedding_inducingFn.t3Space +instance instT3Space : T3Space (E →WOT[𝕜] F) := isEmbedding_inducingFn.t3Space instance instContinuousAdd : ContinuousAdd (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F) instance instContinuousNeg : ContinuousNeg (E →WOT[𝕜] F) := .induced (inducingFn 𝕜 E F) diff --git a/Mathlib/Analysis/Normed/Ring/Units.lean b/Mathlib/Analysis/Normed/Ring/Units.lean index eed32209f935a..44332541ab81f 100644 --- a/Mathlib/Analysis/Normed/Ring/Units.lean +++ b/Mathlib/Analysis/Normed/Ring/Units.lean @@ -201,7 +201,7 @@ open MulOpposite Filter NormedRing /-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the induced topology from the embedding in `R × R`) to `R` is an open embedding. -/ theorem isOpenEmbedding_val : IsOpenEmbedding (val : Rˣ → R) where - toEmbedding := embedding_val_mk' + toIsEmbedding := isEmbedding_val_mk' (fun _ ⟨u, hu⟩ ↦ hu ▸ (inverse_continuousAt u).continuousWithinAt) Ring.inverse_unit isOpen_range := Units.isOpen diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index 02f606b3771ea..2b7591e8a0600 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean @@ -87,7 +87,7 @@ instance ContinuousMultilinearMap.instContinuousEval : let _ := TopologicalAddGroup.toUniformSpace F have := comm_topologicalAddGroup_is_uniform (G := F) refine (UniformOnFun.continuousOn_eval₂ fun m ↦ ?_).comp_continuous - (embedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt + (isEmbedding_toUniformOnFun.continuous.prodMap continuous_id) fun (f, x) ↦ f.cont.continuousAt exact ⟨ball m 1, NormedSpace.isVonNBounded_of_isBounded _ isBounded_ball, ball_mem_nhds _ one_pos⟩ diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean index 27e0b92487849..082320dd797e2 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean @@ -139,10 +139,13 @@ variable (f) /-- If a continuous linear map is a topology embedding, then it is expands the distances by a positive factor. -/ -theorem antilipschitz_of_embedding (f : E →L[𝕜] Fₗ) (hf : Embedding f) : +theorem antilipschitz_of_isEmbedding (f : E →L[𝕜] Fₗ) (hf : IsEmbedding f) : ∃ K, AntilipschitzWith K f := f.toLinearMap.antilipschitz_of_comap_nhds_le <| map_zero f ▸ (hf.nhds_eq_comap 0).ge +@[deprecated (since := "2024-10-26")] +alias antilipschitz_of_embedding := antilipschitz_of_isEmbedding + end OpNorm end ContinuousLinearMap diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean index e257ffe48d381..187db68d382a6 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean @@ -12,7 +12,7 @@ import Mathlib.Topology.MetricSpace.Polish # Properties of the extended logarithm and exponential We prove that `log` and `exp` define order isomorphisms between `ℝ≥0∞` and `EReal`. -## Main Definitions +## Main DefinitionsP - `ENNReal.logOrderIso`: The order isomorphism between `ℝ≥0∞` and `EReal` defined by `log` and `exp`. - `EReal.expOrderIso`: The order isomorphism between `EReal` and `ℝ≥0∞` defined by `exp` @@ -134,6 +134,4 @@ end Measurability end ENNReal -instance : PolishSpace EReal := - IsClosedEmbedding.polishSpace ⟨ENNReal.logOrderIso.symm.toHomeomorph.embedding, - ENNReal.logOrderIso.symm.toHomeomorph.range_coe ▸ isClosed_univ⟩ +instance : PolishSpace EReal := ENNReal.logOrderIso.symm.toHomeomorph.isClosedEmbedding.polishSpace diff --git a/Mathlib/CategoryTheory/Extensive.lean b/Mathlib/CategoryTheory/Extensive.lean index 94619f08a21bb..eedb5f6f44b82 100644 --- a/Mathlib/CategoryTheory/Extensive.lean +++ b/Mathlib/CategoryTheory/Extensive.lean @@ -294,9 +294,9 @@ noncomputable def finitaryExtensiveTopCatAux (Z : TopCat.{u}) · rintro _ ⟨x, rfl⟩; exact ⟨PUnit.unit, x.2.symm⟩ · rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩ refine ((TopCat.binaryCofan_isColimit_iff _).mpr ⟨?_, ?_, ?_⟩).some - · refine ⟨(Homeomorph.prodPUnit Z).embedding.comp embedding_subtype_val, ?_⟩ + · refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩ convert f.2.1 _ isOpen_range_inl - · refine ⟨(Homeomorph.prodPUnit Z).embedding.comp embedding_subtype_val, ?_⟩ + · refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩ convert f.2.1 _ isOpen_range_inr · convert Set.isCompl_range_inl_range_inr.preimage f @@ -321,7 +321,7 @@ instance finitaryExtensive_TopCat : FinitaryExtensive TopCat.{u} := by refine ⟨⟨l, ?_⟩, ContinuousMap.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ContinuousMap.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩ - apply (embedding_inl (X := X') (Y := Y')).toInducing.continuous_iff.mpr + apply (IsEmbedding.inl (X := X') (Y := Y')).toInducing.continuous_iff.mpr convert s.fst.2 using 1 exact (funext hl).symm · refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩ @@ -338,7 +338,7 @@ instance finitaryExtensive_TopCat : FinitaryExtensive TopCat.{u} := by refine ⟨⟨l, ?_⟩, ContinuousMap.ext fun a => (hl a).symm, TopCat.isTerminalPUnit.hom_ext _ _, fun {l'} h₁ _ => ContinuousMap.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩ - apply (embedding_inr (X := X') (Y := Y')).toInducing.continuous_iff.mpr + apply (IsEmbedding.inr (X := X') (Y := Y')).toInducing.continuous_iff.mpr convert s.fst.2 using 1 exact (funext hl).symm · intro Z f diff --git a/Mathlib/CategoryTheory/Galois/Topology.lean b/Mathlib/CategoryTheory/Galois/Topology.lean index f0bb5bf4ec1bb..89ee411e67d44 100644 --- a/Mathlib/CategoryTheory/Galois/Topology.lean +++ b/Mathlib/CategoryTheory/Galois/Topology.lean @@ -93,7 +93,7 @@ instance : T2Space (Aut F) := T2Space.of_injective_continuous (autEmbedding_injective F) continuous_induced_dom instance : TotallyDisconnectedSpace (Aut F) := - (Embedding.isTotallyDisconnected_range (autEmbedding_isClosedEmbedding F).embedding).mp + (autEmbedding_isClosedEmbedding F).isEmbedding.isTotallyDisconnected_range.mp (isTotallyDisconnected_of_totallyDisconnectedSpace _) instance : ContinuousMul (Aut F) := diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index f93d14d8c5e1b..4137d0e6aecfa 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -292,10 +292,10 @@ theorem isClosed_range : IsClosed (range I) := @[deprecated (since := "2024-03-17")] alias closed_range := isClosed_range theorem map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] I x := - I.isClosedEmbedding.toEmbedding.map_nhds_eq x + I.isClosedEmbedding.isEmbedding.map_nhds_eq x theorem map_nhdsWithin_eq (s : Set H) (x : H) : map I (𝓝[s] x) = 𝓝[I '' s] I x := - I.isClosedEmbedding.toEmbedding.map_nhdsWithin_eq s x + I.isClosedEmbedding.isEmbedding.map_nhdsWithin_eq s x theorem image_mem_nhdsWithin {x : H} {s : Set H} (hs : s ∈ 𝓝 x) : I '' s ∈ 𝓝[range I] I x := I.map_nhds_eq x ▸ image_mem_map hs @@ -351,7 +351,7 @@ open TopologicalSpace protected theorem secondCountableTopology [SecondCountableTopology E] (I : ModelWithCorners 𝕜 E H) : SecondCountableTopology H := - I.isClosedEmbedding.toEmbedding.secondCountableTopology + I.isClosedEmbedding.isEmbedding.secondCountableTopology end ModelWithCorners diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 6befd6aab6a80..6966f5cdf1f71 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -265,7 +265,7 @@ theorem to_iso [h' : Epi f.base] : IsIso f := by have : IsIso f.c := NatIso.isIso_of_isIso_app _ apply (config := { allowSynthFailures := true }) isIso_of_components - let t : X ≃ₜ Y := (Homeomorph.ofEmbedding _ H.base_open.toEmbedding).trans + let t : X ≃ₜ Y := (Homeomorph.ofIsEmbedding _ H.base_open.isEmbedding).trans { toFun := Subtype.val invFun := fun x => ⟨x, by rw [Set.range_iff_surjective.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩ @@ -476,7 +476,7 @@ instance forgetPreservesLimitsOfRight : PreservesLimit (cospan g f) (forget C) : theorem pullback_snd_isIso_of_range_subset (H : Set.range g.base ⊆ Set.range f.base) : IsIso (pullback.snd f g) := by - haveI := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.toEmbedding g.base H + haveI := TopCat.snd_iso_of_left_embedding_range_subset hf.base_open.isEmbedding g.base H have : IsIso (pullback.snd f g).base := by delta pullback.snd rw [← limit.isoLimitCone_hom_π ⟨_, pullbackConeOfLeftIsLimit f g⟩ WalkingCospan.right] diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index f0fe4fcd0af4a..3a800284d29f2 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -629,22 +629,25 @@ instance DiscreteMeasurableSpace.toBorelSpace {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [DiscreteMeasurableSpace α] : BorelSpace α := by constructor; ext; simp [MeasurableSpace.measurableSet_generateFrom, MeasurableSet.of_discrete] -protected theorem Embedding.measurableEmbedding {f : α → β} (h₁ : Embedding f) +protected theorem IsEmbedding.measurableEmbedding {f : α → β} (h₁ : IsEmbedding f) (h₂ : MeasurableSet (range f)) : MeasurableEmbedding f := show MeasurableEmbedding - (((↑) : range f → β) ∘ (Homeomorph.ofEmbedding f h₁).toMeasurableEquiv) from + (((↑) : range f → β) ∘ (Homeomorph.ofIsEmbedding f h₁).toMeasurableEquiv) from (MeasurableEmbedding.subtype_coe h₂).comp (MeasurableEquiv.measurableEmbedding _) -protected theorem IsClosedEmbedding.measurableEmbedding {f : α → β} (h : IsClosedEmbedding f) : - MeasurableEmbedding f := - h.toEmbedding.measurableEmbedding h.isClosed_range.measurableSet +@[deprecated (since := "2024-10-26")] +alias Embedding.measurableEmbedding := IsEmbedding.measurableEmbedding + +protected theorem IsClosedEmbedding.measurableEmbedding {f : α → β} + (h : IsClosedEmbedding f) : MeasurableEmbedding f := + h.isEmbedding.measurableEmbedding h.isClosed_range.measurableSet @[deprecated (since := "2024-10-20")] alias ClosedEmbedding.measurableEmbedding := IsClosedEmbedding.measurableEmbedding protected theorem IsOpenEmbedding.measurableEmbedding {f : α → β} (h : IsOpenEmbedding f) : MeasurableEmbedding f := - h.toEmbedding.measurableEmbedding h.isOpen_range.measurableSet + h.isEmbedding.measurableEmbedding h.isOpen_range.measurableSet @[deprecated (since := "2024-10-18")] alias OpenEmbedding.measurableEmbedding := IsOpenEmbedding.measurableEmbedding diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 7e5941d364518..adb2b6dba2e06 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -1064,7 +1064,7 @@ theorem MeasureTheory.Memℒp.of_comp_antilipschitzWith {α E F} {K'} [Measurabl rw [← dist_zero_right, ← dist_zero_right, ← g0] apply hg'.le_mul_dist have B : AEStronglyMeasurable f μ := - (hg'.isUniformEmbedding hg).embedding.aestronglyMeasurable_comp_iff.1 hL.1 + (hg'.isUniformEmbedding hg).isEmbedding.aestronglyMeasurable_comp_iff.1 hL.1 exact hL.of_le_mul B (Filter.Eventually.of_forall A) namespace LipschitzWith diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 012d894c0ae6f..3fdd10d06cb1e 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -684,7 +684,7 @@ lemma _root_.HasCompactSupport.stronglyMeasurable_of_prod {X Y : Type*} [Zero α /-- If `g` is a topological embedding, then `f` is strongly measurable iff `g ∘ f` is. -/ theorem _root_.Embedding.comp_stronglyMeasurable_iff {m : MeasurableSpace α} [TopologicalSpace β] [PseudoMetrizableSpace β] [TopologicalSpace γ] [PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} - (hg : Embedding g) : (StronglyMeasurable fun x => g (f x)) ↔ StronglyMeasurable f := by + (hg : IsEmbedding g) : (StronglyMeasurable fun x => g (f x)) ↔ StronglyMeasurable f := by letI := pseudoMetrizableSpacePseudoMetric γ borelize β γ refine @@ -1504,8 +1504,8 @@ theorem _root_.MeasurableEmbedding.aestronglyMeasurable_map_iff {γ : Type*} rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩ exact ⟨g₂, hgm₂, hf.ae_map_iff.2 heq⟩ -theorem _root_.Embedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β] - [PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} (hg : Embedding g) : +theorem _root_.IsEmbedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β] + [PseudoMetrizableSpace γ] {g : β → γ} {f : α → β} (hg : IsEmbedding g) : AEStronglyMeasurable (fun x => g (f x)) μ ↔ AEStronglyMeasurable f μ := by letI := pseudoMetrizableSpacePseudoMetric γ borelize β γ @@ -1521,6 +1521,9 @@ theorem _root_.Embedding.aestronglyMeasurable_comp_iff [PseudoMetrizableSpace β · rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩ exact ⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩ +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.aestronglyMeasurable_comp_iff := IsEmbedding.aestronglyMeasurable_comp_iff + /-- An almost everywhere sequential limit of almost everywhere strongly measurable functions is almost everywhere strongly measurable. -/ theorem _root_.aestronglyMeasurable_of_tendsto_ae {ι : Type*} [PseudoMetrizableSpace β] diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean index 95fbcc33ea7cf..232923661f030 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Lemmas.lean @@ -46,7 +46,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] theorem aestronglyMeasurable_smul_const_iff {f : α → 𝕜} {c : E} (hc : c ≠ 0) : AEStronglyMeasurable (fun x => f x • c) μ ↔ AEStronglyMeasurable f μ := - (isClosedEmbedding_smul_left hc).toEmbedding.aestronglyMeasurable_comp_iff + (isClosedEmbedding_smul_left hc).isEmbedding.aestronglyMeasurable_comp_iff end NormedSpace diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean index bcdccb8f63e40..b0faec3a21f94 100644 --- a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean +++ b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean @@ -711,8 +711,8 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi rcases mem_atTop_sets.1 hs with ⟨b, hb⟩ rw [← top_le_iff, ← volume_Ici (a := b)] exact measure_mono hb - rwa [B, ← Embedding.tendsto_nhds_iff] at A - exact (Completion.isUniformEmbedding_coe E).embedding + rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A + exact (Completion.isUniformEmbedding_coe E).isEmbedding variable [CompleteSpace E] @@ -908,8 +908,8 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Iic apply le_antisymm (le_top) rw [← volume_Iic (a := b)] exact measure_mono hb - rwa [B, ← Embedding.tendsto_nhds_iff] at A - exact (Completion.isUniformEmbedding_coe E).embedding + rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A + exact (Completion.isUniformEmbedding_coe E).isEmbedding variable [CompleteSpace E] diff --git a/Mathlib/MeasureTheory/Measure/DiracProba.lean b/Mathlib/MeasureTheory/Measure/DiracProba.lean index 51377c0135958..9a4f81e244015 100644 --- a/Mathlib/MeasureTheory/Measure/DiracProba.lean +++ b/Mathlib/MeasureTheory/Measure/DiracProba.lean @@ -13,7 +13,7 @@ import Mathlib.MeasureTheory.Measure.ProbabilityMeasure * `diracProba`: The Dirac delta mass at a point as a probability measure. ## Main results -* `embedding_diracProba`: If `X` is a completely regular T0 space with its Borel sigma algebra, +* `isEmbedding_diracProba`: If `X` is a completely regular T0 space with its Borel sigma algebra, then the mapping that takes a point `x : X` to the delta-measure `diracProba x` is an embedding `X ↪ ProbabilityMeasure X`. @@ -180,9 +180,12 @@ noncomputable def diracProbaHomeomorph [T0Space X] [CompletelyRegularSpace X] : /-- If `X` is a completely regular T0 space with its Borel sigma algebra, then the mapping that takes a point `x : X` to the delta-measure `diracProba x` is an embedding `X → ProbabilityMeasure X`. -/ -theorem embedding_diracProba [T0Space X] [CompletelyRegularSpace X] : - Embedding (fun (x : X) ↦ diracProba x) := - embedding_subtype_val.comp diracProbaHomeomorph.embedding +theorem isEmbedding_diracProba [T0Space X] [CompletelyRegularSpace X] : + IsEmbedding (fun (x : X) ↦ diracProba x) := + IsEmbedding.subtypeVal.comp diracProbaHomeomorph.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_diracProba := isEmbedding_diracProba end embed_to_probabilityMeasure diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index f10ffdcda79a3..bd19b12578128 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -501,16 +501,18 @@ lemma injective_toWeakDualBCNN : variable (Ω) -lemma embedding_toWeakDualBCNN : - Embedding (toWeakDualBCNN : FiniteMeasure Ω → WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) where +lemma isEmbedding_toWeakDualBCNN : + IsEmbedding (toWeakDualBCNN : FiniteMeasure Ω → WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) where induced := rfl inj := injective_toWeakDualBCNN +@[deprecated (since := "2024-10-26")] +alias embedding_toWeakDualBCNN := isEmbedding_toWeakDualBCNN + /-- On topological spaces where indicators of closed sets have decreasing approximating sequences of continuous functions (`HasOuterApproxClosed`), the topology of weak convergence of finite Borel measures is Hausdorff (`T2Space`). -/ -instance t2Space : T2Space (FiniteMeasure Ω) := - Embedding.t2Space (embedding_toWeakDualBCNN Ω) +instance t2Space : T2Space (FiniteMeasure Ω) := (isEmbedding_toWeakDualBCNN Ω).t2Space end Hausdorff -- section diff --git a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean index fa9209bc596e0..b0d9111ef2931 100644 --- a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean +++ b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean @@ -682,7 +682,7 @@ instance instMetrizableSpaceProbabilityMeasure (X : Type*) [TopologicalSpace X] [PseudoMetrizableSpace X] [SeparableSpace X] [MeasurableSpace X] [BorelSpace X] : MetrizableSpace (ProbabilityMeasure X) := by letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X - exact homeomorph_probabilityMeasure_levyProkhorov.embedding.metrizableSpace + exact homeomorph_probabilityMeasure_levyProkhorov.isEmbedding.metrizableSpace end Levy_Prokhorov_metrizes_convergence_in_distribution diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean index 465298ca8e9fc..e8e67cb9fb636 100644 --- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean @@ -252,16 +252,19 @@ theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) : (FiniteMeasure.continuous_testAgainstNN_eval f).comp toFiniteMeasure_continuous -- The canonical mapping from probability measures to finite measures is an embedding. -theorem toFiniteMeasure_embedding (Ω : Type*) [MeasurableSpace Ω] [TopologicalSpace Ω] +theorem toFiniteMeasure_isEmbedding (Ω : Type*) [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] : - Embedding (toFiniteMeasure : ProbabilityMeasure Ω → FiniteMeasure Ω) := + IsEmbedding (toFiniteMeasure : ProbabilityMeasure Ω → FiniteMeasure Ω) := { induced := rfl inj := fun _μ _ν h ↦ Subtype.eq <| congr_arg FiniteMeasure.toMeasure h } +@[deprecated (since := "2024-10-26")] +alias toFiniteMeasure_embedding := toFiniteMeasure_isEmbedding + theorem tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds {δ : Type*} (F : Filter δ) {μs : δ → ProbabilityMeasure Ω} {μ₀ : ProbabilityMeasure Ω} : Tendsto μs F (𝓝 μ₀) ↔ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ₀.toFiniteMeasure) := - Embedding.tendsto_nhds_iff (toFiniteMeasure_embedding Ω) + (toFiniteMeasure_isEmbedding Ω).tendsto_nhds_iff /-- A characterization of weak convergence of probability measures by the condition that the integrals of every continuous bounded nonnegative function converge to the integral of the function @@ -296,8 +299,7 @@ variable (Ω) /-- On topological spaces where indicators of closed sets have decreasing approximating sequences of continuous functions (`HasOuterApproxClosed`), the topology of convergence in distribution of Borel probability measures is Hausdorff (`T2Space`). -/ -instance t2Space : T2Space (ProbabilityMeasure Ω) := - Embedding.t2Space (toFiniteMeasure_embedding Ω) +instance t2Space : T2Space (ProbabilityMeasure Ω) := (toFiniteMeasure_isEmbedding Ω).t2Space end Hausdorff -- section diff --git a/Mathlib/Topology/Algebra/Constructions.lean b/Mathlib/Topology/Algebra/Constructions.lean index 96db33647784a..9f744da52548b 100644 --- a/Mathlib/Topology/Algebra/Constructions.lean +++ b/Mathlib/Topology/Algebra/Constructions.lean @@ -48,12 +48,11 @@ def opHomeomorph : M ≃ₜ Mᵐᵒᵖ where continuous_invFun := continuous_unop @[to_additive] -instance instT2Space [T2Space M] : T2Space Mᵐᵒᵖ := - opHomeomorph.symm.embedding.t2Space +instance instT2Space [T2Space M] : T2Space Mᵐᵒᵖ := opHomeomorph.t2Space @[to_additive] instance instDiscreteTopology [DiscreteTopology M] : DiscreteTopology Mᵐᵒᵖ := - opHomeomorph.symm.embedding.discreteTopology + opHomeomorph.symm.isEmbedding.discreteTopology @[to_additive (attr := simp)] theorem map_op_nhds (x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x) := @@ -90,16 +89,18 @@ theorem inducing_embedProduct : Inducing (embedProduct M) := ⟨rfl⟩ @[to_additive] -theorem embedding_embedProduct : Embedding (embedProduct M) := +theorem isEmbedding_embedProduct : IsEmbedding (embedProduct M) := ⟨inducing_embedProduct, embedProduct_injective M⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_embedProduct := isEmbedding_embedProduct + @[to_additive] -instance instT2Space [T2Space M] : T2Space Mˣ := - embedding_embedProduct.t2Space +instance instT2Space [T2Space M] : T2Space Mˣ := isEmbedding_embedProduct.t2Space @[to_additive] instance instDiscreteTopology [DiscreteTopology M] : DiscreteTopology Mˣ := - embedding_embedProduct.discreteTopology + isEmbedding_embedProduct.discreteTopology @[to_additive] lemma topology_eq_inf : instTopologicalSpaceUnits = @@ -108,12 +109,12 @@ instance instDiscreteTopology [DiscreteTopology M] : DiscreteTopology Mˣ := instTopologicalSpaceMulOpposite, induced_compose]; rfl /-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding. -Use `Units.embedding_val₀`, `Units.embedding_val`, or `toUnits_homeomorph` instead. -/ +Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/ @[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a -topological embedding. Use `AddUnits.embedding_val` or `toAddUnits_homeomorph` instead."] -lemma embedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M} +topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead."] +lemma isEmbedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ u : Mˣ, f u.1 = ↑u⁻¹) : - Embedding (val : Mˣ → M) := by + IsEmbedding (val : Mˣ → M) := by refine ⟨⟨?_⟩, ext⟩ rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced, @continuous_iff_continuousAt _ _ (.induced _ _)] @@ -121,13 +122,16 @@ lemma embedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢ exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_val_mk' := isEmbedding_val_mk' + /-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding. -Use `Units.embedding_val₀`, `Units.embedding_val`, or `toUnits_homeomorph` instead. -/ +Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/ @[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a -topological embedding. Use `AddUnits.embedding_val` or `toAddUnits_homeomorph` instead."] +topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead."] lemma embedding_val_mk {M : Type*} [DivisionMonoid M] [TopologicalSpace M] - (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : Embedding (val : Mˣ → M) := - embedding_val_mk' h fun u ↦ (val_inv_eq_inv_val u).symm + (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : IsEmbedding (val : Mˣ → M) := + isEmbedding_val_mk' h fun u ↦ (val_inv_eq_inv_val u).symm @[to_additive] theorem continuous_embedProduct : Continuous (embedProduct M) := diff --git a/Mathlib/Topology/Algebra/Constructions/DomMulAct.lean b/Mathlib/Topology/Algebra/Constructions/DomMulAct.lean index f8c0f313ada70..c3c41395910d4 100644 --- a/Mathlib/Topology/Algebra/Constructions/DomMulAct.lean +++ b/Mathlib/Topology/Algebra/Constructions/DomMulAct.lean @@ -20,8 +20,7 @@ since the types aren't definitionally equal. topological space, group action, domain action -/ -open Filter TopologicalSpace -open scoped Topology +open Filter TopologicalSpace Topology namespace DomMulAct @@ -48,12 +47,15 @@ def mkHomeomorph : M ≃ₜ Mᵈᵐᵃ where theorem coe_mkHomeomorph_symm : ⇑(mkHomeomorph : M ≃ₜ Mᵈᵐᵃ).symm = mk.symm := rfl @[to_additive] theorem inducing_mk : Inducing (@mk M) := mkHomeomorph.inducing -@[to_additive] theorem embedding_mk : Embedding (@mk M) := mkHomeomorph.embedding +@[to_additive] theorem isEmbedding_mk : IsEmbedding (@mk M) := mkHomeomorph.isEmbedding @[to_additive] theorem isOpenEmbedding_mk : IsOpenEmbedding (@mk M) := mkHomeomorph.isOpenEmbedding @[to_additive] theorem isClosedEmbedding_mk : IsClosedEmbedding (@mk M) := mkHomeomorph.isClosedEmbedding @[to_additive] theorem isQuotientMap_mk : IsQuotientMap (@mk M) := mkHomeomorph.isQuotientMap +@[deprecated (since := "2024-10-26")] +alias embedding_mk := isEmbedding_mk + @[deprecated (since := "2024-10-22")] alias quotientMap_mk := isQuotientMap_mk @@ -64,14 +66,15 @@ alias closedEmbedding_mk := isClosedEmbedding_mk alias openEmbedding_mk := isOpenEmbedding_mk @[to_additive] theorem inducing_mk_symm : Inducing (@mk M).symm := mkHomeomorph.symm.inducing -@[to_additive] theorem embedding_mk_symm : Embedding (@mk M).symm := mkHomeomorph.symm.embedding +@[to_additive] theorem isEmbedding_mk_symm : IsEmbedding (@mk M).symm := + mkHomeomorph.symm.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_mk_symm := isEmbedding_mk_symm @[to_additive] theorem isOpenEmbedding_mk_symm : IsOpenEmbedding (@mk M).symm := mkHomeomorph.symm.isOpenEmbedding -@[deprecated (since := "2024-10-18")] -alias openEmbedding_mk_symm := isOpenEmbedding_mk_symm - @[to_additive] theorem isClosedEmbedding_mk_symm : IsClosedEmbedding (@mk M).symm := mkHomeomorph.symm.isClosedEmbedding @@ -85,30 +88,30 @@ theorem isQuotientMap_mk_symm : IsQuotientMap (@mk M).symm := mkHomeomorph.symm. @[deprecated (since := "2024-10-22")] alias quotientMap_mk_symm := isQuotientMap_mk_symm -@[to_additive] instance instT0Space [T0Space M] : T0Space Mᵈᵐᵃ := embedding_mk_symm.t0Space -@[to_additive] instance instT1Space [T1Space M] : T1Space Mᵈᵐᵃ := embedding_mk_symm.t1Space -@[to_additive] instance instT2Space [T2Space M] : T2Space Mᵈᵐᵃ := embedding_mk_symm.t2Space -@[to_additive] instance instT25Space [T25Space M] : T25Space Mᵈᵐᵃ := embedding_mk_symm.t25Space -@[to_additive] instance instT3Space [T3Space M] : T3Space Mᵈᵐᵃ := embedding_mk_symm.t3Space -@[to_additive] instance instT4Space [T4Space M] : T4Space Mᵈᵐᵃ := isClosedEmbedding_mk_symm.t4Space -@[to_additive] instance instT5Space [T5Space M] : T5Space Mᵈᵐᵃ := isClosedEmbedding_mk_symm.t5Space +@[to_additive] instance instT0Space [T0Space M] : T0Space Mᵈᵐᵃ := mkHomeomorph.t0Space +@[to_additive] instance instT1Space [T1Space M] : T1Space Mᵈᵐᵃ := mkHomeomorph.t1Space +@[to_additive] instance instT2Space [T2Space M] : T2Space Mᵈᵐᵃ := mkHomeomorph.t2Space +@[to_additive] instance instT25Space [T25Space M] : T25Space Mᵈᵐᵃ := mkHomeomorph.t25Space +@[to_additive] instance instT3Space [T3Space M] : T3Space Mᵈᵐᵃ := mkHomeomorph.t3Space +@[to_additive] instance instT4Space [T4Space M] : T4Space Mᵈᵐᵃ := mkHomeomorph.t4Space +@[to_additive] instance instT5Space [T5Space M] : T5Space Mᵈᵐᵃ := mkHomeomorph.t5Space -@[to_additive] instance instR0Space [R0Space M] : R0Space Mᵈᵐᵃ := embedding_mk_symm.r0Space -@[to_additive] instance instR1Space [R1Space M] : R1Space Mᵈᵐᵃ := embedding_mk_symm.r1Space +@[to_additive] instance instR0Space [R0Space M] : R0Space Mᵈᵐᵃ := isEmbedding_mk_symm.r0Space +@[to_additive] instance instR1Space [R1Space M] : R1Space Mᵈᵐᵃ := isEmbedding_mk_symm.r1Space @[to_additive] -instance instRegularSpace [RegularSpace M] : RegularSpace Mᵈᵐᵃ := embedding_mk_symm.regularSpace +instance instRegularSpace [RegularSpace M] : RegularSpace Mᵈᵐᵃ := isEmbedding_mk_symm.regularSpace @[to_additive] -instance instNormalSpace [NormalSpace M] : NormalSpace Mᵈᵐᵃ := isClosedEmbedding_mk_symm.normalSpace +instance instNormalSpace [NormalSpace M] : NormalSpace Mᵈᵐᵃ := mkHomeomorph.normalSpace @[to_additive] instance instCompletelyNormalSpace [CompletelyNormalSpace M] : CompletelyNormalSpace Mᵈᵐᵃ := - isClosedEmbedding_mk_symm.completelyNormalSpace + mkHomeomorph.symm.isEmbedding.completelyNormalSpace @[to_additive] instance instDiscreteTopology [DiscreteTopology M] : DiscreteTopology Mᵈᵐᵃ := - embedding_mk_symm.discreteTopology + isEmbedding_mk_symm.discreteTopology @[to_additive] instance instSeparableSpace [SeparableSpace M] : SeparableSpace Mᵈᵐᵃ := diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean index ff9ec26c16279..d91dbfb62ec0e 100644 --- a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean +++ b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean @@ -236,10 +236,13 @@ theorem inducing_toContinuousMap : Inducing (toContinuousMap : ContinuousMonoidH ⟨rfl⟩ @[to_additive] -theorem embedding_toContinuousMap : - Embedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) := +theorem isEmbedding_toContinuousMap : + IsEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) := ⟨inducing_toContinuousMap A B, toContinuousMap_injective⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_toContinuousMap := isEmbedding_toContinuousMap + @[to_additive] instance instContinuousEvalConst : ContinuousEvalConst (ContinuousMonoidHom A B) A B := .of_continuous_forget (inducing_toContinuousMap A B).continuous @@ -260,7 +263,7 @@ lemma range_toContinuousMap : @[to_additive] theorem isClosedEmbedding_toContinuousMap [ContinuousMul B] [T2Space B] : IsClosedEmbedding (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) where - toEmbedding := embedding_toContinuousMap A B + toIsEmbedding := isEmbedding_toContinuousMap A B isClosed_range := by simp only [range_toContinuousMap, Set.setOf_and, Set.setOf_forall] refine .inter (isClosed_singleton.preimage (continuous_eval_const 1)) <| @@ -275,7 +278,7 @@ variable {A B C D E} @[to_additive] instance [T2Space B] : T2Space (ContinuousMonoidHom A B) := - (embedding_toContinuousMap A B).t2Space + (isEmbedding_toContinuousMap A B).t2Space @[to_additive] instance : TopologicalGroup (ContinuousMonoidHom A E) := diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean index 49cb37c34c00c..cea2d7ee9d120 100644 --- a/Mathlib/Topology/Algebra/Group/Basic.lean +++ b/Mathlib/Topology/Algebra/Group/Basic.lean @@ -1257,7 +1257,7 @@ variable {G} @[to_additive] theorem group_inseparable_iff {x y : G} : Inseparable x y ↔ x / y ∈ closure (1 : Set G) := by rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable, - ← (Homeomorph.mulRight y⁻¹).embedding.inseparable_iff] + ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff] simp [div_eq_mul_inv] @[to_additive] @@ -1563,9 +1563,12 @@ def toUnits_homeomorph [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ continuous_toFun := Units.continuous_iff.2 ⟨continuous_id, continuous_inv⟩ continuous_invFun := Units.continuous_val -@[to_additive] theorem Units.embedding_val [Group G] [TopologicalSpace G] [ContinuousInv G] : - Embedding (val : Gˣ → G) := - toUnits_homeomorph.symm.embedding +@[to_additive] theorem Units.isEmbedding_val [Group G] [TopologicalSpace G] [ContinuousInv G] : + IsEmbedding (val : Gˣ → G) := + toUnits_homeomorph.symm.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias Units.embedding_val := Units.isEmbedding_val namespace Units diff --git a/Mathlib/Topology/Algebra/GroupWithZero.lean b/Mathlib/Topology/Algebra/GroupWithZero.lean index 8874a996043c3..17c7548166c68 100644 --- a/Mathlib/Topology/Algebra/GroupWithZero.lean +++ b/Mathlib/Topology/Algebra/GroupWithZero.lean @@ -129,10 +129,13 @@ end Inv₀ /-- If `G₀` is a group with zero with topology such that `x ↦ x⁻¹` is continuous at all nonzero points. Then the coercion `G₀ˣ → G₀` is a topological embedding. -/ -theorem Units.embedding_val₀ [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] : - Embedding (val : G₀ˣ → G₀) := +theorem Units.isEmbedding_val₀ [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] : + IsEmbedding (val : G₀ˣ → G₀) := embedding_val_mk <| (continuousOn_inv₀ (G₀ := G₀)).mono fun _ ↦ IsUnit.ne_zero +@[deprecated (since := "2024-10-26")] +alias Units.embedding_val₀ := Units.isEmbedding_val₀ + section NhdsInv variable [GroupWithZero G₀] [TopologicalSpace G₀] [HasContinuousInv₀ G₀] {x : G₀} diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean index 6002b8905bc13..0ec905dcba11e 100644 --- a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean +++ b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean @@ -134,28 +134,31 @@ end UniformAddGroup variable [TopologicalSpace F] [TopologicalAddGroup F] -lemma embedding_toContinuousMultilinearMap : - Embedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) := +lemma isEmbedding_toContinuousMultilinearMap : + IsEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) := letI := TopologicalAddGroup.toUniformSpace F haveI := comm_topologicalAddGroup_is_uniform (G := F) - isUniformEmbedding_toContinuousMultilinearMap.embedding + isUniformEmbedding_toContinuousMultilinearMap.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_toContinuousMultilinearMap := isEmbedding_toContinuousMultilinearMap instance instTopologicalAddGroup : TopologicalAddGroup (E [⋀^ι]→L[𝕜] F) := - embedding_toContinuousMultilinearMap.topologicalAddGroup + isEmbedding_toContinuousMultilinearMap.topologicalAddGroup (toContinuousMultilinearMapLinear (R := ℕ)) @[continuity, fun_prop] lemma continuous_toContinuousMultilinearMap : Continuous (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) := - embedding_toContinuousMultilinearMap.continuous + isEmbedding_toContinuousMultilinearMap.continuous instance instContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : ContinuousConstSMul M (E [⋀^ι]→L[𝕜] F) := - embedding_toContinuousMultilinearMap.continuousConstSMul id rfl + isEmbedding_toContinuousMultilinearMap.continuousConstSMul id rfl instance instContinuousSMul [ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F) := - embedding_toContinuousMultilinearMap.continuousSMul continuous_id rfl + isEmbedding_toContinuousMultilinearMap.continuousSMul continuous_id rfl theorem hasBasis_nhds_zero_of_basis {ι' : Type*} {p : ι' → Prop} {b : ι' → Set F} (h : (𝓝 (0 : F)).HasBasis p b) : @@ -176,7 +179,7 @@ variable [ContinuousSMul 𝕜 E] lemma isClosedEmbedding_toContinuousMultilinearMap [T2Space F] : IsClosedEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F) := - ⟨embedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩ + ⟨isEmbedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩ @[deprecated (since := "2024-10-20")] alias closedEmbedding_toContinuousMultilinearMap := isClosedEmbedding_toContinuousMultilinearMap @@ -201,16 +204,19 @@ section RestrictScalars variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] -theorem embedding_restrictScalars : - Embedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := +theorem isEmbedding_restrictScalars : + IsEmbedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (isUniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_restrictScalars := isEmbedding_restrictScalars @[continuity, fun_prop] theorem continuous_restrictScalars : Continuous (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := - embedding_restrictScalars.continuous + isEmbedding_restrictScalars.continuous variable (𝕜') in /-- `ContinuousMultilinearMap.restrictScalars` as a `ContinuousLinearMap`. -/ diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 8f9b4584bce46..bdab9d7a3ba36 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -520,7 +520,7 @@ theorem Submodule.closed_of_finiteDimensional theorem LinearMap.isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] {f : E →ₗ[𝕜] F} (hf : LinearMap.ker f = ⊥) : IsClosedEmbedding f := let g := LinearEquiv.ofInjective f (LinearMap.ker_eq_bot.mp hf) - { embedding_subtype_val.comp g.toContinuousLinearEquiv.toHomeomorph.embedding with + { IsEmbedding.subtypeVal.comp g.toContinuousLinearEquiv.toHomeomorph.isEmbedding with isClosed_range := by haveI := f.finiteDimensional_range simpa [LinearMap.range_coe f] using f.range.closed_of_finiteDimensional } diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean index 87d86ced20d2e..e757aff98c206 100644 --- a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean +++ b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean @@ -78,10 +78,13 @@ lemma isUniformEmbedding_toUniformOnFun : @[deprecated (since := "2024-10-01")] alias uniformEmbedding_toUniformOnFun := isUniformEmbedding_toUniformOnFun -lemma embedding_toUniformOnFun : - Embedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → +lemma isEmbedding_toUniformOnFun : + IsEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) := - isUniformEmbedding_toUniformOnFun.embedding + isUniformEmbedding_toUniformOnFun.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_toUniformOnFun := isEmbedding_toUniformOnFun theorem uniformContinuous_coe_fun [∀ i, ContinuousSMul 𝕜 (E i)] : UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) := @@ -192,7 +195,7 @@ instance instContinuousSMul [ContinuousSMul 𝕜 F] : let φ : ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] (Π i, E i) → F := { toFun := (↑), map_add' := fun _ _ ↦ rfl, map_smul' := fun _ _ ↦ rfl } UniformOnFun.continuousSMul_induced_of_image_bounded _ _ _ _ φ - embedding_toUniformOnFun.toInducing fun _ _ hu ↦ hu.image_multilinear _ + isEmbedding_toUniformOnFun.toInducing fun _ _ hu ↦ hu.image_multilinear _ theorem hasBasis_nhds_zero_of_basis {ι : Type*} {p : ι → Prop} {b : ι → Set F} (h : (𝓝 (0 : F)).HasBasis p b) : @@ -235,18 +238,21 @@ section RestrictScalars variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [∀ i, Module 𝕜' (E i)] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] -theorem embedding_restrictScalars : - Embedding +theorem isEmbedding_restrictScalars : + IsEmbedding (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (isUniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_restrictScalars := isEmbedding_restrictScalars @[continuity, fun_prop] theorem continuous_restrictScalars : Continuous (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := - embedding_restrictScalars.continuous + isEmbedding_restrictScalars.continuous variable (𝕜') in /-- `ContinuousMultilinearMap.restrictScalars` as a `ContinuousLinearMap`. -/ diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean index 40a009bdf15e6..0ff9730bfc9ff 100644 --- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean +++ b/Mathlib/Topology/Algebra/Module/StrongTopology.lean @@ -130,10 +130,13 @@ theorem isUniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Se @[deprecated (since := "2024-10-01")] alias uniformEmbedding_coeFn := isUniformEmbedding_coeFn -theorem embedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : - Embedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F) +theorem isEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : + IsEmbedding (X := UniformConvergenceCLM σ F 𝔖) (Y := E →ᵤ[𝔖] F) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) := - IsUniformEmbedding.embedding (isUniformEmbedding_coeFn _ _ _) + IsUniformEmbedding.isEmbedding (isUniformEmbedding_coeFn _ _ _) + +@[deprecated (since := "2024-10-26")] +alias embedding_coeFn := isEmbedding_coeFn instance instAddCommGroup [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : AddCommGroup (UniformConvergenceCLM σ F 𝔖) := ContinuousLinearMap.addCommGroup @@ -162,12 +165,14 @@ theorem continuousEvalConst [TopologicalSpace F] [TopologicalAddGroup F] letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp - (embedding_coeFn σ F 𝔖).continuous + (isEmbedding_coeFn σ F 𝔖).continuous theorem t2Space [TopologicalSpace F] [TopologicalAddGroup F] [T2Space F] - (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) := - have := continuousEvalConst σ F 𝔖 h𝔖 - .of_injective_continuous DFunLike.coe_injective continuous_coeFun + (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = univ) : T2Space (UniformConvergenceCLM σ F 𝔖) := by + letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F + haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform + haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖 + exact (isEmbedding_coeFn σ F 𝔖).t2Space instance instDistribMulAction (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [TopologicalSpace F] [TopologicalAddGroup F] [ContinuousConstSMul M F] (𝔖 : Set (Set E)) : @@ -196,7 +201,7 @@ theorem hasBasis_nhds_zero_of_basis [TopologicalSpace F] [TopologicalAddGroup F] fun Si => { f : E →SL[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2 } := by letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - rw [(embedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap] + rw [(isEmbedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap] exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap DFunLike.coe theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F] @@ -213,7 +218,7 @@ theorem nhds_zero_eq_of_basis [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 𝓟 {f : UniformConvergenceCLM σ F 𝔖 | MapsTo f s (b i)} := by letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - rw [(embedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap, + rw [(isEmbedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap, UniformOnFun.nhds_eq_of_basis _ _ h.uniformity_of_nhds_zero] simp [MapsTo] @@ -280,7 +285,7 @@ theorem tendsto_iff_tendstoUniformlyOn {ι : Type*} {p : Filter ι} [UniformSpac [UniformAddGroup F] (𝔖 : Set (Set E)) {a : ι → UniformConvergenceCLM σ F 𝔖} {a₀ : UniformConvergenceCLM σ F 𝔖} : Filter.Tendsto a p (𝓝 a₀) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (a · ·) a₀ p s := by - rw [(embedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn] + rw [(isEmbedding_coeFn σ F 𝔖).tendsto_nhds_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn] rfl variable {F} in @@ -468,11 +473,11 @@ def precomp [TopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurj cont := by letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform - rw [(UniformConvergenceCLM.embedding_coeFn _ _ _).continuous_iff] + rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff] -- Porting note: without this, the following doesn't work change Continuous ((fun f ↦ UniformOnFun.ofFun _ (f ∘ L)) ∘ DFunLike.coe) exact (UniformOnFun.precomp_uniformContinuous fun S hS => hS.image L).continuous.comp - (UniformConvergenceCLM.embedding_coeFn _ _ _).continuous + (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous variable (E) {G} @@ -490,10 +495,10 @@ def postcomp [TopologicalAddGroup F] [TopologicalAddGroup G] [ContinuousConstSMu haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - rw [(UniformConvergenceCLM.embedding_coeFn _ _ _).continuous_iff] + rw [(UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous_iff] exact (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp - (UniformConvergenceCLM.embedding_coeFn _ _ _).continuous + (UniformConvergenceCLM.isEmbedding_coeFn _ _ _).continuous end BoundedSets @@ -544,16 +549,19 @@ variable [TopologicalSpace F] [TopologicalAddGroup F] [Module 𝕜 F] (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] -theorem embedding_restrictScalars : - Embedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := +theorem isEmbedding_restrictScalars : + IsEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (isUniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_restrictScalars := isEmbedding_restrictScalars @[continuity, fun_prop] theorem continuous_restrictScalars : Continuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := - (embedding_restrictScalars _).continuous + (isEmbedding_restrictScalars _).continuous variable (𝕜 E F) variable (𝕜'' : Type*) [Ring 𝕜''] diff --git a/Mathlib/Topology/Algebra/Module/WeakBilin.lean b/Mathlib/Topology/Algebra/Module/WeakBilin.lean index 916301730f678..256a8a929210a 100644 --- a/Mathlib/Topology/Algebra/Module/WeakBilin.lean +++ b/Mathlib/Topology/Algebra/Module/WeakBilin.lean @@ -106,14 +106,17 @@ theorem continuous_of_continuous_eval [TopologicalSpace α] {g : α → WeakBili continuous_induced_rng.2 (continuous_pi_iff.mpr h) /-- The coercion `(fun x y => B x y) : E → (F → 𝕜)` is an embedding. -/ -theorem embedding {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective B) : - Embedding fun (x : WeakBilin B) y => B x y := - Function.Injective.embedding_induced <| LinearMap.coe_injective.comp hB +theorem isEmbedding {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : Function.Injective B) : + IsEmbedding fun (x : WeakBilin B) y => B x y := + Function.Injective.isEmbedding_induced <| LinearMap.coe_injective.comp hB + +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding theorem tendsto_iff_forall_eval_tendsto {l : Filter α} {f : α → WeakBilin B} {x : WeakBilin B} (hB : Function.Injective B) : Tendsto f l (𝓝 x) ↔ ∀ y, Tendsto (fun i => B (f i) y) l (𝓝 (B x y)) := by - rw [← tendsto_pi_nhds, Embedding.tendsto_nhds_iff (embedding hB)] + rw [← tendsto_pi_nhds, (isEmbedding hB).tendsto_nhds_iff] rfl /-- Addition in `WeakBilin B` is continuous. -/ diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean index 45e6b09628962..d2bdbb2408760 100644 --- a/Mathlib/Topology/Algebra/Module/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean @@ -143,9 +143,7 @@ theorem continuous_of_continuous_eval [TopologicalSpace α] {g : α → WeakDual continuous_induced_rng.2 (continuous_pi_iff.mpr h) instance instT2Space [T2Space 𝕜] : T2Space (WeakDual 𝕜 E) := - Embedding.t2Space <| - WeakBilin.embedding <| - show Function.Injective (topDualPairing 𝕜 E) from ContinuousLinearMap.coe_injective + (WeakBilin.isEmbedding ContinuousLinearMap.coe_injective).t2Space end Semiring diff --git a/Mathlib/Topology/Algebra/ProperAction/Basic.lean b/Mathlib/Topology/Algebra/ProperAction/Basic.lean index 52a706f6ad93c..5b68b2d2d0d6f 100644 --- a/Mathlib/Topology/Algebra/ProperAction/Basic.lean +++ b/Mathlib/Topology/Algebra/ProperAction/Basic.lean @@ -130,7 +130,7 @@ theorem t2Space_of_properSMul_of_t2Group [h_proper : ProperSMul G X] [T2Space G] refine IsClosedEmbedding.isProperMap ⟨?_, ?_⟩ · let g := fun gx : G × X ↦ gx.2 have : Function.LeftInverse g f := fun x ↦ by simp - exact this.embedding (by fun_prop) (by fun_prop) + exact this.isEmbedding (by fun_prop) (by fun_prop) · have : range f = ({1} ×ˢ univ) := by simp rw [this] exact isClosed_singleton.prod isClosed_univ diff --git a/Mathlib/Topology/Algebra/SeparationQuotient/Section.lean b/Mathlib/Topology/Algebra/SeparationQuotient/Section.lean index 5e4941bd8a541..186ab10d15349 100644 --- a/Mathlib/Topology/Algebra/SeparationQuotient/Section.lean +++ b/Mathlib/Topology/Algebra/SeparationQuotient/Section.lean @@ -59,11 +59,14 @@ theorem postcomp_mkCLM_surjective {L : Type*} [Semiring L] (σ : L →+* K) rw [← ContinuousLinearMap.comp_assoc, mkCLM_comp_outCLM, ContinuousLinearMap.id_comp] /-- The `SeparationQuotient.outCLM K E` map is a topological embedding. -/ -theorem outCLM_embedding : Embedding (outCLM K E) := - Function.LeftInverse.embedding (mk_outCLM K) continuous_mk (map_continuous _) +theorem isEmbedding_outCLM : IsEmbedding (outCLM K E) := + Function.LeftInverse.isEmbedding (mk_outCLM K) continuous_mk (map_continuous _) + +@[deprecated (since := "2024-10-26")] +alias outCLM_embedding := isEmbedding_outCLM theorem outCLM_injective : Function.Injective (outCLM K E) := - (outCLM_embedding K E).injective + (isEmbedding_outCLM K E).injective end VectorSpace diff --git a/Mathlib/Topology/Algebra/StarSubalgebra.lean b/Mathlib/Topology/Algebra/StarSubalgebra.lean index 295e2416e5169..7cf15ed3628a0 100644 --- a/Mathlib/Topology/Algebra/StarSubalgebra.lean +++ b/Mathlib/Topology/Algebra/StarSubalgebra.lean @@ -33,14 +33,18 @@ instance [TopologicalSemiring A] (s : StarSubalgebra R A) : TopologicalSemiring s.toSubalgebra.topologicalSemiring /-- The `StarSubalgebra.inclusion` of a star subalgebra is an `Embedding`. -/ -theorem embedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : Embedding (inclusion h) := - { induced := Eq.symm induced_compose - inj := Subtype.map_injective h Function.injective_id } +lemma isEmbedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : + IsEmbedding (inclusion h) where + induced := Eq.symm induced_compose + inj := Subtype.map_injective h Function.injective_id + +@[deprecated (since := "2024-10-26")] +alias embedding_inclusion := isEmbedding_inclusion /-- The `StarSubalgebra.inclusion` of a closed star subalgebra is a `IsClosedEmbedding`. -/ theorem isClosedEmbedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (hS₁ : IsClosed (S₁ : Set A)) : IsClosedEmbedding (inclusion h) := - { embedding_inclusion h with + { IsEmbedding.inclusion h with isClosed_range := isClosed_induced_iff.2 ⟨S₁, hS₁, by convert (Set.range_subtype_map id _).symm @@ -135,7 +139,7 @@ theorem _root_.StarAlgHom.ext_topologicalClosure [T2Space B] {S : StarSubalgebra φ = ψ := by rw [DFunLike.ext'_iff] have : Dense (Set.range <| inclusion (le_topologicalClosure S)) := by - refine embedding_subtype_val.toInducing.dense_iff.2 fun x => ?_ + refine IsEmbedding.subtypeVal.toInducing.dense_iff.2 fun x => ?_ convert show ↑x ∈ closure (S : Set A) from x.prop rw [← Set.range_comp] exact diff --git a/Mathlib/Topology/Bases.lean b/Mathlib/Topology/Bases.lean index 796775ecb345e..082f387a0fde5 100644 --- a/Mathlib/Topology/Bases.lean +++ b/Mathlib/Topology/Bases.lean @@ -665,11 +665,14 @@ protected theorem _root_.Inducing.firstCountableTopology {β : Type*} rw [hf.1] exact firstCountableTopology_induced α β f -protected theorem _root_.Embedding.firstCountableTopology {β : Type*} - [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : Embedding f) : +protected theorem _root_.IsEmbedding.firstCountableTopology {β : Type*} + [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) : FirstCountableTopology α := hf.1.firstCountableTopology +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.firstCountableTopology := IsEmbedding.firstCountableTopology + namespace FirstCountableTopology /-- In a first-countable space, a cluster point `x` of a sequence @@ -974,13 +977,13 @@ protected theorem Inducing.secondCountableTopology [TopologicalSpace β] [Second rw [hf.1] exact secondCountableTopology_induced α β f -protected theorem Embedding.secondCountableTopology +protected theorem IsEmbedding.secondCountableTopology [TopologicalSpace β] [SecondCountableTopology β] - (hf : Embedding f) : SecondCountableTopology α := + (hf : IsEmbedding f) : SecondCountableTopology α := hf.1.secondCountableTopology -protected theorem Embedding.separableSpace - [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : Embedding f) : +protected theorem IsEmbedding.separableSpace + [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) : TopologicalSpace.SeparableSpace α := by have := hf.secondCountableTopology exact SecondCountableTopology.to_separableSpace diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index 275dd04efa2cf..d4b021e2620d3 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -1788,7 +1788,7 @@ Given a profinite set `S` and a closed embedding `S → (I → Bool)`, the `ℤ` -/ theorem Nobeling_aux : Module.Free ℤ (LocallyConstant S ℤ) := Module.Free.of_equiv' (Module.Free.of_basis <| GoodProducts.Basis _ hι.isClosed_range) (LocallyConstant.congrLeftₗ ℤ - (Homeomorph.ofEmbedding ι hι.toEmbedding)).symm + (.ofIsEmbedding ι hι.isEmbedding)).symm end NobelingProof @@ -1801,7 +1801,7 @@ def Nobeling.ι : S → ({C : Set S // IsClopen C} → Bool) := fun s C => decid open scoped Classical in /-- The map `Nobeling.ι` is a closed embedding. -/ -theorem Nobeling.embedding : IsClosedEmbedding (Nobeling.ι S) := by +theorem Nobeling.isClosedEmbedding : IsClosedEmbedding (Nobeling.ι S) := by apply Continuous.isClosedEmbedding · dsimp (config := { unfoldPartialApp := true }) [ι] refine continuous_pi ?_ @@ -1826,6 +1826,9 @@ theorem Nobeling.embedding : IsClosedEmbedding (Nobeling.ι S) := by rw [← congr_fun h ⟨C, hC⟩] exact decide_eq_true hh.1 +@[deprecated (since := "2024-10-26")] +alias Nobeling.embedding := Nobeling.isClosedEmbedding + end Profinite open Profinite NobelingProof @@ -1835,6 +1838,6 @@ instance LocallyConstant.freeOfProfinite (S : Profinite.{u}) : Module.Free ℤ (LocallyConstant S ℤ) := @Nobeling_aux {C : Set S // IsClopen C} (IsWellOrder.linearOrder WellOrderingRel) WellOrderingRel.isWellOrder - S (Nobeling.ι S) (Nobeling.embedding S) + S (Nobeling.ι S) (Nobeling.isClosedEmbedding S) set_option linter.style.longFile 2000 diff --git a/Mathlib/Topology/Category/Stonean/Limits.lean b/Mathlib/Topology/Category/Stonean/Limits.lean index 2b9c500e98a2e..bb3322edc7eeb 100644 --- a/Mathlib/Topology/Category/Stonean/Limits.lean +++ b/Mathlib/Topology/Category/Stonean/Limits.lean @@ -39,7 +39,7 @@ lemma extremallyDisconnected_preimage : ExtremallyDisconnected (i ⁻¹' (Set.ra lemma extremallyDisconnected_pullback : ExtremallyDisconnected {xy : X × Y | f xy.1 = i xy.2} := have := extremallyDisconnected_preimage i hi - let e := (TopCat.pullbackHomeoPreimage i i.2 f hi.toEmbedding).symm + let e := (TopCat.pullbackHomeoPreimage i i.2 f hi.isEmbedding).symm let e' : {xy : X × Y | f xy.1 = i xy.2} ≃ₜ {xy : Y × X | i xy.1 = f xy.2} := by exact TopCat.homeoOfIso ((TopCat.pullbackIsoProdSubtype f i).symm ≪≫ pullbackSymmetry _ _ ≪≫ diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean index 132e2144e2090..ea767c6dc7158 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Products.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Products.lean @@ -252,13 +252,16 @@ theorem inducing_prod_map {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf erw [← hf.induced, ← hg.induced] -- now `erw` after #13170 rfl -- `rfl` was not needed before #13170 -theorem embedding_prod_map {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : Embedding f) - (hg : Embedding g) : Embedding (Limits.prod.map f g) := +theorem isEmbedding_prodMap {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : IsEmbedding f) + (hg : IsEmbedding g) : IsEmbedding (Limits.prod.map f g) := ⟨inducing_prod_map hf.toInducing hg.toInducing, by haveI := (TopCat.mono_iff_injective _).mpr hf.inj haveI := (TopCat.mono_iff_injective _).mpr hg.inj exact (TopCat.mono_iff_injective _).mp inferInstance⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_prod_map := isEmbedding_prodMap + end Prod /-- The binary coproduct cofan in `TopCat`. -/ @@ -316,7 +319,7 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) : · revert h x apply (IsOpen.continuousOn_iff _).mp · rw [continuousOn_iff_continuous_restrict] - convert_to Continuous (f ∘ (Homeomorph.ofEmbedding _ h₁.toEmbedding).symm) + convert_to Continuous (f ∘ (Homeomorph.ofIsEmbedding _ h₁.isEmbedding).symm) · ext ⟨x, hx⟩ exact dif_pos hx apply Continuous.comp @@ -330,14 +333,14 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) : rintro a (h : a ∈ (Set.range c.inl)ᶜ) rwa [eq_compl_iff_isCompl.mpr h₃.symm] convert_to Continuous - (g ∘ (Homeomorph.ofEmbedding _ h₂.toEmbedding).symm ∘ Subtype.map _ this) + (g ∘ (Homeomorph.ofIsEmbedding _ h₂.isEmbedding).symm ∘ Subtype.map _ this) · ext ⟨x, hx⟩ exact dif_neg hx apply Continuous.comp · exact g.continuous_toFun · apply Continuous.comp · continuity - · rw [embedding_subtype_val.toInducing.continuous_iff] + · rw [IsEmbedding.subtypeVal.toInducing.continuous_iff] exact continuous_subtype_val · change IsOpen (Set.range c.inl)ᶜ rw [← eq_compl_iff_isCompl.mpr h₃.symm] diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index e51d68906803f..dc00c0849f936 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -161,7 +161,7 @@ theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : noncomputable def pullbackHomeoPreimage {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] - (f : X → Z) (hf : Continuous f) (g : Y → Z) (hg : Embedding g) : + (f : X → Z) (hf : Continuous f) (g : Y → Z) (hg : IsEmbedding g) : { p : X × Y // f p.1 = g p.2 } ≃ₜ f ⁻¹' Set.range g where toFun := fun x ↦ ⟨x.1.1, _, x.2.symm⟩ invFun := fun x ↦ ⟨⟨x.1, Exists.choose x.2⟩, (Exists.choose_spec x.2).symm⟩ @@ -186,10 +186,13 @@ theorem inducing_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Inducing <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) := ⟨by simp [topologicalSpace_coe, prod_topology, pullback_topology, induced_compose, ← coe_comp]⟩ -theorem embedding_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) : - Embedding <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) := +theorem isEmbedding_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) : + IsEmbedding <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) := ⟨inducing_pullback_to_prod f g, (TopCat.mono_iff_injective _).mp inferInstance⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_pullback_to_prod := isEmbedding_pullback_to_prod + /-- If the map `S ⟶ T` is mono, then there is a description of the image of `W ×ₛ X ⟶ Y ×ₜ Z`. -/ theorem range_pullback_map {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) [H₃ : Mono i₃] (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) @@ -258,20 +261,22 @@ W ⟶ Y X ⟶ Z ``` -/ -theorem pullback_map_embedding_of_embeddings {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) (f₂ : X ⟶ S) - (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Embedding i₁) (H₂ : Embedding i₂) - (i₃ : S ⟶ T) (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : - Embedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) := by - refine - embedding_of_embedding_compose (ContinuousMap.continuous_toFun _) - (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from +theorem pullback_map_isEmbedding {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) (f₂ : X ⟶ S) + (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : IsEmbedding i₁) + (H₂ : IsEmbedding i₂) (i₃ : S ⟶ T) (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : + IsEmbedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) := by + refine .of_comp (ContinuousMap.continuous_toFun _) + (show Continuous (prod.lift (pullback.fst g₁ g₂) (pullback.snd g₁ g₂)) from ContinuousMap.continuous_toFun _) ?_ suffices - Embedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by + IsEmbedding (prod.lift (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ≫ Limits.prod.map i₁ i₂) by simpa [← coe_comp] using this rw [coe_comp] - exact Embedding.comp (embedding_prod_map H₁ H₂) (embedding_pullback_to_prod _ _) + exact (isEmbedding_prodMap H₁ H₂).comp (isEmbedding_pullback_to_prod _ _) + +@[deprecated (since := "2024-10-26")] +alias pullback_map_embedding_of_embeddings := pullback_map_isEmbedding /-- If there is a diagram where the morphisms `W ⟶ Y` and `X ⟶ Z` are open embeddings, and `S ⟶ T` is mono, then the induced morphism `W ×ₛ X ⟶ Y ×ₜ Z` is also an open embedding. @@ -290,7 +295,7 @@ theorem pullback_map_isOpenEmbedding {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) : IsOpenEmbedding (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) := by constructor · apply - pullback_map_embedding_of_embeddings f₁ f₂ g₁ g₂ H₁.toEmbedding H₂.toEmbedding i₃ eq₁ eq₂ + pullback_map_isEmbedding f₁ f₂ g₁ g₂ H₁.isEmbedding H₂.isEmbedding i₃ eq₁ eq₂ · rw [range_pullback_map] apply IsOpen.inter <;> apply Continuous.isOpen_preimage · apply ContinuousMap.continuous_toFun @@ -301,28 +306,38 @@ theorem pullback_map_isOpenEmbedding {W X Y Z S T : TopCat.{u}} (f₁ : W ⟶ S) @[deprecated (since := "2024-10-18")] alias pullback_map_openEmbedding_of_open_embeddings := pullback_map_isOpenEmbedding -theorem snd_embedding_of_left_embedding {X Y S : TopCat} {f : X ⟶ S} (H : Embedding f) (g : Y ⟶ S) : - Embedding <| ⇑(pullback.snd f g) := by - convert (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).embedding.comp - (pullback_map_embedding_of_embeddings (i₂ := 𝟙 Y) - f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).embedding (𝟙 _) rfl (by simp)) + +lemma snd_isEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : IsEmbedding f) (g : Y ⟶ S) : + IsEmbedding <| ⇑(pullback.snd f g) := by + convert (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp + (pullback_map_isEmbedding (i₂ := 𝟙 Y) + f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding (𝟙 _) rfl (by simp)) erw [← coe_comp] simp -theorem fst_embedding_of_right_embedding {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} - (H : Embedding g) : Embedding <| ⇑(pullback.fst f g) := by - convert (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).embedding.comp - (pullback_map_embedding_of_embeddings (i₁ := 𝟙 X) - f g f (𝟙 _) (homeoOfIso (Iso.refl _)).embedding H (𝟙 _) rfl (by simp)) +@[deprecated (since := "2024-10-26")] +alias snd_embedding_of_left_embedding := snd_isEmbedding_of_left + +theorem fst_isEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} + (H : IsEmbedding g) : IsEmbedding <| ⇑(pullback.fst f g) := by + convert (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isEmbedding.comp + (pullback_map_isEmbedding (i₁ := 𝟙 X) + f g f (𝟙 _) (homeoOfIso (Iso.refl _)).isEmbedding H (𝟙 _) rfl (by simp)) erw [← coe_comp] simp -theorem embedding_of_pullback_embeddings {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : Embedding f) - (H₂ : Embedding g) : Embedding (limit.π (cospan f g) WalkingCospan.one) := by - convert H₂.comp (snd_embedding_of_left_embedding H₁ g) +@[deprecated (since := "2024-10-26")] +alias fst_embedding_of_right_embedding := fst_isEmbedding_of_right + +theorem isEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsEmbedding f) + (H₂ : IsEmbedding g) : IsEmbedding (limit.π (cospan f g) WalkingCospan.one) := by + convert H₂.comp (snd_isEmbedding_of_left H₁ g) rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr] rfl +@[deprecated (since := "2024-10-26")] +alias embedding_of_pullback_embeddings := isEmbedding_of_pullback + theorem snd_isOpenEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : IsOpenEmbedding f) (g : Y ⟶ S) : IsOpenEmbedding <| ⇑(pullback.snd f g) := by convert (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp @@ -357,10 +372,10 @@ theorem isOpenEmbedding_of_pullback_open_embeddings {X Y S : TopCat} {f : X ⟶ alias openEmbedding_of_pullback_open_embeddings := isOpenEmbedding_of_pullback_open_embeddings theorem fst_iso_of_right_embedding_range_subset {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} - (hg : Embedding g) (H : Set.range f ⊆ Set.range g) : + (hg : IsEmbedding g) (H : Set.range f ⊆ Set.range g) : IsIso (pullback.fst f g) := by let esto : (pullback f g : TopCat) ≃ₜ X := - (Homeomorph.ofEmbedding _ (fst_embedding_of_right_embedding f hg)).trans + (Homeomorph.ofIsEmbedding _ (fst_isEmbedding_of_right f hg)).trans { toFun := Subtype.val invFun := fun x => ⟨x, by @@ -370,10 +385,10 @@ theorem fst_iso_of_right_embedding_range_subset {X Y S : TopCat} (f : X ⟶ S) { right_inv := fun x => rfl } convert (isoOfHomeo esto).isIso_hom -theorem snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X ⟶ S} (hf : Embedding f) +theorem snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X ⟶ S} (hf : IsEmbedding f) (g : Y ⟶ S) (H : Set.range g ⊆ Set.range f) : IsIso (pullback.snd f g) := by let esto : (pullback f g : TopCat) ≃ₜ Y := - (Homeomorph.ofEmbedding _ (snd_embedding_of_left_embedding hf g)).trans + (Homeomorph.ofIsEmbedding _ (snd_isEmbedding_of_left hf g)).trans { toFun := Subtype.val invFun := fun x => ⟨x, by diff --git a/Mathlib/Topology/Category/TopCat/Opens.lean b/Mathlib/Topology/Category/TopCat/Opens.lean index de97a8d22ea44..bbb4a6f5369a9 100644 --- a/Mathlib/Topology/Category/TopCat/Opens.lean +++ b/Mathlib/Topology/Category/TopCat/Opens.lean @@ -99,9 +99,7 @@ realising each open set as a topological space itself. -/ def toTopCat (X : TopCat.{u}) : Opens X ⥤ TopCat where obj U := ⟨U, inferInstance⟩ - map i := - ⟨fun x => ⟨x.1, i.le x.2⟩, - (Embedding.continuous_iff embedding_subtype_val).2 continuous_induced_dom⟩ + map i := ⟨fun x ↦ ⟨x.1, i.le x.2⟩, IsEmbedding.subtypeVal.continuous_iff.2 continuous_induced_dom⟩ @[simp] theorem toTopCat_map (X : TopCat.{u}) {U V : Opens X} {f : U ⟶ V} {x} {h} : diff --git a/Mathlib/Topology/CompactOpen.lean b/Mathlib/Topology/CompactOpen.lean index 8f58dc36f0245..783763b6584eb 100644 --- a/Mathlib/Topology/CompactOpen.lean +++ b/Mathlib/Topology/CompactOpen.lean @@ -95,11 +95,14 @@ theorem inducing_postcomp (g : C(Y, Z)) (hg : Inducing g) : /-- If `g : C(Y, Z)` is a topological embedding, then the composition `ContinuousMap.comp g : C(X, Y) → C(X, Z)` is an embedding too. -/ -theorem embedding_postcomp (g : C(Y, Z)) (hg : Embedding g) : - Embedding (g.comp : C(X, Y) → C(X, Z)) := +theorem isEmbedding_postcomp (g : C(Y, Z)) (hg : IsEmbedding g) : + IsEmbedding (g.comp : C(X, Y) → C(X, Z)) := ⟨inducing_postcomp g hg.1, fun _ _ ↦ (cancel_left hg.2).1⟩ -@[deprecated (since := "2024-10-19")] alias embedding_comp := embedding_postcomp +@[deprecated (since := "2024-10-26")] +alias embedding_postcomp := isEmbedding_postcomp + +@[deprecated (since := "2024-10-19")] alias embedding_comp := isEmbedding_postcomp /-- `C(·, Z)` is a functor. -/ @[continuity, fun_prop] diff --git a/Mathlib/Topology/Compactification/OnePoint.lean b/Mathlib/Topology/Compactification/OnePoint.lean index dec6ca2d9e95f..71c9947f7a4fb 100644 --- a/Mathlib/Topology/Compactification/OnePoint.lean +++ b/Mathlib/Topology/Compactification/OnePoint.lean @@ -258,7 +258,7 @@ theorem nhds_coe_eq (x : X) : 𝓝 ↑x = map ((↑) : X → OnePoint X) (𝓝 x theorem nhdsWithin_coe_image (s : Set X) (x : X) : 𝓝[(↑) '' s] (x : OnePoint X) = map (↑) (𝓝[s] x) := - (isOpenEmbedding_coe.toEmbedding.map_nhdsWithin_eq _ _).symm + (isOpenEmbedding_coe.isEmbedding.map_nhdsWithin_eq _ _).symm theorem nhdsWithin_coe (s : Set (OnePoint X)) (x : X) : 𝓝[s] ↑x = map (↑) (𝓝[(↑) ⁻¹' s] x) := (isOpenEmbedding_coe.map_nhdsWithin_preimage_eq _ _).symm diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index 306e7735c660f..9cbaa2b845fd0 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/Mathlib/Topology/Compactness/Compact.lean @@ -908,9 +908,12 @@ theorem Inducing.isCompact_iff {f : X → Y} (hf : Inducing f) : /-- If `f : X → Y` is an `Embedding`, the image `f '' s` of a set `s` is compact if and only if `s` is compact. -/ -theorem Embedding.isCompact_iff {f : X → Y} (hf : Embedding f) : +theorem IsEmbedding.isCompact_iff {f : X → Y} (hf : IsEmbedding f) : IsCompact s ↔ IsCompact (f '' s) := hf.toInducing.isCompact_iff +@[deprecated (since := "2024-10-26")] +alias Embedding.isCompact_iff := IsEmbedding.isCompact_iff + /-- The preimage of a compact set under an inducing map is a compact set. -/ theorem Inducing.isCompact_preimage {f : X → Y} (hf : Inducing f) (hf' : IsClosed (range f)) {K : Set Y} (hK : IsCompact K) : IsCompact (f ⁻¹' K) := by @@ -947,7 +950,7 @@ alias ClosedEmbedding.tendsto_cocompact := IsClosedEmbedding.tendsto_cocompact /-- Sets of subtype are compact iff the image under a coercion is. -/ theorem Subtype.isCompact_iff {p : X → Prop} {s : Set { x // p x }} : IsCompact s ↔ IsCompact ((↑) '' s : Set X) := - embedding_subtype_val.isCompact_iff + IsEmbedding.subtypeVal.isCompact_iff theorem isCompact_iff_isCompact_univ : IsCompact s ↔ IsCompact (univ : Set s) := by rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe] diff --git a/Mathlib/Topology/Compactness/Lindelof.lean b/Mathlib/Topology/Compactness/Lindelof.lean index 9a5383d41086c..8097324686a4a 100644 --- a/Mathlib/Topology/Compactness/Lindelof.lean +++ b/Mathlib/Topology/Compactness/Lindelof.lean @@ -610,9 +610,12 @@ theorem Inducing.isLindelof_iff {f : X → Y} (hf : Inducing f) : /-- If `f : X → Y` is an `Embedding`, the image `f '' s` of a set `s` is Lindelöf if and only if `s` is Lindelöf. -/ -theorem Embedding.isLindelof_iff {f : X → Y} (hf : Embedding f) : +theorem IsEmbedding.isLindelof_iff {f : X → Y} (hf : IsEmbedding f) : IsLindelof s ↔ IsLindelof (f '' s) := hf.toInducing.isLindelof_iff +@[deprecated (since := "2024-10-26")] +alias Embedding.isLindelof_iff := IsEmbedding.isLindelof_iff + /-- The preimage of a Lindelöf set under an inducing map is a Lindelöf set. -/ theorem Inducing.isLindelof_preimage {f : X → Y} (hf : Inducing f) (hf' : IsClosed (range f)) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K) := by @@ -641,7 +644,7 @@ alias ClosedEmbedding.tendsto_coLindelof := IsClosedEmbedding.tendsto_coLindelof /-- Sets of subtype are Lindelöf iff the image under a coercion is. -/ theorem Subtype.isLindelof_iff {p : X → Prop} {s : Set { x // p x }} : IsLindelof s ↔ IsLindelof ((↑) '' s : Set X) := - embedding_subtype_val.isLindelof_iff + IsEmbedding.subtypeVal.isLindelof_iff theorem isLindelof_iff_isLindelof_univ : IsLindelof s ↔ IsLindelof (univ : Set s) := by rw [Subtype.isLindelof_iff, image_univ, Subtype.range_coe] diff --git a/Mathlib/Topology/Compactness/LocallyCompact.lean b/Mathlib/Topology/Compactness/LocallyCompact.lean index f479bd3f6e859..b0356d7148b65 100644 --- a/Mathlib/Topology/Compactness/LocallyCompact.lean +++ b/Mathlib/Topology/Compactness/LocallyCompact.lean @@ -214,7 +214,7 @@ alias OpenEmbedding.locallyCompactSpace := IsOpenEmbedding.locallyCompactSpace protected theorem IsLocallyClosed.locallyCompactSpace [LocallyCompactSpace X] {s : Set X} (hs : IsLocallyClosed s) : LocallyCompactSpace s := - embedding_subtype_val.locallyCompactSpace <| by rwa [Subtype.range_val] + IsEmbedding.subtypeVal.locallyCompactSpace <| by rwa [Subtype.range_val] protected theorem IsClosed.locallyCompactSpace [LocallyCompactSpace X] {s : Set X} (hs : IsClosed s) : LocallyCompactSpace s := diff --git a/Mathlib/Topology/Compactness/SigmaCompact.lean b/Mathlib/Topology/Compactness/SigmaCompact.lean index 9718f4ea99c27..c03033f26d87a 100644 --- a/Mathlib/Topology/Compactness/SigmaCompact.lean +++ b/Mathlib/Topology/Compactness/SigmaCompact.lean @@ -120,14 +120,17 @@ lemma Inducing.isSigmaCompact_iff {f : X → Y} {s : Set X} /-- If `f : X → Y` is an `Embedding`, the image `f '' s` of a set `s` is σ-compact if and only `s` is σ-compact. -/ -lemma Embedding.isSigmaCompact_iff {f : X → Y} {s : Set X} - (hf : Embedding f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s) := +lemma IsEmbedding.isSigmaCompact_iff {f : X → Y} {s : Set X} + (hf : IsEmbedding f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s) := hf.toInducing.isSigmaCompact_iff +@[deprecated (since := "2024-10-26")] +alias Embedding.isSigmaCompact_iff := IsEmbedding.isSigmaCompact_iff + /-- Sets of subtype are σ-compact iff the image under a coercion is. -/ lemma Subtype.isSigmaCompact_iff {p : X → Prop} {s : Set { a // p a }} : IsSigmaCompact s ↔ IsSigmaCompact ((↑) '' s : Set X) := - embedding_subtype_val.isSigmaCompact_iff + IsEmbedding.subtypeVal.isSigmaCompact_iff /-- A σ-compact space is a space that is the union of a countable collection of compact subspaces. Note that a locally compact separable T₂ space need not be σ-compact. diff --git a/Mathlib/Topology/Connected/Clopen.lean b/Mathlib/Topology/Connected/Clopen.lean index 4a2541134dba0..205522d936fa0 100644 --- a/Mathlib/Topology/Connected/Clopen.lean +++ b/Mathlib/Topology/Connected/Clopen.lean @@ -99,7 +99,7 @@ theorem Continuous.exists_lift_sigma [ConnectedSpace α] [∀ i, TopologicalSpac exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩ rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩ refine ⟨i, g, ?_, rfl⟩ - rwa [← embedding_sigmaMk.continuous_iff] at hf + rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf theorem nonempty_inter [PreconnectedSpace α] {s t : Set α} : IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty := by diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index 78fdd9f07db9d..598a066f3d205 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -141,25 +141,34 @@ theorem isTotallyDisconnected_of_image [TopologicalSpace β] {f : α → β} (hf h _ (image_subset f hts) (ht.image f <| hf.mono hts) (mem_image_of_mem f x_in) (mem_image_of_mem f y_in) -theorem Embedding.isTotallyDisconnected [TopologicalSpace β] {f : α → β} (hf : Embedding f) - {s : Set α} (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := +lemma IsEmbedding.isTotallyDisconnected [TopologicalSpace β] {f : α → β} {s : Set α} + (hf : IsEmbedding f) (h : IsTotallyDisconnected (f '' s)) : IsTotallyDisconnected s := isTotallyDisconnected_of_image hf.continuous.continuousOn hf.inj h -lemma Embedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} (hf : Embedding f) - {s : Set α} : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s := by +@[deprecated (since := "2024-10-26")] +alias Embedding.isTotallyDisconnected := IsEmbedding.isTotallyDisconnected + +lemma IsEmbedding.isTotallyDisconnected_image [TopologicalSpace β] {f : α → β} {s : Set α} + (hf : IsEmbedding f) : IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s := by refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩ obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u := ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩ rw [hf.toInducing.isPreconnected_image] at hu exact (hs v hvs hu).image _ -lemma Embedding.isTotallyDisconnected_range [TopologicalSpace β] {f : α → β} (hf : Embedding f) : - IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α := by +@[deprecated (since := "2024-10-26")] +alias Embedding.isTotallyDisconnected_image := IsEmbedding.isTotallyDisconnected_image + +lemma IsEmbedding.isTotallyDisconnected_range [TopologicalSpace β] {f : α → β} + (hf : IsEmbedding f) : IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α := by rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image] +@[deprecated (since := "2024-10-26")] +alias Embedding.isTotallyDisconnected_range := IsEmbedding.isTotallyDisconnected_range + lemma totallyDisconnectedSpace_subtype_iff {s : Set α} : TotallyDisconnectedSpace s ↔ IsTotallyDisconnected s := by - rw [← embedding_subtype_val.isTotallyDisconnected_range, Subtype.range_val] + rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val] instance Subtype.totallyDisconnectedSpace {α : Type*} {p : α → Prop} [TopologicalSpace α] [TotallyDisconnectedSpace α] : TotallyDisconnectedSpace (Subtype p) := diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index c2dffe31a13df..cc95ce3be1b2f 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -813,11 +813,14 @@ theorem inducing_prod_const {y : Y} {f : X → Z} : (Inducing fun x => (f x, y)) simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp_def, induced_const, inf_top_eq] -theorem Embedding.prodMap {f : X → Y} {g : Z → W} (hf : Embedding f) (hg : Embedding g) : - Embedding (Prod.map f g) := +theorem IsEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsEmbedding f) (hg : IsEmbedding g) : + IsEmbedding (Prod.map f g) := { hf.toInducing.prodMap hg.toInducing with inj := fun ⟨x₁, z₁⟩ ⟨x₂, z₂⟩ => by simp [hf.inj.eq_iff, hg.inj.eq_iff] } +@[deprecated (since := "2024-10-26")] +alias Embedding.prodMap := IsEmbedding.prodMap + @[deprecated (since := "2024-10-05")] alias Embedding.prod_map := Embedding.prodMap protected theorem IsOpenMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : @@ -831,18 +834,24 @@ protected theorem IsOpenMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap protected theorem IsOpenEmbedding.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) : IsOpenEmbedding (Prod.map f g) := - isOpenEmbedding_of_embedding_open (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap) + .of_isEmbedding_isOpenMap (hf.1.prodMap hg.1) (hf.isOpenMap.prodMap hg.isOpenMap) @[deprecated (since := "2024-10-18")] alias OpenEmbedding.prodMap := IsOpenEmbedding.prodMap @[deprecated (since := "2024-10-05")] alias IsOpenEmbedding.prod := IsOpenEmbedding.prodMap -theorem embedding_graph {f : X → Y} (hf : Continuous f) : Embedding fun x => (x, f x) := - embedding_of_embedding_compose (continuous_id.prod_mk hf) continuous_fst embedding_id +lemma isEmbedding_graph {f : X → Y} (hf : Continuous f) : IsEmbedding fun x => (x, f x) := + .of_comp (continuous_id.prod_mk hf) continuous_fst .id + +@[deprecated (since := "2024-10-26")] +alias embedding_graph := isEmbedding_graph + +lemma isEmbedding_prodMk (x : X) : IsEmbedding (Prod.mk x : Y → X × Y) := + .of_comp (Continuous.Prod.mk x) continuous_snd .id -theorem embedding_prod_mk (x : X) : Embedding (Prod.mk x : Y → X × Y) := - embedding_of_embedding_compose (Continuous.Prod.mk x) continuous_snd embedding_id +@[deprecated (since := "2024-10-26")] +alias embedding_prod_mk := isEmbedding_prodMk theorem IsOpenQuotientMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g) := @@ -923,11 +932,11 @@ theorem isOpenEmbedding_inr : IsOpenEmbedding (@inr X Y) := @[deprecated (since := "2024-10-18")] alias openEmbedding_inr := isOpenEmbedding_inr -theorem embedding_inl : Embedding (@inl X Y) := - isOpenEmbedding_inl.1 +protected lemma IsEmbedding.inl : IsEmbedding (@inl X Y) := isOpenEmbedding_inl.1 +protected lemma IsEmbedding.inr : IsEmbedding (@inr X Y) := isOpenEmbedding_inr.1 -theorem embedding_inr : Embedding (@inr X Y) := - isOpenEmbedding_inr.1 +@[deprecated (since := "2024-10-26")] +alias embedding_inr := IsEmbedding.inr theorem isOpen_range_inl : IsOpen (range (inl : X → X ⊕ Y)) := isOpenEmbedding_inl.2 @@ -944,13 +953,13 @@ theorem isClosed_range_inr : IsClosed (range (inr : Y → X ⊕ Y)) := by exact isOpen_range_inl theorem isClosedEmbedding_inl : IsClosedEmbedding (inl : X → X ⊕ Y) := - ⟨embedding_inl, isClosed_range_inl⟩ + ⟨.inl, isClosed_range_inl⟩ @[deprecated (since := "2024-10-20")] alias closedEmbedding_inl := isClosedEmbedding_inl theorem isClosedEmbedding_inr : IsClosedEmbedding (inr : Y → X ⊕ Y) := - ⟨embedding_inr, isClosed_range_inr⟩ + ⟨.inr, isClosed_range_inr⟩ @[deprecated (since := "2024-10-20")] alias closedEmbedding_inr := isClosedEmbedding_inr @@ -965,7 +974,7 @@ theorem nhds_inr (y : Y) : 𝓝 (inr y : X ⊕ Y) = map inr (𝓝 y) := theorem continuous_sum_map {f : X → Y} {g : Z → W} : Continuous (Sum.map f g) ↔ Continuous f ∧ Continuous g := continuous_sum_elim.trans <| - embedding_inl.continuous_iff.symm.and embedding_inr.continuous_iff.symm + IsEmbedding.inl.continuous_iff.symm.and IsEmbedding.inr.continuous_iff.symm @[continuity, fun_prop] theorem Continuous.sum_map {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) : @@ -1012,12 +1021,15 @@ theorem Inducing.of_codRestrict {f : X → Y} {t : Set Y} (ht : ∀ x, f x ∈ t (h : Inducing (t.codRestrict f ht)) : Inducing f := inducing_subtype_val.comp h -theorem embedding_subtype_val : Embedding ((↑) : Subtype p → X) := +lemma IsEmbedding.subtypeVal : IsEmbedding ((↑) : Subtype p → X) := ⟨inducing_subtype_val, Subtype.coe_injective⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_subtype_val := IsEmbedding.subtypeVal + theorem IsClosedEmbedding.subtypeVal (h : IsClosed {a | p a}) : IsClosedEmbedding ((↑) : Subtype p → X) := - ⟨embedding_subtype_val, by rwa [Subtype.range_coe_subtype]⟩ + ⟨.subtypeVal, by rwa [Subtype.range_coe_subtype]⟩ @[deprecated (since := "2024-10-20")] alias closedEmbedding_subtype_val := IsClosedEmbedding.subtypeVal @@ -1032,7 +1044,7 @@ theorem Continuous.subtype_val {f : Y → Subtype p} (hf : Continuous f) : theorem IsOpen.isOpenEmbedding_subtypeVal {s : Set X} (hs : IsOpen s) : IsOpenEmbedding ((↑) : s → X) := - ⟨embedding_subtype_val, (@Subtype.range_coe _ s).symm ▸ hs⟩ + ⟨.subtypeVal, (@Subtype.range_coe _ s).symm ▸ hs⟩ @[deprecated (since := "2024-10-18")] alias IsOpen.openEmbedding_subtype_val := IsOpen.isOpenEmbedding_subtypeVal @@ -1126,18 +1138,24 @@ theorem Inducing.codRestrict {e : X → Y} (he : Inducing e) {s : Set Y} (hs : Inducing (codRestrict e s hs) := inducing_of_inducing_compose (he.continuous.codRestrict hs) continuous_subtype_val he -theorem Embedding.codRestrict {e : X → Y} (he : Embedding e) (s : Set Y) (hs : ∀ x, e x ∈ s) : - Embedding (codRestrict e s hs) := - embedding_of_embedding_compose (he.continuous.codRestrict hs) continuous_subtype_val he +protected lemma IsEmbedding.codRestrict {e : X → Y} (he : IsEmbedding e) (s : Set Y) + (hs : ∀ x, e x ∈ s) : IsEmbedding (codRestrict e s hs) := + he.of_comp (he.continuous.codRestrict hs) continuous_subtype_val + +@[deprecated (since := "2024-10-26")] +alias Embedding.codRestrict := IsEmbedding.codRestrict -theorem embedding_inclusion {s t : Set X} (h : s ⊆ t) : Embedding (inclusion h) := - embedding_subtype_val.codRestrict _ _ +protected lemma IsEmbedding.inclusion {s t : Set X} (h : s ⊆ t) : + IsEmbedding (inclusion h) := IsEmbedding.subtypeVal.codRestrict _ _ + +@[deprecated (since := "2024-10-26")] +alias embedding_inclusion := IsEmbedding.inclusion /-- Let `s, t ⊆ X` be two subsets of a topological space `X`. If `t ⊆ s` and the topology induced by `X`on `s` is discrete, then also the topology induces on `t` is discrete. -/ theorem DiscreteTopology.of_subset {X : Type*} [TopologicalSpace X] {s t : Set X} (_ : DiscreteTopology s) (ts : t ⊆ s) : DiscreteTopology t := - (embedding_inclusion ts).discreteTopology + (IsEmbedding.inclusion ts).discreteTopology /-- Let `s` be a discrete subset of a topological space. Then the preimage of `s` by a continuous injective map is also discrete. -/ @@ -1161,7 +1179,7 @@ alias QuotientMap.restrictPreimage_isOpen := IsQuotientMap.restrictPreimage_isOp open scoped Set.Notation in lemma isClosed_preimage_val {s t : Set X} : IsClosed (s ↓∩ t) ↔ s ∩ closure (s ∩ t) ⊆ t := by - rw [← closure_eq_iff_isClosed, embedding_subtype_val.closure_eq_preimage_closure_image, + rw [← closure_eq_iff_isClosed, IsEmbedding.subtypeVal.closure_eq_preimage_closure_image, ← Subtype.val_injective.image_injective.eq_iff, Subtype.image_preimage_coe, Subtype.image_preimage_coe, subset_antisymm_iff, and_iff_left, Set.subset_inter_iff, and_iff_right] @@ -1580,9 +1598,12 @@ theorem isClosedEmbedding_sigmaMk {i : ι} : IsClosedEmbedding (@Sigma.mk ι σ @[deprecated (since := "2024-10-20")] alias closedEmbedding_sigmaMk := isClosedEmbedding_sigmaMk -theorem embedding_sigmaMk {i : ι} : Embedding (@Sigma.mk ι σ i) := +lemma IsEmbedding.sigmaMk {i : ι} : IsEmbedding (@Sigma.mk ι σ i) := isClosedEmbedding_sigmaMk.1 +@[deprecated (since := "2024-10-26")] +alias embedding_sigmaMk := IsEmbedding.sigmaMk + theorem Sigma.nhds_mk (i : ι) (x : σ i) : 𝓝 (⟨i, x⟩ : Sigma σ) = Filter.map (Sigma.mk i) (𝓝 x) := (isOpenEmbedding_sigmaMk.map_nhds_eq x).symm @@ -1591,7 +1612,7 @@ theorem Sigma.nhds_eq (x : Sigma σ) : 𝓝 x = Filter.map (Sigma.mk x.1) (𝓝 apply Sigma.nhds_mk theorem comap_sigmaMk_nhds (i : ι) (x : σ i) : comap (Sigma.mk i) (𝓝 ⟨i, x⟩) = 𝓝 x := - (embedding_sigmaMk.nhds_eq_comap _).symm + (IsEmbedding.sigmaMk.nhds_eq_comap _).symm theorem isOpen_sigma_fst_preimage (s : Set ι) : IsOpen (Sigma.fst ⁻¹' s : Set (Σ a, σ a)) := by rw [← biUnion_of_singleton s, preimage_iUnion₂] @@ -1618,7 +1639,7 @@ component under `f` can be separated from the images of all other components by theorem inducing_sigma {f : Sigma σ → X} : Inducing f ↔ (∀ i, Inducing (f ∘ Sigma.mk i)) ∧ (∀ i, ∃ U, IsOpen U ∧ ∀ x, f x ∈ U ↔ x.1 = i) := by - refine ⟨fun h ↦ ⟨fun i ↦ h.comp embedding_sigmaMk.1, fun i ↦ ?_⟩, ?_⟩ + refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩ · rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩ refine ⟨U, hUo, ?_⟩ simpa [Set.ext_iff] using hU @@ -1631,7 +1652,8 @@ theorem inducing_sigma {f : Sigma σ → X} : @[simp 1100] theorem continuous_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} : Continuous (Sigma.map f₁ f₂) ↔ ∀ i, Continuous (f₂ i) := - continuous_sigma_iff.trans <| by simp only [Sigma.map, embedding_sigmaMk.continuous_iff, comp_def] + continuous_sigma_iff.trans <| by + simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def] @[continuity, fun_prop] theorem Continuous.sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (hf : ∀ i, Continuous (f₂ i)) : @@ -1651,13 +1673,17 @@ theorem inducing_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i simp only [inducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk, ← map_sigma_mk_comap h₁, map_inj sigma_mk_injective] -theorem embedding_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h : Injective f₁) : - Embedding (Sigma.map f₁ f₂) ↔ ∀ i, Embedding (f₂ i) := by - simp only [embedding_iff, Injective.sigma_map, inducing_sigma_map h, forall_and, h.sigma_map_iff] +lemma isEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} + (h : Injective f₁) : IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsEmbedding (f₂ i) := by + simp only [isEmbedding_iff, Injective.sigma_map, inducing_sigma_map h, forall_and, + h.sigma_map_iff] + +@[deprecated (since := "2024-10-26")] +alias embedding_sigma_map := isEmbedding_sigmaMap theorem isOpenEmbedding_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h : Injective f₁) : IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsOpenEmbedding (f₂ i) := by - simp only [isOpenEmbedding_iff_embedding_open, isOpenMap_sigma_map, embedding_sigma_map h, + simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isOpenMap_sigma_map, isEmbedding_sigmaMap h, forall_and] @[deprecated (since := "2024-10-18")] @@ -1683,18 +1709,21 @@ theorem continuous_uLift_down [TopologicalSpace X] : Continuous (ULift.down : UL theorem continuous_uLift_up [TopologicalSpace X] : Continuous (ULift.up : X → ULift.{v, u} X) := continuous_induced_rng.2 continuous_id -theorem embedding_uLift_down [TopologicalSpace X] : Embedding (ULift.down : ULift.{v, u} X → X) := - ⟨⟨rfl⟩, ULift.down_injective⟩ +lemma IsEmbedding.uliftDown [TopologicalSpace X] : + IsEmbedding (ULift.down : ULift.{v, u} X → X) := ⟨⟨rfl⟩, ULift.down_injective⟩ + +@[deprecated (since := "2024-10-26")] +alias embedding_uLift_down := IsEmbedding.uliftDown theorem ULift.isClosedEmbedding_down [TopologicalSpace X] : IsClosedEmbedding (ULift.down : ULift.{v, u} X → X) := - ⟨embedding_uLift_down, by simp only [ULift.down_surjective.range_eq, isClosed_univ]⟩ + ⟨.uliftDown, by simp only [ULift.down_surjective.range_eq, isClosed_univ]⟩ @[deprecated (since := "2024-10-20")] alias ULift.closedEmbedding_down := ULift.isClosedEmbedding_down instance [TopologicalSpace X] [DiscreteTopology X] : DiscreteTopology (ULift X) := - embedding_uLift_down.discreteTopology + IsEmbedding.uliftDown.discreteTopology end ULift diff --git a/Mathlib/Topology/ContinuousMap/Bounded.lean b/Mathlib/Topology/ContinuousMap/Bounded.lean index c85a6b15c3a3a..f8d8e66ebbdba 100644 --- a/Mathlib/Topology/ContinuousMap/Bounded.lean +++ b/Mathlib/Topology/ContinuousMap/Bounded.lean @@ -246,10 +246,13 @@ theorem inducing_coeFn : Inducing (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) UniformFun.tendsto_iff_tendstoUniformly] simp [comp_def] --- TODO: upgrade to a `IsUniformEmbedding` -theorem embedding_coeFn : Embedding (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) → α →ᵤ β) := +-- TODO: upgrade to `IsUniformEmbedding` +theorem isEmbedding_coeFn : IsEmbedding (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) → α →ᵤ β) := ⟨inducing_coeFn, fun _ _ h => ext fun x => congr_fun h x⟩ +@[deprecated (since := "2024-10-26")] +alias embedding_coeFn := isEmbedding_coeFn + variable (α) /-- Constant as a continuous bounded function. -/ diff --git a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean index 6bb261df3d76d..f4796c7e9350c 100644 --- a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean +++ b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean @@ -80,27 +80,30 @@ lemma le_def [PartialOrder R] (f g : C(X, R)₀) : f ≤ g ↔ ∀ x, f x ≤ g protected instance instTopologicalSpace : TopologicalSpace C(X, R)₀ := TopologicalSpace.induced ((↑) : C(X, R)₀ → C(X, R)) inferInstance -lemma embedding_toContinuousMap : Embedding ((↑) : C(X, R)₀ → C(X, R)) where +lemma isEmbedding_toContinuousMap : IsEmbedding ((↑) : C(X, R)₀ → C(X, R)) where induced := rfl inj _ _ h := ext fun x ↦ congr($(h) x) -instance [T0Space R] : T0Space C(X, R)₀ := embedding_toContinuousMap.t0Space -instance [R0Space R] : R0Space C(X, R)₀ := embedding_toContinuousMap.r0Space -instance [T1Space R] : T1Space C(X, R)₀ := embedding_toContinuousMap.t1Space -instance [R1Space R] : R1Space C(X, R)₀ := embedding_toContinuousMap.r1Space -instance [T2Space R] : T2Space C(X, R)₀ := embedding_toContinuousMap.t2Space -instance [RegularSpace R] : RegularSpace C(X, R)₀ := embedding_toContinuousMap.regularSpace -instance [T3Space R] : T3Space C(X, R)₀ := embedding_toContinuousMap.t3Space +@[deprecated (since := "2024-10-26")] +alias embedding_toContinuousMap := isEmbedding_toContinuousMap + +instance [T0Space R] : T0Space C(X, R)₀ := isEmbedding_toContinuousMap.t0Space +instance [R0Space R] : R0Space C(X, R)₀ := isEmbedding_toContinuousMap.r0Space +instance [T1Space R] : T1Space C(X, R)₀ := isEmbedding_toContinuousMap.t1Space +instance [R1Space R] : R1Space C(X, R)₀ := isEmbedding_toContinuousMap.r1Space +instance [T2Space R] : T2Space C(X, R)₀ := isEmbedding_toContinuousMap.t2Space +instance [RegularSpace R] : RegularSpace C(X, R)₀ := isEmbedding_toContinuousMap.regularSpace +instance [T3Space R] : T3Space C(X, R)₀ := isEmbedding_toContinuousMap.t3Space instance instContinuousEvalConst : ContinuousEvalConst C(X, R)₀ X R := - .of_continuous_forget embedding_toContinuousMap.continuous + .of_continuous_forget isEmbedding_toContinuousMap.continuous instance instContinuousEval [LocallyCompactPair X R] : ContinuousEval C(X, R)₀ X R := - .of_continuous_forget embedding_toContinuousMap.continuous + .of_continuous_forget isEmbedding_toContinuousMap.continuous lemma isClosedEmbedding_toContinuousMap [T1Space R] : IsClosedEmbedding ((↑) : C(X, R)₀ → C(X, R)) where - toEmbedding := embedding_toContinuousMap + toIsEmbedding := isEmbedding_toContinuousMap isClosed_range := by rw [range_toContinuousMap] exact isClosed_singleton.preimage <| continuous_eval_const 0 diff --git a/Mathlib/Topology/ContinuousMap/Sigma.lean b/Mathlib/Topology/ContinuousMap/Sigma.lean index f205d452cbc48..2327ac617f9c0 100644 --- a/Mathlib/Topology/ContinuousMap/Sigma.lean +++ b/Mathlib/Topology/ContinuousMap/Sigma.lean @@ -41,10 +41,10 @@ variable {X ι : Type*} {Y : ι → Type*} [TopologicalSpace X] [∀ i, Topologi namespace ContinuousMap -theorem embedding_sigmaMk_comp [Nonempty X] : - Embedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where +theorem isEmbedding_sigmaMk_comp [Nonempty X] : + IsEmbedding (fun g : Σ i, C(X, Y i) ↦ (sigmaMk g.1).comp g.2) where toInducing := inducing_sigma.2 - ⟨fun i ↦ (sigmaMk i).inducing_postcomp embedding_sigmaMk.toInducing, fun i ↦ + ⟨fun i ↦ (sigmaMk i).inducing_postcomp IsEmbedding.sigmaMk.toInducing, fun i ↦ let ⟨x⟩ := ‹Nonempty X› ⟨_, (isOpen_sigma_fst_preimage {i}).preimage (continuous_eval_const x), fun _ ↦ Iff.rfl⟩⟩ inj := by @@ -53,6 +53,9 @@ theorem embedding_sigmaMk_comp [Nonempty X] : Function.eq_of_sigmaMk_comp <| congr_arg DFunLike.coe h simpa using hg +@[deprecated (since := "2024-10-26")] +alias embedding_sigmaMk_comp := isEmbedding_sigmaMk_comp + section ConnectedSpace variable [ConnectedSpace X] @@ -76,9 +79,9 @@ The inverse map sends `⟨i, g⟩` to `ContinuousMap.comp (ContinuousMap.sigmaMk @[simps! symm_apply] def sigmaCodHomeomorph : C(X, Σ i, Y i) ≃ₜ Σ i, C(X, Y i) := .symm <| Equiv.toHomeomorphOfInducing - (.ofBijective _ ⟨embedding_sigmaMk_comp.inj, fun f ↦ + (.ofBijective _ ⟨isEmbedding_sigmaMk_comp.inj, fun f ↦ let ⟨i, g, hg⟩ := f.exists_lift_sigma; ⟨⟨i, g⟩, hg.symm⟩⟩) - embedding_sigmaMk_comp.toInducing + isEmbedding_sigmaMk_comp.toInducing end ConnectedSpace diff --git a/Mathlib/Topology/ContinuousMap/T0Sierpinski.lean b/Mathlib/Topology/ContinuousMap/T0Sierpinski.lean index 4e9903ccc7400..29abc7cb18c43 100644 --- a/Mathlib/Topology/ContinuousMap/T0Sierpinski.lean +++ b/Mathlib/Topology/ContinuousMap/T0Sierpinski.lean @@ -52,7 +52,10 @@ theorem productOfMemOpens_injective [T0Space X] : Function.Injective (productOfM apply Inseparable.eq rw [← Inducing.inseparable_iff (productOfMemOpens_inducing X), h] -theorem productOfMemOpens_embedding [T0Space X] : Embedding (productOfMemOpens X) := - Embedding.mk (productOfMemOpens_inducing X) (productOfMemOpens_injective X) +theorem productOfMemOpens_isEmbedding [T0Space X] : IsEmbedding (productOfMemOpens X) := + .mk (productOfMemOpens_inducing X) (productOfMemOpens_injective X) + +@[deprecated (since := "2024-10-26")] +alias productOfMemOpens_embedding := productOfMemOpens_isEmbedding end TopologicalSpace diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index b9e11fa1067f8..bd1b996919bf8 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/Mathlib/Topology/ContinuousOn.lean @@ -1103,18 +1103,24 @@ theorem Inducing.continuousOn_iff {f : α → β} {g : β → γ} (hg : Inducing ContinuousOn f s ↔ ContinuousOn (g ∘ f) s := by simp_rw [ContinuousOn, hg.continuousWithinAt_iff] -theorem Embedding.continuousOn_iff {f : α → β} {g : β → γ} (hg : Embedding g) {s : Set α} : - ContinuousOn f s ↔ ContinuousOn (g ∘ f) s := +lemma IsEmbedding.continuousOn_iff {f : α → β} {g : β → γ} (hg : IsEmbedding g) + {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s := Inducing.continuousOn_iff hg.1 -theorem Embedding.map_nhdsWithin_eq {f : α → β} (hf : Embedding f) (s : Set α) (x : α) : +@[deprecated (since := "2024-10-26")] +alias Embedding.continuousOn_iff := IsEmbedding.continuousOn_iff + +lemma IsEmbedding.map_nhdsWithin_eq {f : α → β} (hf : IsEmbedding f) (s : Set α) (x : α) : map f (𝓝[s] x) = 𝓝[f '' s] f x := by rw [nhdsWithin, Filter.map_inf hf.inj, hf.map_nhds_eq, map_principal, ← nhdsWithin_inter', inter_eq_self_of_subset_right (image_subset_range _ _)] +@[deprecated (since := "2024-10-26")] +alias Embedding.map_nhdsWithin_eq := IsEmbedding.map_nhdsWithin_eq + theorem IsOpenEmbedding.map_nhdsWithin_preimage_eq {f : α → β} (hf : IsOpenEmbedding f) (s : Set β) (x : α) : map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x := by - rw [hf.toEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range] + rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range] apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.isOpen_range rw [inter_assoc, inter_self] diff --git a/Mathlib/Topology/Covering.lean b/Mathlib/Topology/Covering.lean index 10e634e668440..855b4d06fbde2 100644 --- a/Mathlib/Topology/Covering.lean +++ b/Mathlib/Topology/Covering.lean @@ -63,7 +63,7 @@ theorem to_isEvenlyCovered_preimage {x : X} {I : Type*} [TopologicalSpace I] (h : IsEvenlyCovered f x I) : IsEvenlyCovered f x (f ⁻¹' {x}) := let ⟨_, h2⟩ := h ⟨((Classical.choose h2).preimageSingletonHomeomorph - (Classical.choose_spec h2)).embedding.discreteTopology, + (Classical.choose_spec h2)).isEmbedding.discreteTopology, _, h.mem_toTrivialization_baseSet⟩ end IsEvenlyCovered diff --git a/Mathlib/Topology/Defs/Induced.lean b/Mathlib/Topology/Defs/Induced.lean index e76112cfb337f..d21ee2180992a 100644 --- a/Mathlib/Topology/Defs/Induced.lean +++ b/Mathlib/Topology/Defs/Induced.lean @@ -105,14 +105,16 @@ structure Inducing (f : X → Y) : Prop where /-- A function between topological spaces is an embedding if it is injective, and for all `s : Set X`, `s` is open iff it is the preimage of an open set. -/ @[mk_iff] -structure Embedding [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) extends - Inducing f : Prop where +structure IsEmbedding (f : X → Y) extends Inducing f : Prop where /-- A topological embedding is injective. -/ inj : Function.Injective f +@[deprecated (since := "2024-10-26")] +alias Embedding := IsEmbedding + /-- An open embedding is an embedding with open range. -/ @[mk_iff] -structure IsOpenEmbedding (f : X → Y) extends Embedding f : Prop where +structure IsOpenEmbedding (f : X → Y) extends IsEmbedding f : Prop where /-- The range of an open embedding is an open set. -/ isOpen_range : IsOpen <| range f @@ -121,7 +123,7 @@ alias OpenEmbedding := IsOpenEmbedding /-- A closed embedding is an embedding with closed image. -/ @[mk_iff] -structure IsClosedEmbedding (f : X → Y) extends Embedding f : Prop where +structure IsClosedEmbedding (f : X → Y) extends IsEmbedding f : Prop where /-- The range of a closed embedding is a closed set. -/ isClosed_range : IsClosed <| range f diff --git a/Mathlib/Topology/DenseEmbedding.lean b/Mathlib/Topology/DenseEmbedding.lean index f42b8f1149a17..f129bedfccb82 100644 --- a/Mathlib/Topology/DenseEmbedding.lean +++ b/Mathlib/Topology/DenseEmbedding.lean @@ -228,9 +228,10 @@ variable {e : α → β} theorem inj_iff (de : IsDenseEmbedding e) {x y} : e x = e y ↔ x = y := de.inj.eq_iff -theorem to_embedding (de : IsDenseEmbedding e) : Embedding e := - { induced := de.induced - inj := de.inj } +theorem isEmbedding (de : IsDenseEmbedding e) : IsEmbedding e where __ := de + +@[deprecated (since := "2024-10-26")] +alias to_embedding := isEmbedding /-- If the domain of a `IsDenseEmbedding` is a separable space, then so is its codomain. -/ protected theorem separableSpace [SeparableSpace α] (de : IsDenseEmbedding e) : SeparableSpace β := @@ -267,7 +268,7 @@ theorem dense_image (de : IsDenseEmbedding e) {s : Set α} : Dense (e '' s) ↔ de.toIsDenseInducing.dense_image protected lemma id {α : Type*} [TopologicalSpace α] : IsDenseEmbedding (id : α → α) := - { embedding_id with dense := denseRange_id } + { IsEmbedding.id with dense := denseRange_id } end IsDenseEmbedding @@ -276,7 +277,7 @@ alias denseEmbedding_id := IsDenseEmbedding.id theorem Dense.isDenseEmbedding_val [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseEmbedding ((↑) : s → α) := - { embedding_subtype_val with dense := hs.denseRange_val } + { IsEmbedding.subtypeVal with dense := hs.denseRange_val } @[deprecated (since := "2024-09-30")] alias Dense.denseEmbedding_val := Dense.isDenseEmbedding_val diff --git a/Mathlib/Topology/FiberBundle/Basic.lean b/Mathlib/Topology/FiberBundle/Basic.lean index 275daa23c07b7..0dd775389ba18 100644 --- a/Mathlib/Topology/FiberBundle/Basic.lean +++ b/Mathlib/Topology/FiberBundle/Basic.lean @@ -261,12 +261,15 @@ alias quotientMap_proj := isQuotientMap_proj theorem continuous_totalSpaceMk (x : B) : Continuous (@TotalSpace.mk B F E x) := (totalSpaceMk_inducing F E x).continuous -theorem totalSpaceMk_embedding (x : B) : Embedding (@TotalSpace.mk B F E x) := +theorem totalSpaceMk_isEmbedding (x : B) : IsEmbedding (@TotalSpace.mk B F E x) := ⟨totalSpaceMk_inducing F E x, TotalSpace.mk_injective x⟩ +@[deprecated (since := "2024-10-26")] +alias totalSpaceMk_embedding := totalSpaceMk_isEmbedding + theorem totalSpaceMk_isClosedEmbedding [T1Space B] (x : B) : IsClosedEmbedding (@TotalSpace.mk B F E x) := - ⟨totalSpaceMk_embedding F E x, by + ⟨totalSpaceMk_isEmbedding F E x, by rw [TotalSpace.range_mk] exact isClosed_singleton.preimage <| continuous_proj F E⟩ @@ -680,7 +683,7 @@ instance fiberBundle : FiberBundle F Z.Fiber where rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf, comap_principal, comap_comap] simp only [Function.comp_def, localTrivAt_apply_mk, Trivialization.coe_coe, - ← (embedding_prod_mk b).nhds_eq_comap] + ← (isEmbedding_prodMk b).nhds_eq_comap] convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ · congr exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _) diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean index 644c93f2a65fb..65f52bacfc964 100644 --- a/Mathlib/Topology/Gluing.lean +++ b/Mathlib/Topology/Gluing.lean @@ -85,7 +85,7 @@ conditions are stated in a less categorical way. -- porting note (#5171): removed @[nolint has_nonempty_instance] structure GlueData extends GlueData TopCat where f_open : ∀ i j, IsOpenEmbedding (f i j) - f_mono := fun i j => (TopCat.mono_iff_injective _).mpr (f_open i j).toEmbedding.inj + f_mono i j := (TopCat.mono_iff_injective _).mpr (f_open i j).isEmbedding.inj namespace GlueData diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean index 28a19e26b5b3d..7c078d8ef7dc4 100644 --- a/Mathlib/Topology/Homeomorph.lean +++ b/Mathlib/Topology/Homeomorph.lean @@ -220,15 +220,20 @@ alias quotientMap := isQuotientMap theorem coinduced_eq (h : X ≃ₜ Y) : TopologicalSpace.coinduced h ‹_› = ‹_› := h.isQuotientMap.2.symm -protected theorem embedding (h : X ≃ₜ Y) : Embedding h := - ⟨h.inducing, h.injective⟩ +theorem isEmbedding (h : X ≃ₜ Y) : IsEmbedding h := ⟨h.inducing, h.injective⟩ + +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding /-- Homeomorphism given an embedding. -/ -noncomputable def ofEmbedding (f : X → Y) (hf : Embedding f) : X ≃ₜ Set.range f where +noncomputable def ofIsEmbedding (f : X → Y) (hf : IsEmbedding f) : X ≃ₜ Set.range f where continuous_toFun := hf.continuous.subtype_mk _ continuous_invFun := hf.continuous_iff.2 <| by simp [continuous_subtype_val] toEquiv := Equiv.ofInjective f hf.inj +@[deprecated (since := "2024-10-26")] +alias ofEmbedding := ofIsEmbedding + protected theorem secondCountableTopology [SecondCountableTopology Y] (h : X ≃ₜ Y) : SecondCountableTopology X := h.inducing.secondCountableTopology @@ -236,7 +241,7 @@ protected theorem secondCountableTopology [SecondCountableTopology Y] /-- If `h : X → Y` is a homeomorphism, `h(s)` is compact iff `s` is. -/ @[simp] theorem isCompact_image {s : Set X} (h : X ≃ₜ Y) : IsCompact (h '' s) ↔ IsCompact s := - h.embedding.isCompact_iff.symm + h.isEmbedding.isCompact_iff.symm /-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is compact iff `s` is. -/ @[simp] @@ -247,7 +252,7 @@ theorem isCompact_preimage {s : Set Y} (h : X ≃ₜ Y) : IsCompact (h ⁻¹' s) @[simp] theorem isSigmaCompact_image {s : Set X} (h : X ≃ₜ Y) : IsSigmaCompact (h '' s) ↔ IsSigmaCompact s := - h.embedding.isSigmaCompact_iff.symm + h.isEmbedding.isSigmaCompact_iff.symm /-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is σ-compact iff `s` is. -/ @[simp] @@ -297,20 +302,14 @@ theorem map_cocompact (h : X ≃ₜ Y) : map h (cocompact X) = cocompact Y := by protected theorem compactSpace [CompactSpace X] (h : X ≃ₜ Y) : CompactSpace Y where isCompact_univ := h.symm.isCompact_preimage.2 isCompact_univ -protected theorem t0Space [T0Space X] (h : X ≃ₜ Y) : T0Space Y := - h.symm.embedding.t0Space - -protected theorem t1Space [T1Space X] (h : X ≃ₜ Y) : T1Space Y := - h.symm.embedding.t1Space - -protected theorem t2Space [T2Space X] (h : X ≃ₜ Y) : T2Space Y := - h.symm.embedding.t2Space - -protected theorem t3Space [T3Space X] (h : X ≃ₜ Y) : T3Space Y := - h.symm.embedding.t3Space +protected theorem t0Space [T0Space X] (h : X ≃ₜ Y) : T0Space Y := h.symm.isEmbedding.t0Space +protected theorem t1Space [T1Space X] (h : X ≃ₜ Y) : T1Space Y := h.symm.isEmbedding.t1Space +protected theorem t2Space [T2Space X] (h : X ≃ₜ Y) : T2Space Y := h.symm.isEmbedding.t2Space +protected theorem t25Space [T25Space X] (h : X ≃ₜ Y) : T25Space Y := h.symm.isEmbedding.t25Space +protected theorem t3Space [T3Space X] (h : X ≃ₜ Y) : T3Space Y := h.symm.isEmbedding.t3Space theorem isDenseEmbedding (h : X ≃ₜ Y) : IsDenseEmbedding h := - { h.embedding with dense := h.surjective.denseRange } + { h.isEmbedding with dense := h.surjective.denseRange } @[deprecated (since := "2024-09-30")] alias denseEmbedding := isDenseEmbedding @@ -336,13 +335,13 @@ theorem isClosed_image (h : X ≃ₜ Y) {s : Set X} : IsClosed (h '' s) ↔ IsCl protected theorem isClosedMap (h : X ≃ₜ Y) : IsClosedMap h := fun _ => h.isClosed_image.2 theorem isOpenEmbedding (h : X ≃ₜ Y) : IsOpenEmbedding h := - isOpenEmbedding_of_embedding_open h.embedding h.isOpenMap + .of_isEmbedding_isOpenMap h.isEmbedding h.isOpenMap @[deprecated (since := "2024-10-18")] alias openEmbedding := isOpenEmbedding theorem isClosedEmbedding (h : X ≃ₜ Y) : IsClosedEmbedding h := - .of_embedding_closed h.embedding h.isClosedMap + .of_isEmbedding_isClosedMap h.isEmbedding h.isClosedMap @[deprecated (since := "2024-10-20")] alias closedEmbedding := isClosedEmbedding @@ -350,8 +349,8 @@ alias closedEmbedding := isClosedEmbedding protected theorem normalSpace [NormalSpace X] (h : X ≃ₜ Y) : NormalSpace Y := h.symm.isClosedEmbedding.normalSpace -protected theorem t4Space [T4Space X] (h : X ≃ₜ Y) : T4Space Y := - h.symm.isClosedEmbedding.t4Space +protected theorem t4Space [T4Space X] (h : X ≃ₜ Y) : T4Space Y := h.symm.isClosedEmbedding.t4Space +protected theorem t5Space [T5Space X] (h : X ≃ₜ Y) : T5Space Y := h.symm.isClosedEmbedding.t5Space theorem preimage_closure (h : X ≃ₜ Y) (s : Set Y) : h ⁻¹' closure s = closure (h ⁻¹' s) := h.isOpenMap.preimage_closure_eq_closure_preimage h.continuous _ @@ -378,11 +377,11 @@ theorem _root_.HasCompactMulSupport.comp_homeomorph {M} [One M] {f : Y → M} @[simp] theorem map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝 x) = 𝓝 (h x) := - h.embedding.map_nhds_of_mem _ (by simp) + h.isEmbedding.map_nhds_of_mem _ (by simp) @[simp] theorem map_punctured_nhds_eq (h : X ≃ₜ Y) (x : X) : map h (𝓝[≠] x) = 𝓝[≠] (h x) := by - convert h.embedding.map_nhdsWithin_eq ({x}ᶜ) x + convert h.isEmbedding.map_nhdsWithin_eq ({x}ᶜ) x rw [h.image_compl, Set.image_singleton] theorem symm_map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h.symm (𝓝 (h x)) = 𝓝 x := by @@ -916,11 +915,14 @@ noncomputable def homeomorph : X ≃ₜ Y where protected lemma isClosedMap : IsClosedMap f := (hf.homeomorph f).isClosedMap protected lemma inducing : Inducing f := (hf.homeomorph f).inducing lemma isQuotientMap : IsQuotientMap f := (hf.homeomorph f).isQuotientMap -protected lemma embedding : Embedding f := (hf.homeomorph f).embedding +lemma isEmbedding : IsEmbedding f := (hf.homeomorph f).isEmbedding lemma isOpenEmbedding : IsOpenEmbedding f := (hf.homeomorph f).isOpenEmbedding lemma isClosedEmbedding : IsClosedEmbedding f := (hf.homeomorph f).isClosedEmbedding lemma isDenseEmbedding : IsDenseEmbedding f := (hf.homeomorph f).isDenseEmbedding +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding + @[deprecated (since := "2024-10-22")] alias quotientMap := isQuotientMap @@ -946,11 +948,14 @@ lemma isHomeomorph_iff_exists_inverse : IsHomeomorph f ↔ Continuous f ∧ ∃ · exact (Homeomorph.mk ⟨f, g, hg.1, hg.2.1⟩ hf hg.2.2).isHomeomorph /-- A map is a homeomorphism iff it is a surjective embedding. -/ -lemma isHomeomorph_iff_embedding_surjective : IsHomeomorph f ↔ Embedding f ∧ Surjective f where - mp hf := ⟨hf.embedding, hf.surjective⟩ +lemma isHomeomorph_iff_isEmbedding_surjective : IsHomeomorph f ↔ IsEmbedding f ∧ Surjective f where + mp hf := ⟨hf.isEmbedding, hf.surjective⟩ mpr h := ⟨h.1.continuous, ((isOpenEmbedding_iff f).2 ⟨h.1, h.2.range_eq ▸ isOpen_univ⟩).isOpenMap, h.1.inj, h.2⟩ +@[deprecated (since := "2024-10-26")] +alias isHomeomorph_iff_embedding_surjective := isHomeomorph_iff_isEmbedding_surjective + /-- A map is a homeomorphism iff it is continuous, closed and bijective. -/ lemma isHomeomorph_iff_continuous_isClosedMap_bijective : IsHomeomorph f ↔ Continuous f ∧ IsClosedMap f ∧ Function.Bijective f := @@ -980,8 +985,8 @@ lemma IsHomeomorph.sigmaMap {ι κ : Type*} {X : ι → Type*} {Y : κ → Type* [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : ι → κ} (hf : Bijective f) {g : (i : ι) → X i → Y (f i)} (hg : ∀ i, IsHomeomorph (g i)) : IsHomeomorph (Sigma.map f g) := by - simp_rw [isHomeomorph_iff_embedding_surjective,] at hg ⊢ - exact ⟨(embedding_sigma_map hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩ + simp_rw [isHomeomorph_iff_isEmbedding_surjective,] at hg ⊢ + exact ⟨(isEmbedding_sigmaMap hf.1).2 fun i ↦ (hg i).1, hf.2.sigma_map fun i ↦ (hg i).2⟩ lemma IsHomeomorph.pi_map {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (h : ∀ i, IsHomeomorph (f i)) : diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index c227c3915781d..6859a23562128 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -45,13 +45,16 @@ instance : T5Space ℝ≥0∞ := inferInstance instance : T4Space ℝ≥0∞ := inferInstance instance : SecondCountableTopology ℝ≥0∞ := - orderIsoUnitIntervalBirational.toHomeomorph.embedding.secondCountableTopology + orderIsoUnitIntervalBirational.toHomeomorph.isEmbedding.secondCountableTopology instance : MetrizableSpace ENNReal := - orderIsoUnitIntervalBirational.toHomeomorph.embedding.metrizableSpace + orderIsoUnitIntervalBirational.toHomeomorph.isEmbedding.metrizableSpace -theorem embedding_coe : Embedding ((↑) : ℝ≥0 → ℝ≥0∞) := - coe_strictMono.embedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio +theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) := + coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe']; exact ordConnected_Iio + +@[deprecated (since := "2024-10-26")] +alias embedding_coe := isEmbedding_coe theorem isOpen_ne_top : IsOpen { a : ℝ≥0∞ | a ≠ ∞ } := isOpen_ne @@ -60,7 +63,7 @@ theorem isOpen_Ico_zero : IsOpen (Ico 0 b) := by exact isOpen_Iio theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) := - ⟨embedding_coe, by rw [range_coe']; exact isOpen_Iio⟩ + ⟨isEmbedding_coe, by rw [range_coe']; exact isOpen_Iio⟩ @[deprecated (since := "2024-10-18")] alias openEmbedding_coe := isOpenEmbedding_coe @@ -71,15 +74,15 @@ theorem coe_range_mem_nhds : range ((↑) : ℝ≥0 → ℝ≥0∞) ∈ 𝓝 (r @[norm_cast] theorem tendsto_coe {f : Filter α} {m : α → ℝ≥0} {a : ℝ≥0} : Tendsto (fun a => (m a : ℝ≥0∞)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) := - embedding_coe.tendsto_nhds_iff.symm + isEmbedding_coe.tendsto_nhds_iff.symm @[fun_prop] theorem continuous_coe : Continuous ((↑) : ℝ≥0 → ℝ≥0∞) := - embedding_coe.continuous + isEmbedding_coe.continuous theorem continuous_coe_iff {α} [TopologicalSpace α] {f : α → ℝ≥0} : (Continuous fun a => (f a : ℝ≥0∞)) ↔ Continuous f := - embedding_coe.continuous_iff.symm + isEmbedding_coe.continuous_iff.symm theorem nhds_coe {r : ℝ≥0} : 𝓝 (r : ℝ≥0∞) = (𝓝 r).map (↑) := (isOpenEmbedding_coe.map_nhds_eq r).symm diff --git a/Mathlib/Topology/Instances/ENat.lean b/Mathlib/Topology/Instances/ENat.lean index c69882b280e04..7372c30ed2795 100644 --- a/Mathlib/Topology/Instances/ENat.lean +++ b/Mathlib/Topology/Instances/ENat.lean @@ -30,11 +30,14 @@ instance : OrderTopology ℕ∞ := ⟨rfl⟩ @[simp] theorem range_natCast : range ((↑) : ℕ → ℕ∞) = Iio ⊤ := WithTop.range_coe -theorem embedding_natCast : Embedding ((↑) : ℕ → ℕ∞) := - Nat.strictMono_cast.embedding_of_ordConnected <| range_natCast ▸ ordConnected_Iio +theorem isEmbedding_natCast : IsEmbedding ((↑) : ℕ → ℕ∞) := + Nat.strictMono_cast.isEmbedding_of_ordConnected <| range_natCast ▸ ordConnected_Iio + +@[deprecated (since := "2024-10-26")] +alias embedding_natCast := isEmbedding_natCast theorem isOpenEmbedding_natCast : IsOpenEmbedding ((↑) : ℕ → ℕ∞) := - ⟨embedding_natCast, range_natCast ▸ isOpen_Iio⟩ + ⟨isEmbedding_natCast, range_natCast ▸ isOpen_Iio⟩ @[deprecated (since := "2024-10-18")] alias openEmbedding_natCast := isOpenEmbedding_natCast diff --git a/Mathlib/Topology/Instances/EReal.lean b/Mathlib/Topology/Instances/EReal.lean index 89c410a5d2b73..cedc98e15dfa0 100644 --- a/Mathlib/Topology/Instances/EReal.lean +++ b/Mathlib/Topology/Instances/EReal.lean @@ -48,11 +48,14 @@ instance : SecondCountableTopology EReal := /-! ### Real coercion -/ -theorem embedding_coe : Embedding ((↑) : ℝ → EReal) := - coe_strictMono.embedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo +theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ → EReal) := + coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo + +@[deprecated (since := "2024-10-26")] +alias embedding_coe := isEmbedding_coe theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ → EReal) := - ⟨embedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩ + ⟨isEmbedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩ @[deprecated (since := "2024-10-18")] alias openEmbedding_coe := isOpenEmbedding_coe @@ -60,13 +63,13 @@ alias openEmbedding_coe := isOpenEmbedding_coe @[norm_cast] theorem tendsto_coe {α : Type*} {f : Filter α} {m : α → ℝ} {a : ℝ} : Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) := - embedding_coe.tendsto_nhds_iff.symm + isEmbedding_coe.tendsto_nhds_iff.symm theorem _root_.continuous_coe_real_ereal : Continuous ((↑) : ℝ → EReal) := - embedding_coe.continuous + isEmbedding_coe.continuous theorem continuous_coe_iff {f : α → ℝ} : (Continuous fun a => (f a : EReal)) ↔ Continuous f := - embedding_coe.continuous_iff.symm + isEmbedding_coe.continuous_iff.symm theorem nhds_coe {r : ℝ} : 𝓝 (r : EReal) = (𝓝 r).map (↑) := (isOpenEmbedding_coe.map_nhds_eq r).symm @@ -92,12 +95,15 @@ def neBotTopHomeomorphReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ₜ ℝ where /-! ### ENNReal coercion -/ -theorem embedding_coe_ennreal : Embedding ((↑) : ℝ≥0∞ → EReal) := - coe_ennreal_strictMono.embedding_of_ordConnected <| by +theorem isEmbedding_coe_ennreal : IsEmbedding ((↑) : ℝ≥0∞ → EReal) := + coe_ennreal_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_ennreal]; exact ordConnected_Ici +@[deprecated (since := "2024-10-26")] +alias embedding_coe_ennreal := isEmbedding_coe_ennreal + theorem isClosedEmbedding_coe_ennreal : IsClosedEmbedding ((↑) : ℝ≥0∞ → EReal) := - ⟨embedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩ + ⟨isEmbedding_coe_ennreal, by rw [range_coe_ennreal]; exact isClosed_Ici⟩ @[deprecated (since := "2024-10-20")] alias closedEmbedding_coe_ennreal := isClosedEmbedding_coe_ennreal @@ -105,14 +111,14 @@ alias closedEmbedding_coe_ennreal := isClosedEmbedding_coe_ennreal @[norm_cast] theorem tendsto_coe_ennreal {α : Type*} {f : Filter α} {m : α → ℝ≥0∞} {a : ℝ≥0∞} : Tendsto (fun a => (m a : EReal)) f (𝓝 ↑a) ↔ Tendsto m f (𝓝 a) := - embedding_coe_ennreal.tendsto_nhds_iff.symm + isEmbedding_coe_ennreal.tendsto_nhds_iff.symm theorem _root_.continuous_coe_ennreal_ereal : Continuous ((↑) : ℝ≥0∞ → EReal) := - embedding_coe_ennreal.continuous + isEmbedding_coe_ennreal.continuous theorem continuous_coe_ennreal_iff {f : α → ℝ≥0∞} : (Continuous fun a => (f a : EReal)) ↔ Continuous f := - embedding_coe_ennreal.continuous_iff.symm + isEmbedding_coe_ennreal.continuous_iff.symm /-! ### Neighborhoods of infinity -/ diff --git a/Mathlib/Topology/Instances/Rat.lean b/Mathlib/Topology/Instances/Rat.lean index 8847d81d5d088..a09e2b65750df 100644 --- a/Mathlib/Topology/Instances/Rat.lean +++ b/Mathlib/Topology/Instances/Rat.lean @@ -42,8 +42,11 @@ theorem isDenseEmbedding_coe_real : IsDenseEmbedding ((↑) : ℚ → ℝ) := @[deprecated (since := "2024-09-30")] alias denseEmbedding_coe_real := isDenseEmbedding_coe_real -theorem embedding_coe_real : Embedding ((↑) : ℚ → ℝ) := - isDenseEmbedding_coe_real.to_embedding +theorem isEmbedding_coe_real : IsEmbedding ((↑) : ℚ → ℝ) := + isDenseEmbedding_coe_real.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding_coe_real := isEmbedding_coe_real theorem continuous_coe_real : Continuous ((↑) : ℚ → ℝ) := uniformContinuous_coe_real.continuous diff --git a/Mathlib/Topology/Instances/TrivSqZeroExt.lean b/Mathlib/Topology/Instances/TrivSqZeroExt.lean index 0868eabcd9e01..1ef2a9105f02b 100644 --- a/Mathlib/Topology/Instances/TrivSqZeroExt.lean +++ b/Mathlib/Topology/Instances/TrivSqZeroExt.lean @@ -63,11 +63,17 @@ theorem continuous_inl [Zero M] : Continuous (inl : R → tsze R M) := theorem continuous_inr [Zero R] : Continuous (inr : M → tsze R M) := continuous_const.prod_mk continuous_id -theorem embedding_inl [Zero M] : Embedding (inl : R → tsze R M) := - embedding_of_embedding_compose continuous_inl continuous_fst embedding_id +theorem IsEmbedding.inl [Zero M] : IsEmbedding (inl : R → tsze R M) := + .of_comp continuous_inl continuous_fst .id -theorem embedding_inr [Zero R] : Embedding (inr : M → tsze R M) := - embedding_of_embedding_compose continuous_inr continuous_snd embedding_id +@[deprecated (since := "2024-10-26")] +alias embedding_inl := IsEmbedding.inl + +theorem IsEmbedding.inr [Zero R] : IsEmbedding (inr : M → tsze R M) := + .of_comp continuous_inr continuous_snd .id + +@[deprecated (since := "2024-10-26")] +alias embedding_inr := IsEmbedding.inr variable (R M) diff --git a/Mathlib/Topology/IsLocalHomeomorph.lean b/Mathlib/Topology/IsLocalHomeomorph.lean index d75d32d051089..84f295b840f54 100644 --- a/Mathlib/Topology/IsLocalHomeomorph.lean +++ b/Mathlib/Topology/IsLocalHomeomorph.lean @@ -46,7 +46,7 @@ theorem isLocalHomeomorphOn_iff_isOpenEmbedding_restrict {f : X → Y} : exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩ · obtain ⟨U, hU, emb⟩ := h x hx have : IsOpenEmbedding ((interior U).restrict f) := by - refine emb.comp ⟨embedding_inclusion interior_subset, ?_⟩ + refine emb.comp ⟨.inclusion interior_subset, ?_⟩ rw [Set.range_inclusion]; exact isOpen_induced isOpen_interior obtain ⟨cont, inj, openMap⟩ := isOpenEmbedding_iff_continuous_injective_open.mp this haveI : Nonempty X := ⟨x⟩ @@ -212,10 +212,13 @@ theorem isOpenEmbedding_of_injective (hf : IsLocalHomeomorph f) (hi : f.Injectiv alias openEmbedding_of_injective := isOpenEmbedding_of_injective /-- A surjective embedding is a homeomorphism. -/ -noncomputable def _root_.Embedding.toHomeomeomorph_of_surjective (hf : Embedding f) +noncomputable def _root_.IsEmbedding.toHomeomorph_of_surjective (hf : IsEmbedding f) (hsurj : Function.Surjective f) : X ≃ₜ Y := Homeomorph.homeomorphOfContinuousOpen (Equiv.ofBijective f ⟨hf.inj, hsurj⟩) - hf.continuous (hf.toIsOpenEmbedding_of_surjective hsurj).isOpenMap + hf.continuous (hf.isOpenEmbedding_of_surjective hsurj).isOpenMap + +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.toHomeomeomorph_of_surjective := IsEmbedding.toHomeomorph_of_surjective /-- A bijective local homeomorphism is a homeomorphism. -/ noncomputable def toHomeomorph_of_bijective (hf : IsLocalHomeomorph f) (hb : f.Bijective) : @@ -237,7 +240,8 @@ theorem isTopologicalBasis (hf : IsLocalHomeomorph f) : IsTopologicalBasis {U : Set X | ∃ V : Set Y, IsOpen V ∧ ∃ s : C(V,X), f ∘ s = (↑) ∧ Set.range s = U} := by refine isTopologicalBasis_of_isOpen_of_nhds ?_ fun x U hx hU ↦ ?_ · rintro _ ⟨U, hU, s, hs, rfl⟩ - refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨embedding_subtype_val, ?_⟩) s.continuous).isOpen_range + refine (isOpenEmbedding_of_comp hf (hs ▸ ⟨IsEmbedding.subtypeVal, ?_⟩) + s.continuous).isOpen_range rwa [Subtype.range_val] · obtain ⟨f, hxf, rfl⟩ := hf x refine ⟨f.source ∩ U, ⟨f.target ∩ f.symm ⁻¹' U, f.symm.isOpen_inter_preimage hU, diff --git a/Mathlib/Topology/LocalAtTarget.lean b/Mathlib/Topology/LocalAtTarget.lean index 73a4072157b9c..fa013d4e10968 100644 --- a/Mathlib/Topology/LocalAtTarget.lean +++ b/Mathlib/Topology/LocalAtTarget.lean @@ -11,7 +11,7 @@ import Mathlib.Topology.LocallyClosed We show that the following properties of continuous maps are local at the target : - `Inducing` -- `Embedding` +- `IsEmbedding` - `IsOpenEmbedding` - `IsClosedEmbedding` @@ -34,11 +34,17 @@ theorem Set.restrictPreimage_inducing (s : Set β) (h : Inducing f) : alias Inducing.restrictPreimage := Set.restrictPreimage_inducing -theorem Set.restrictPreimage_embedding (s : Set β) (h : Embedding f) : - Embedding (s.restrictPreimage f) := +theorem Set.restrictPreimage_isEmbedding (s : Set β) (h : IsEmbedding f) : + IsEmbedding (s.restrictPreimage f) := ⟨h.1.restrictPreimage s, h.2.restrictPreimage s⟩ -alias Embedding.restrictPreimage := Set.restrictPreimage_embedding +@[deprecated (since := "2024-10-26")] +alias Set.restrictPreimage_embedding := Set.restrictPreimage_isEmbedding + +alias IsEmbedding.restrictPreimage := Set.restrictPreimage_isEmbedding + +@[deprecated (since := "2024-10-26")] +alias Embedding.restrictPreimage := IsEmbedding.restrictPreimage theorem Set.restrictPreimage_isOpenEmbedding (s : Set β) (h : IsOpenEmbedding f) : IsOpenEmbedding (s.restrictPreimage f) := @@ -167,9 +173,9 @@ theorem inducing_iff_inducing_of_iSup_eq_top (h : Continuous f) : inf_eq_left, Filter.le_principal_iff] exact Filter.preimage_mem_comap ((U i).2.mem_nhds hi) -theorem embedding_iff_embedding_of_iSup_eq_top (h : Continuous f) : - Embedding f ↔ ∀ i, Embedding ((U i).1.restrictPreimage f) := by - simp_rw [embedding_iff] +theorem isEmbedding_iff_of_iSup_eq_top (h : Continuous f) : + IsEmbedding f ↔ ∀ i, IsEmbedding ((U i).1.restrictPreimage f) := by + simp_rw [isEmbedding_iff] rw [forall_and] apply and_congr · apply inducing_iff_inducing_of_iSup_eq_top <;> assumption @@ -177,12 +183,15 @@ theorem embedding_iff_embedding_of_iSup_eq_top (h : Continuous f) : convert congr_arg SetLike.coe hU simp +@[deprecated (since := "2024-10-26")] +alias embedding_iff_embedding_of_iSup_eq_top := isEmbedding_iff_of_iSup_eq_top + theorem isOpenEmbedding_iff_isOpenEmbedding_of_iSup_eq_top (h : Continuous f) : IsOpenEmbedding f ↔ ∀ i, IsOpenEmbedding ((U i).1.restrictPreimage f) := by simp_rw [isOpenEmbedding_iff] rw [forall_and] apply and_congr - · apply embedding_iff_embedding_of_iSup_eq_top <;> assumption + · apply isEmbedding_iff_of_iSup_eq_top <;> assumption · simp_rw [Set.range_restrictPreimage] apply isOpen_iff_coe_preimage_of_iSup_eq_top hU @@ -195,7 +204,7 @@ theorem isClosedEmbedding_iff_isClosedEmbedding_of_iSup_eq_top (h : Continuous f simp_rw [isClosedEmbedding_iff] rw [forall_and] apply and_congr - · apply embedding_iff_embedding_of_iSup_eq_top <;> assumption + · apply isEmbedding_iff_of_iSup_eq_top <;> assumption · simp_rw [Set.range_restrictPreimage] apply isClosed_iff_coe_preimage_of_iSup_eq_top hU diff --git a/Mathlib/Topology/LocallyClosed.lean b/Mathlib/Topology/LocallyClosed.lean index 6aa387864372e..25a830958acf9 100644 --- a/Mathlib/Topology/LocallyClosed.lean +++ b/Mathlib/Topology/LocallyClosed.lean @@ -125,12 +125,15 @@ lemma Inducing.isLocallyClosed_iff {s : Set X} · rintro ⟨_, ⟨U, Z, hU, hZ, rfl⟩, rfl⟩ exact ⟨_, _, ⟨U, hU, rfl⟩, ⟨Z, hZ, rfl⟩, rfl⟩ -lemma Embedding.isLocallyClosed_iff {s : Set X} - {f : X → Y} (hf : Embedding f) : +lemma IsEmbedding.isLocallyClosed_iff {s : Set X} + {f : X → Y} (hf : IsEmbedding f) : IsLocallyClosed s ↔ ∃ s' : Set Y, IsLocallyClosed s' ∧ s' ∩ range f = f '' s := by simp_rw [hf.toInducing.isLocallyClosed_iff, ← (image_injective.mpr hf.inj).eq_iff, image_preimage_eq_inter_range] +@[deprecated (since := "2024-10-26")] +alias Embedding.isLocallyClosed_iff := IsEmbedding.isLocallyClosed_iff + lemma IsLocallyClosed.image {s : Set X} (hs : IsLocallyClosed s) {f : X → Y} (hf : Inducing f) (hf' : IsLocallyClosed (range f)) : IsLocallyClosed (f '' s) := by diff --git a/Mathlib/Topology/Maps/Basic.lean b/Mathlib/Topology/Maps/Basic.lean index 16c18a15ebc2f..ff834620302c0 100644 --- a/Mathlib/Topology/Maps/Basic.lean +++ b/Mathlib/Topology/Maps/Basic.lean @@ -18,14 +18,14 @@ This file introduces the following properties of a map `f : X → Y` between top * `Inducing f` means the topology on `X` is the one induced via `f` from the topology on `Y`. These behave like embeddings except they need not be injective. Instead, points of `X` which are identified by `f` are also inseparable in the topology on `X`. -* `Embedding f` means `f` is inducing and also injective. Equivalently, `f` identifies `X` with +* `IsEmbedding f` means `f` is inducing and also injective. Equivalently, `f` identifies `X` with a subspace of `Y`. * `IsOpenEmbedding f` means `f` is an embedding with open image, so it identifies `X` with an open subspace of `Y`. Equivalently, `f` is an embedding and an open map. * `IsClosedEmbedding f` similarly means `f` is an embedding with closed image, so it identifies `X` with a closed subspace of `Y`. Equivalently, `f` is an embedding and a closed map. -* `IsQuotientMap f` is the dual condition to `Embedding f`: `f` is surjective and the topology +* `IsQuotientMap f` is the dual condition to `IsEmbedding f`: `f` is surjective and the topology on `Y` is the one coinduced via `f` from the topology on `X`. Equivalently, `f` identifies `Y` with a quotient of `X`. Quotient maps are also sometimes known as identification maps. @@ -162,71 +162,105 @@ end Inducing end Inducing -section Embedding +namespace IsEmbedding -theorem Function.Injective.embedding_induced [t : TopologicalSpace Y] (hf : Injective f) : - @_root_.Embedding X Y (t.induced f) t f := - @_root_.Embedding.mk X Y (t.induced f) t _ (inducing_induced f) hf +theorem _root_.Function.Injective.isEmbedding_induced [t : TopologicalSpace Y] (hf : Injective f) : + @_root_.IsEmbedding X Y (t.induced f) t f := + @_root_.IsEmbedding.mk X Y (t.induced f) t _ (inducing_induced f) hf + +@[deprecated (since := "2024-10-26")] +alias Function.Injective.embedding_induced := _root_.Function.Injective.isEmbedding_induced variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] -theorem Embedding.mk' (f : X → Y) (inj : Injective f) (induced : ∀ x, comap f (𝓝 (f x)) = 𝓝 x) : - Embedding f := +lemma mk' (f : X → Y) (inj : Injective f) (induced : ∀ x, comap f (𝓝 (f x)) = 𝓝 x) : + IsEmbedding f := ⟨inducing_iff_nhds.2 fun x => (induced x).symm, inj⟩ -theorem embedding_id : Embedding (@id X) := - ⟨inducing_id, fun _ _ h => h⟩ +@[deprecated (since := "2024-10-26")] +alias Embedding.mk' := mk' + +protected lemma id : IsEmbedding (@id X) := ⟨inducing_id, fun _ _ h => h⟩ + +@[deprecated (since := "2024-10-26")] +alias embedding_id := IsEmbedding.id -protected theorem Embedding.comp (hg : Embedding g) (hf : Embedding f) : - Embedding (g ∘ f) := +protected lemma comp (hg : IsEmbedding g) (hf : IsEmbedding f) : IsEmbedding (g ∘ f) := { hg.toInducing.comp hf.toInducing with inj := fun _ _ h => hf.inj <| hg.inj h } -theorem Embedding.of_comp_iff (hg : Embedding g) : Embedding (g ∘ f) ↔ Embedding f := by - simp_rw [embedding_iff, hg.toInducing.of_comp_iff, hg.inj.of_comp_iff f] +@[deprecated (since := "2024-10-26")] +alias Embedding.comp := IsEmbedding.comp + +lemma of_comp_iff (hg : IsEmbedding g) : IsEmbedding (g ∘ f) ↔ IsEmbedding f := by + simp_rw [isEmbedding_iff, hg.toInducing.of_comp_iff, hg.inj.of_comp_iff f] + +@[deprecated (since := "2024-10-26")] +alias Embedding.of_comp_iff := of_comp_iff + +protected lemma of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsEmbedding (g ∘ f)) : + IsEmbedding f where + toInducing := inducing_of_inducing_compose hf hg hgf.toInducing + inj := hgf.inj.of_comp -theorem embedding_of_embedding_compose - (hf : Continuous f) (hg : Continuous g) (hgf : Embedding (g ∘ f)) : Embedding f := - { induced := (inducing_of_inducing_compose hf hg hgf.toInducing).induced - inj := fun x₁ x₂ h => hgf.inj <| by simp [h, (· ∘ ·)] } +@[deprecated (since := "2024-10-26")] +alias embedding_of_embedding_compose := IsEmbedding.of_comp -protected theorem Function.LeftInverse.embedding {f : X → Y} {g : Y → X} (h : LeftInverse f g) - (hf : Continuous f) (hg : Continuous g) : _root_.Embedding g := - embedding_of_embedding_compose hg hf <| h.comp_eq_id.symm ▸ embedding_id +lemma of_leftInverse {f : X → Y} {g : Y → X} (h : LeftInverse f g) (hf : Continuous f) + (hg : Continuous g) : IsEmbedding g := .of_comp hg hf <| h.comp_eq_id.symm ▸ .id -theorem Embedding.map_nhds_eq (hf : Embedding f) (x : X) : - (𝓝 x).map f = 𝓝[range f] f x := +alias _root_.Function.LeftInverse.isEmbedding := of_leftInverse + +@[deprecated (since := "2024-10-26")] +alias _root_.Function.LeftInverse.embedding := Function.LeftInverse.isEmbedding + +lemma map_nhds_eq (hf : IsEmbedding f) (x : X) : (𝓝 x).map f = 𝓝[range f] f x := hf.1.map_nhds_eq x -theorem Embedding.map_nhds_of_mem (hf : Embedding f) (x : X) (h : range f ∈ 𝓝 (f x)) : +@[deprecated (since := "2024-10-26")] +alias Embedding.map_nhds_eq := map_nhds_eq + +lemma map_nhds_of_mem (hf : IsEmbedding f) (x : X) (h : range f ∈ 𝓝 (f x)) : (𝓝 x).map f = 𝓝 (f x) := hf.1.map_nhds_of_mem x h -theorem Embedding.tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} - (hg : Embedding g) : Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := - hg.toInducing.tendsto_nhds_iff +@[deprecated (since := "2024-10-26")] +alias Embedding.map_nhds_of_mem := map_nhds_of_mem + +lemma tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsEmbedding g) : + Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := hg.toInducing.tendsto_nhds_iff + +lemma continuous_iff (hg : IsEmbedding g) : Continuous f ↔ Continuous (g ∘ f) := + hg.toInducing.continuous_iff -theorem Embedding.continuous_iff (hg : Embedding g) : - Continuous f ↔ Continuous (g ∘ f) := - Inducing.continuous_iff hg.1 +@[deprecated (since := "2024-10-26")] +alias Embedding.continuous_iff := continuous_iff -theorem Embedding.continuous (hf : Embedding f) : Continuous f := - Inducing.continuous hf.1 +lemma continuous (hf : IsEmbedding f) : Continuous f := hf.toInducing.continuous -theorem Embedding.closure_eq_preimage_closure_image (hf : Embedding f) (s : Set X) : +lemma closure_eq_preimage_closure_image (hf : IsEmbedding f) (s : Set X) : closure s = f ⁻¹' closure (f '' s) := hf.1.closure_eq_preimage_closure_image s +@[deprecated (since := "2024-10-26")] +alias Embedding.closure_eq_preimage_closure_image := closure_eq_preimage_closure_image + /-- The topology induced under an inclusion `f : X → Y` from a discrete topological space `Y` is the discrete topology on `X`. See also `DiscreteTopology.of_continuous_injective`. -/ -theorem Embedding.discreteTopology [DiscreteTopology Y] (hf : Embedding f) : DiscreteTopology X := +lemma discreteTopology [DiscreteTopology Y] (hf : IsEmbedding f) : DiscreteTopology X := .of_continuous_injective hf.continuous hf.inj -theorem Embedding.of_subsingleton [Subsingleton X] (f : X → Y) : Embedding f := +@[deprecated (since := "2024-10-26")] +alias Embedding.discreteTopology := discreteTopology + +lemma of_subsingleton [Subsingleton X] (f : X → Y) : IsEmbedding f := ⟨.of_subsingleton f, f.injective_of_subsingleton⟩ -end Embedding +@[deprecated (since := "2024-10-26")] +alias Embedding.of_subsingleton := of_subsingleton + +end IsEmbedding section IsQuotientMap @@ -488,15 +522,19 @@ section IsOpenEmbedding variable [TopologicalSpace X] [TopologicalSpace Y] -theorem IsOpenEmbedding.isOpenMap (hf : IsOpenEmbedding f) : IsOpenMap f := - hf.toEmbedding.toInducing.isOpenMap hf.isOpen_range +lemma IsOpenEmbedding.isEmbedding (hf : IsOpenEmbedding f) : IsEmbedding f := hf.toIsEmbedding +lemma IsOpenEmbedding.inducing (hf : IsOpenEmbedding f) : Inducing f := + hf.isEmbedding.toInducing + +lemma IsOpenEmbedding.isOpenMap (hf : IsOpenEmbedding f) : IsOpenMap f := + hf.isEmbedding.toInducing.isOpenMap hf.isOpen_range @[deprecated (since := "2024-10-18")] alias OpenEmbedding.isOpenMap := IsOpenEmbedding.isOpenMap theorem IsOpenEmbedding.map_nhds_eq (hf : IsOpenEmbedding f) (x : X) : map f (𝓝 x) = 𝓝 (f x) := - hf.toEmbedding.map_nhds_of_mem _ <| hf.isOpen_range.mem_nhds <| mem_range_self _ + hf.isEmbedding.map_nhds_of_mem _ <| hf.isOpen_range.mem_nhds <| mem_range_self _ @[deprecated (since := "2024-10-18")] alias OpenEmbedding.map_nhds_eq := IsOpenEmbedding.map_nhds_eq @@ -504,7 +542,7 @@ alias OpenEmbedding.map_nhds_eq := IsOpenEmbedding.map_nhds_eq theorem IsOpenEmbedding.open_iff_image_open (hf : IsOpenEmbedding f) {s : Set X} : IsOpen s ↔ IsOpen (f '' s) := ⟨hf.isOpenMap s, fun h => by - convert ← h.preimage hf.toEmbedding.continuous + convert ← h.preimage hf.isEmbedding.continuous apply preimage_image_eq _ hf.inj⟩ @[deprecated (since := "2024-10-18")] @@ -512,7 +550,7 @@ alias OpenEmbedding.open_iff_image_open := IsOpenEmbedding.open_iff_image_open theorem IsOpenEmbedding.tendsto_nhds_iff [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsOpenEmbedding g) : Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y)) := - hg.toEmbedding.tendsto_nhds_iff + hg.isEmbedding.tendsto_nhds_iff @[deprecated (since := "2024-10-18")] alias OpenEmbedding.tendsto_nhds_iff := IsOpenEmbedding.tendsto_nhds_iff @@ -532,7 +570,7 @@ theorem IsOpenEmbedding.continuousAt_iff [TopologicalSpace Z] (hf : IsOpenEmbedd alias OpenEmbedding.continuousAt_iff := IsOpenEmbedding.continuousAt_iff theorem IsOpenEmbedding.continuous (hf : IsOpenEmbedding f) : Continuous f := - hf.toEmbedding.continuous + hf.isEmbedding.continuous @[deprecated (since := "2024-10-18")] alias OpenEmbedding.continuous := IsOpenEmbedding.continuous @@ -544,31 +582,42 @@ theorem IsOpenEmbedding.open_iff_preimage_open (hf : IsOpenEmbedding f) {s : Set @[deprecated (since := "2024-10-18")] alias OpenEmbedding.open_iff_preimage_open := IsOpenEmbedding.open_iff_preimage_open -theorem isOpenEmbedding_of_embedding_open (h₁ : Embedding f) (h₂ : IsOpenMap f) : +lemma IsOpenEmbedding.of_isEmbedding_isOpenMap (h₁ : IsEmbedding f) (h₂ : IsOpenMap f) : IsOpenEmbedding f := ⟨h₁, h₂.isOpen_range⟩ +@[deprecated (since := "2024-10-26")] +alias isOpenEmbedding_of_embedding_open := IsOpenEmbedding.of_isEmbedding_isOpenMap + @[deprecated (since := "2024-10-18")] -alias openEmbedding_of_embedding_open := isOpenEmbedding_of_embedding_open +alias openEmbedding_of_embedding_open := IsOpenEmbedding.of_isEmbedding_isOpenMap /-- A surjective embedding is an `IsOpenEmbedding`. -/ -theorem _root_.Embedding.toIsOpenEmbedding_of_surjective (hf : Embedding f) (hsurj : f.Surjective) : +lemma IsEmbedding.isOpenEmbedding_of_surjective (hf : IsEmbedding f) (hsurj : f.Surjective) : IsOpenEmbedding f := ⟨hf, hsurj.range_eq ▸ isOpen_univ⟩ +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.toIsOpenEmbedding_of_surjective := IsEmbedding.isOpenEmbedding_of_surjective + +alias IsOpenEmbedding.of_isEmbedding := IsEmbedding.isOpenEmbedding_of_surjective + @[deprecated (since := "2024-10-18")] -alias _root_.Embedding.toOpenEmbedding_of_surjective := Embedding.toIsOpenEmbedding_of_surjective +alias _root_.Embedding.toOpenEmbedding_of_surjective := IsEmbedding.isOpenEmbedding_of_surjective + +lemma isOpenEmbedding_iff_isEmbedding_isOpenMap : IsOpenEmbedding f ↔ IsEmbedding f ∧ IsOpenMap f := + ⟨fun h => ⟨h.1, h.isOpenMap⟩, fun h => .of_isEmbedding_isOpenMap h.1 h.2⟩ -theorem isOpenEmbedding_iff_embedding_open : - IsOpenEmbedding f ↔ Embedding f ∧ IsOpenMap f := - ⟨fun h => ⟨h.1, h.isOpenMap⟩, fun h => isOpenEmbedding_of_embedding_open h.1 h.2⟩ +@[deprecated (since := "2024-10-26")] +alias isOpenEmbedding_iff_embedding_open := isOpenEmbedding_iff_isEmbedding_isOpenMap @[deprecated (since := "2024-10-18")] -alias openEmbedding_iff_embedding_open := isOpenEmbedding_iff_embedding_open +alias openEmbedding_iff_embedding_open := isOpenEmbedding_iff_isEmbedding_isOpenMap theorem isOpenEmbedding_of_continuous_injective_open (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsOpenMap f) : IsOpenEmbedding f := by - simp only [isOpenEmbedding_iff_embedding_open, embedding_iff, inducing_iff_nhds, *, and_true] + simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isEmbedding_iff, inducing_iff_nhds, *, + and_true] exact fun x => le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _)) @@ -581,7 +630,7 @@ theorem isOpenEmbedding_iff_continuous_injective_open : alias openEmbedding_iff_continuous_injective_open := isOpenEmbedding_iff_continuous_injective_open theorem isOpenEmbedding_id : IsOpenEmbedding (@id X) := - ⟨embedding_id, IsOpenMap.id.isOpen_range⟩ + ⟨.id, IsOpenMap.id.isOpen_range⟩ @[deprecated (since := "2024-10-18")] alias openEmbedding_id := isOpenEmbedding_id @@ -607,7 +656,7 @@ theorem of_comp (f : X → Y) (hg : IsOpenEmbedding g) (IsOpenEmbedding.of_comp_iff f hg).1 h theorem of_isEmpty [IsEmpty X] (f : X → Y) : IsOpenEmbedding f := - isOpenEmbedding_of_embedding_open (.of_subsingleton f) (IsOpenMap.of_isEmpty f) + of_isEmbedding_isOpenMap (.of_subsingleton f) (.of_isEmpty f) theorem image_mem_nhds {f : X → Y} (hf : IsOpenEmbedding f) {s : Set X} {x : X} : f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x := by @@ -623,15 +672,15 @@ variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] namespace IsClosedEmbedding -theorem tendsto_nhds_iff {g : ι → X} {l : Filter ι} {x : X} (hf : IsClosedEmbedding f) : - Tendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x)) := - hf.toEmbedding.tendsto_nhds_iff +lemma isEmbedding (hf : IsClosedEmbedding f) : IsEmbedding f := hf.toIsEmbedding +lemma inducing (hf : IsClosedEmbedding f) : Inducing f := hf.isEmbedding.toInducing +lemma continuous (hf : IsClosedEmbedding f) : Continuous f := hf.isEmbedding.continuous -theorem continuous (hf : IsClosedEmbedding f) : Continuous f := - hf.toEmbedding.continuous +lemma tendsto_nhds_iff {g : ι → X} {l : Filter ι} {x : X} (hf : IsClosedEmbedding f) : + Tendsto g l (𝓝 x) ↔ Tendsto (f ∘ g) l (𝓝 (f x)) := hf.isEmbedding.tendsto_nhds_iff -theorem isClosedMap (hf : IsClosedEmbedding f) : IsClosedMap f := - hf.toEmbedding.toInducing.isClosedMap hf.isClosed_range +lemma isClosedMap (hf : IsClosedEmbedding f) : IsClosedMap f := + hf.isEmbedding.toInducing.isClosedMap hf.isClosed_range theorem closed_iff_image_closed (hf : IsClosedEmbedding f) {s : Set X} : IsClosed s ↔ IsClosed (f '' s) := @@ -643,16 +692,19 @@ theorem closed_iff_preimage_closed (hf : IsClosedEmbedding f) {s : Set Y} (hs : s ⊆ range f) : IsClosed s ↔ IsClosed (f ⁻¹' s) := by rw [hf.closed_iff_image_closed, image_preimage_eq_of_subset hs] -theorem _root_.IsClosedEmbedding.of_embedding_closed (h₁ : Embedding f) (h₂ : IsClosedMap f) : +lemma of_isEmbedding_isClosedMap (h₁ : IsEmbedding f) (h₂ : IsClosedMap f) : IsClosedEmbedding f := ⟨h₁, image_univ (f := f) ▸ h₂ univ isClosed_univ⟩ +@[deprecated (since := "2024-10-26")] +alias _root_.IsClosedEmbedding.of_embedding_closed := of_isEmbedding_isClosedMap + @[deprecated (since := "2024-10-20")] -alias _root_.closedEmbedding_of_embedding_closed := _root_.IsClosedEmbedding.of_embedding_closed +alias _root_.closedEmbedding_of_embedding_closed := of_isEmbedding_isClosedMap lemma _root_.IsClosedEmbedding.of_continuous_injective_isClosedMap (h₁ : Continuous f) (h₂ : Injective f) (h₃ : IsClosedMap f) : IsClosedEmbedding f := by - refine .of_embedding_closed ⟨⟨?_⟩, h₂⟩ h₃ + refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃ refine h₁.le_induced.antisymm fun s hs => ?_ refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩ rw [preimage_compl, preimage_image_eq _ h₂, compl_compl] @@ -662,20 +714,22 @@ alias _root_.closedEmbedding_of_continuous_injective_closed := IsClosedEmbedding.of_continuous_injective_isClosedMap theorem _root_.isClosedEmbedding_id : IsClosedEmbedding (@id X) := - ⟨embedding_id, IsClosedMap.id.isClosed_range⟩ + ⟨.id, IsClosedMap.id.isClosed_range⟩ @[deprecated (since := "2024-10-20")] alias _root_.closedEmbedding_id := _root_.isClosedEmbedding_id theorem comp (hg : IsClosedEmbedding g) (hf : IsClosedEmbedding f) : IsClosedEmbedding (g ∘ f) := - ⟨hg.toEmbedding.comp hf.toEmbedding, (hg.isClosedMap.comp hf.isClosedMap).isClosed_range⟩ + ⟨hg.isEmbedding.comp hf.isEmbedding, (hg.isClosedMap.comp hf.isClosedMap).isClosed_range⟩ -theorem of_comp_iff (hg : IsClosedEmbedding g) : - IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f := by - simp_rw [isClosedEmbedding_iff, hg.toEmbedding.of_comp_iff, Set.range_comp, +lemma of_comp_iff (hg : IsClosedEmbedding g) : IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f := by + simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp, ← hg.closed_iff_image_closed] +@[deprecated (since := "2024-10-26")] +alias Embedding.of_comp_iff := of_comp_iff + theorem closure_image_eq (hf : IsClosedEmbedding f) (s : Set X) : closure (f '' s) = f '' closure s := hf.isClosedMap.closure_image_eq_of_continuous hf.continuous s diff --git a/Mathlib/Topology/MetricSpace/Antilipschitz.lean b/Mathlib/Topology/MetricSpace/Antilipschitz.lean index 3ee1290ac0f7c..809699925af5d 100644 --- a/Mathlib/Topology/MetricSpace/Antilipschitz.lean +++ b/Mathlib/Topology/MetricSpace/Antilipschitz.lean @@ -168,7 +168,7 @@ theorem isClosed_range {α β : Type*} [PseudoEMetricSpace α] [EMetricSpace β] theorem isClosedEmbedding {α : Type*} {β : Type*} [EMetricSpace α] [EMetricSpace β] {K : ℝ≥0} {f : α → β} [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsClosedEmbedding f := - { (hf.isUniformEmbedding hfc).embedding with isClosed_range := hf.isClosed_range hfc } + { (hf.isUniformEmbedding hfc).isEmbedding with isClosed_range := hf.isClosed_range hfc } @[deprecated (since := "2024-10-20")] alias closedEmbedding := isClosedEmbedding diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean index 884f0a045a2a0..407ba2b7951ea 100644 --- a/Mathlib/Topology/MetricSpace/Basic.lean +++ b/Mathlib/Topology/MetricSpace/Basic.lean @@ -112,10 +112,13 @@ alias UniformEmbedding.comapMetricSpace := IsUniformEmbedding.comapMetricSpace /-- Pull back a metric space structure by an embedding. This is a version of `MetricSpace.induced` useful in case if the domain already has a `TopologicalSpace` structure. -/ -abbrev Embedding.comapMetricSpace {α β} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) - (h : Embedding f) : MetricSpace α := +abbrev IsEmbedding.comapMetricSpace {α β} [TopologicalSpace α] [m : MetricSpace β] + (f : α → β) (h : IsEmbedding f) : MetricSpace α := .replaceTopology (.induced f h.inj m) h.induced +@[deprecated (since := "2024-10-26")] +alias Embedding.comapMetricSpace := IsEmbedding.comapMetricSpace + instance Subtype.metricSpace {α : Type*} {p : α → Prop} [MetricSpace α] : MetricSpace (Subtype p) := .induced Subtype.val Subtype.coe_injective ‹_› diff --git a/Mathlib/Topology/MetricSpace/Closeds.lean b/Mathlib/Topology/MetricSpace/Closeds.lean index 8c33b2ec9c2f7..32f085537b00a 100644 --- a/Mathlib/Topology/MetricSpace/Closeds.lean +++ b/Mathlib/Topology/MetricSpace/Closeds.lean @@ -288,7 +288,7 @@ instance NonemptyCompacts.completeSpace [CompleteSpace α] : CompleteSpace (None the same statement for closed subsets -/ instance NonemptyCompacts.compactSpace [CompactSpace α] : CompactSpace (NonemptyCompacts α) := ⟨by - rw [NonemptyCompacts.ToCloseds.isUniformEmbedding.embedding.isCompact_iff, image_univ] + rw [NonemptyCompacts.ToCloseds.isUniformEmbedding.isEmbedding.isCompact_iff, image_univ] exact NonemptyCompacts.isClosed_in_closeds.isCompact⟩ /-- In a second countable space, the type of nonempty compact subsets is second countable -/ diff --git a/Mathlib/Topology/MetricSpace/Dilation.lean b/Mathlib/Topology/MetricSpace/Dilation.lean index a0d5113e469b3..4abde916f1e72 100644 --- a/Mathlib/Topology/MetricSpace/Dilation.lean +++ b/Mathlib/Topology/MetricSpace/Dilation.lean @@ -427,9 +427,12 @@ lemma isUniformEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) @[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding /-- A dilation from a metric space is an embedding -/ -protected theorem embedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : - Embedding (f : α → β) := - (Dilation.isUniformEmbedding f).embedding +theorem isEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : + IsEmbedding (f : α → β) := + (Dilation.isUniformEmbedding f).isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding /-- A dilation from a complete emetric space is a closed embedding -/ lemma isClosedEmbedding [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) : diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean index 21177706ee722..a12099f6f05cf 100644 --- a/Mathlib/Topology/MetricSpace/Isometry.lean +++ b/Mathlib/Topology/MetricSpace/Isometry.lean @@ -173,8 +173,10 @@ lemma isUniformEmbedding (hf : Isometry f) : IsUniformEmbedding f := @[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding /-- An isometry from an emetric space is an embedding -/ -protected theorem embedding (hf : Isometry f) : Embedding f := - hf.isUniformEmbedding.embedding +theorem isEmbedding (hf : Isometry f) : IsEmbedding f := hf.isUniformEmbedding.isEmbedding + +@[deprecated (since := "2024-10-26")] +alias embedding := isEmbedding /-- An isometry from a complete emetric space is a closed embedding -/ theorem isClosedEmbedding [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : @@ -246,11 +248,14 @@ alias UniformEmbedding.to_isometry := IsUniformEmbedding.to_isometry /-- An embedding from a topological space to a metric space is an isometry with respect to the induced metric space structure on the source space. -/ -theorem Embedding.to_isometry {α β} [TopologicalSpace α] [MetricSpace β] {f : α → β} - (h : Embedding f) : (letI := h.comapMetricSpace f; Isometry f) := +theorem IsEmbedding.to_isometry {α β} [TopologicalSpace α] [MetricSpace β] {f : α → β} + (h : IsEmbedding f) : (letI := h.comapMetricSpace f; Isometry f) := let _ := h.comapMetricSpace f Isometry.of_dist_eq fun _ _ => rfl +@[deprecated (since := "2024-10-26")] +alias Embedding.to_isometry := IsEmbedding.to_isometry + -- such a bijection need not exist /-- `α` and `β` are isometric if there is an isometric bijection between them. -/ -- Porting note(#5171): was @[nolint has_nonempty_instance] diff --git a/Mathlib/Topology/MetricSpace/Polish.lean b/Mathlib/Topology/MetricSpace/Polish.lean index c1e6a80a0300c..259dc5eccb7d9 100644 --- a/Mathlib/Topology/MetricSpace/Polish.lean +++ b/Mathlib/Topology/MetricSpace/Polish.lean @@ -143,10 +143,10 @@ theorem exists_nat_nat_continuous_surjective (α : Type*) [TopologicalSpace α] lemma _root_.IsClosedEmbedding.polishSpace [TopologicalSpace α] [TopologicalSpace β] [PolishSpace β] {f : α → β} (hf : IsClosedEmbedding f) : PolishSpace α := by letI := upgradePolishSpace β - letI : MetricSpace α := hf.toEmbedding.comapMetricSpace f - haveI : SecondCountableTopology α := hf.toEmbedding.secondCountableTopology + letI : MetricSpace α := hf.isEmbedding.comapMetricSpace f + haveI : SecondCountableTopology α := hf.isEmbedding.secondCountableTopology have : CompleteSpace α := by - rw [completeSpace_iff_isComplete_range hf.toEmbedding.to_isometry.isUniformInducing] + rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing] exact hf.isClosed_range.isComplete infer_instance @@ -214,8 +214,7 @@ theorem exists_polishSpace_forall_le {ι : Type*} [Countable ι] [t : Topologica .iInf ⟨none, Option.forall.2 ⟨le_rfl, hm⟩⟩ <| Option.forall.2 ⟨p, h'm⟩⟩ instance : PolishSpace ENNReal := - IsClosedEmbedding.polishSpace ⟨ENNReal.orderIsoUnitIntervalBirational.toHomeomorph.embedding, - ENNReal.orderIsoUnitIntervalBirational.range_eq ▸ isClosed_univ⟩ + ENNReal.orderIsoUnitIntervalBirational.toHomeomorph.isClosedEmbedding.polishSpace end PolishSpace diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean b/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean index 94125fb3b8a4c..3323820a562cc 100644 --- a/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean +++ b/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean @@ -219,10 +219,13 @@ protected theorem _root_.Inducing.isSeparable_preimage {f : β → α} [Topologi have := this.secondCountableTopology exact .of_subtype _ -protected theorem _root_.Embedding.isSeparable_preimage {f : β → α} [TopologicalSpace β] - (hf : Embedding f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) := +protected theorem _root_.IsEmbedding.isSeparable_preimage {f : β → α} [TopologicalSpace β] + (hf : IsEmbedding f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) := hf.toInducing.isSeparable_preimage hs +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.isSeparable_preimage := _root_.IsEmbedding.isSeparable_preimage + end Metric /-- A compact set is separable. -/ diff --git a/Mathlib/Topology/Metrizable/Basic.lean b/Mathlib/Topology/Metrizable/Basic.lean index 80f40eafabe28..fc489f8a0129c 100644 --- a/Mathlib/Topology/Metrizable/Basic.lean +++ b/Mathlib/Topology/Metrizable/Basic.lean @@ -98,13 +98,16 @@ instance metrizableSpace_prod [MetrizableSpace X] [MetrizableSpace Y] : Metrizab /-- Given an embedding of a topological space into a metrizable space, the source space is also metrizable. -/ -theorem _root_.Embedding.metrizableSpace [MetrizableSpace Y] {f : X → Y} (hf : Embedding f) : - MetrizableSpace X := +theorem _root_.IsEmbedding.metrizableSpace [MetrizableSpace Y] {f : X → Y} + (hf : IsEmbedding f) : MetrizableSpace X := letI : MetricSpace Y := metrizableSpaceMetric Y ⟨⟨hf.comapMetricSpace f, rfl⟩⟩ +@[deprecated (since := "2024-10-26")] +alias _root_.Embedding.metrizableSpace := IsEmbedding.metrizableSpace + instance MetrizableSpace.subtype [MetrizableSpace X] (s : Set X) : MetrizableSpace s := - embedding_subtype_val.metrizableSpace + IsEmbedding.subtypeVal.metrizableSpace instance metrizableSpace_pi [∀ i, MetrizableSpace (π i)] : MetrizableSpace (∀ i, π i) := by cases nonempty_fintype ι diff --git a/Mathlib/Topology/Metrizable/Urysohn.lean b/Mathlib/Topology/Metrizable/Urysohn.lean index bddb6a6ead668..66ff67b040be3 100644 --- a/Mathlib/Topology/Metrizable/Urysohn.lean +++ b/Mathlib/Topology/Metrizable/Urysohn.lean @@ -46,7 +46,7 @@ theorem exists_inducing_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Inducing f := by rsuffices ⟨f, hf⟩ : ∃ f : X → s →ᵇ ℝ, Inducing f · exact ⟨fun x => (f x).extend (Encodable.encode' s) 0, (BoundedContinuousFunction.isometry_extend (Encodable.encode' s) - (0 : ℕ →ᵇ ℝ)).embedding.toInducing.comp hf⟩ + (0 : ℕ →ᵇ ℝ)).isEmbedding.toInducing.comp hf⟩ have hd : ∀ UV : s, Disjoint (closure UV.1.1) UV.1.2ᶜ := fun UV => disjoint_compl_right.mono_right (compl_subset_compl.2 UV.2.2) -- Choose a sequence of `εₙ > 0`, `n : s`, that is bounded above by `1` and tends to zero @@ -116,8 +116,8 @@ end RegularSpace variable (X : Type*) [TopologicalSpace X] [T3Space X] [SecondCountableTopology X] /-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`. -/ -theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, Embedding f := - let ⟨f, hf⟩ := exists_inducing_l_infty X; ⟨f, hf.embedding⟩ +theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, IsEmbedding f := + let ⟨f, hf⟩ := exists_inducing_l_infty X; ⟨f, hf.isEmbedding⟩ /-- *Urysohn's metrization theorem* (Tychonoff's version): a T₃ topological space with second countable topology `X` is metrizable, i.e., there exists a metric space structure that generates the diff --git a/Mathlib/Topology/NoetherianSpace.lean b/Mathlib/Topology/NoetherianSpace.lean index 9c2e714b18849..79cc5a667cf2c 100644 --- a/Mathlib/Topology/NoetherianSpace.lean +++ b/Mathlib/Topology/NoetherianSpace.lean @@ -125,7 +125,7 @@ theorem NoetherianSpace.range [NoetherianSpace α] (f : α → β) (hf : Continu theorem noetherianSpace_set_iff (s : Set α) : NoetherianSpace s ↔ ∀ t, t ⊆ s → IsCompact t := by - simp only [noetherianSpace_iff_isCompact, embedding_subtype_val.isCompact_iff, + simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff, Subtype.forall_set_subtype] @[simp] diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index beee03643d1b3..ca052f92ae658 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -232,11 +232,14 @@ nonrec theorem StrictMono.induced_topology_eq_preorder {α β : Type*} [LinearOr /-- A strictly monotone function between linear orders with order topology is a topological embedding provided that the range of `f` is order-connected. -/ -theorem StrictMono.embedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β] +theorem StrictMono.isEmbedding_of_ordConnected {α β : Type*} [LinearOrder α] [LinearOrder β] [TopologicalSpace α] [h : OrderTopology α] [TopologicalSpace β] [OrderTopology β] {f : α → β} - (hf : StrictMono f) (hc : OrdConnected (range f)) : Embedding f := + (hf : StrictMono f) (hc : OrdConnected (range f)) : IsEmbedding f := ⟨⟨h.1.trans <| Eq.symm <| hf.induced_topology_eq_preorder hc⟩, hf.injective⟩ +@[deprecated (since := "2024-10-26")] +alias StrictMono.embedding_of_ordConnected := StrictMono.isEmbedding_of_ordConnected + /-- On a `Set.OrdConnected` subset of a linear order, the order topology for the restriction of the order is the same as the restriction to the subset of the order topology. -/ instance orderTopology_of_ordConnected {α : Type u} [TopologicalSpace α] [LinearOrder α] diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean index 4d2b050b3eb3c..0f70e094b5f72 100644 --- a/Mathlib/Topology/PartialHomeomorph.lean +++ b/Mathlib/Topology/PartialHomeomorph.lean @@ -1171,7 +1171,7 @@ whose source is all of `X`. The converse is also true; see `PartialHomeomorph.to_isOpenEmbedding`. -/ @[simps! (config := mfld_cfg) apply source target] noncomputable def toPartialHomeomorph [Nonempty X] : PartialHomeomorph X Y := - PartialHomeomorph.ofContinuousOpen (h.toEmbedding.inj.injOn.toPartialEquiv f univ) + PartialHomeomorph.ofContinuousOpen (h.isEmbedding.inj.injOn.toPartialEquiv f univ) h.continuous.continuousOn h.isOpenMap isOpen_univ variable [Nonempty X] diff --git a/Mathlib/Topology/QuasiSeparated.lean b/Mathlib/Topology/QuasiSeparated.lean index f550bb0a8528c..f4ab068bd84bc 100644 --- a/Mathlib/Topology/QuasiSeparated.lean +++ b/Mathlib/Topology/QuasiSeparated.lean @@ -54,8 +54,8 @@ theorem isQuasiSeparated_univ {α : Type*} [TopologicalSpace α] [QuasiSeparated IsQuasiSeparated (Set.univ : Set α) := isQuasiSeparated_univ_iff.mpr inferInstance -theorem IsQuasiSeparated.image_of_embedding {s : Set α} (H : IsQuasiSeparated s) (h : Embedding f) : - IsQuasiSeparated (f '' s) := by +theorem IsQuasiSeparated.image_of_isEmbedding {s : Set α} (H : IsQuasiSeparated s) + (h : IsEmbedding f) : IsQuasiSeparated (f '' s) := by intro U V hU hU' hU'' hV hV' hV'' convert (H (f ⁻¹' U) (f ⁻¹' V) @@ -78,11 +78,14 @@ theorem IsQuasiSeparated.image_of_embedding {s : Set α} (H : IsQuasiSeparated s rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left] exact hV.trans (Set.image_subset_range _ _) +@[deprecated (since := "2024-10-26")] +alias IsQuasiSeparated.image_of_embedding := IsQuasiSeparated.image_of_isEmbedding + theorem IsOpenEmbedding.isQuasiSeparated_iff (h : IsOpenEmbedding f) {s : Set α} : IsQuasiSeparated s ↔ IsQuasiSeparated (f '' s) := by - refine ⟨fun hs => hs.image_of_embedding h.toEmbedding, ?_⟩ + refine ⟨fun hs => hs.image_of_isEmbedding h.isEmbedding, ?_⟩ intro H U V hU hU' hU'' hV hV' hV'' - rw [h.toEmbedding.isCompact_iff, Set.image_inter h.inj] + rw [h.isEmbedding.isCompact_iff, Set.image_inter h.inj] exact H (f '' U) (f '' V) (Set.image_subset _ hU) (h.isOpenMap _ hU') (hU''.image h.continuous) (Set.image_subset _ hV) (h.isOpenMap _ hV') (hV''.image h.continuous) diff --git a/Mathlib/Topology/SeparatedMap.lean b/Mathlib/Topology/SeparatedMap.lean index 992ff27b3e79a..ee6f959bbb624 100644 --- a/Mathlib/Topology/SeparatedMap.lean +++ b/Mathlib/Topology/SeparatedMap.lean @@ -38,11 +38,14 @@ open scoped Topology variable {X Y A} [TopologicalSpace X] [TopologicalSpace A] -theorem embedding_toPullbackDiag (f : X → Y) : Embedding (toPullbackDiag f) := - Embedding.mk' _ (injective_toPullbackDiag f) fun x ↦ by +protected lemma IsEmbedding.toPullbackDiag (f : X → Y) : IsEmbedding (toPullbackDiag f) := + .mk' _ (injective_toPullbackDiag f) fun x ↦ by rw [toPullbackDiag, nhds_induced, Filter.comap_comap, nhds_prod_eq, Filter.comap_prod] erw [Filter.comap_id, inf_idem] +@[deprecated (since := "2024-10-26")] +alias embedding_toPullbackDiag := IsEmbedding.toPullbackDiag + lemma Continuous.mapPullback {X₁ X₂ Y₁ Y₂ Z₁ Z₂} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z₁] [TopologicalSpace Z₂] {f₁ : X₁ → Y₁} {g₁ : Z₁ → Y₁} {f₂ : X₂ → Y₂} {g₂ : Z₂ → Y₂} @@ -89,7 +92,7 @@ theorem isSeparatedMap_iff_isClosed_diagonal {f : X → Y} : theorem isSeparatedMap_iff_isClosedEmbedding {f : X → Y} : IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f) := by rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag] - exact ⟨fun h ↦ ⟨embedding_toPullbackDiag f, h⟩, fun h ↦ h.isClosed_range⟩ + exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isClosed_range⟩ @[deprecated (since := "2024-10-20")] alias isSeparatedMap_iff_closedEmbedding := isSeparatedMap_iff_isClosedEmbedding @@ -98,7 +101,7 @@ theorem isSeparatedMap_iff_isClosedMap {f : X → Y} : IsSeparatedMap f ↔ IsClosedMap (toPullbackDiag f) := isSeparatedMap_iff_isClosedEmbedding.trans ⟨IsClosedEmbedding.isClosedMap, .of_continuous_injective_isClosedMap - (embedding_toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩ + (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩ open Function.Pullback in theorem IsSeparatedMap.pullback {f : X → Y} (sep : IsSeparatedMap f) (g : A → Y) : @@ -147,7 +150,7 @@ theorem isLocallyInjective_iff_isOpen_diagonal {f : X → Y} : theorem IsLocallyInjective_iff_isOpenEmbedding {f : X → Y} : IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f) := by rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag] - exact ⟨fun h ↦ ⟨embedding_toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩ + exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩ @[deprecated (since := "2024-10-18")] alias IsLocallyInjective_iff_openEmbedding := IsLocallyInjective_iff_isOpenEmbedding @@ -156,7 +159,7 @@ theorem isLocallyInjective_iff_isOpenMap {f : X → Y} : IsLocallyInjective f ↔ IsOpenMap (toPullbackDiag f) := IsLocallyInjective_iff_isOpenEmbedding.trans ⟨IsOpenEmbedding.isOpenMap, isOpenEmbedding_of_continuous_injective_open - (embedding_toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩ + (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩ theorem discreteTopology_iff_locallyInjective (y : Y) : DiscreteTopology X ↔ IsLocallyInjective fun _ : X ↦ y := by diff --git a/Mathlib/Topology/Separation/Basic.lean b/Mathlib/Topology/Separation/Basic.lean index cd3e2041e3180..12128827f3111 100644 --- a/Mathlib/Topology/Separation/Basic.lean +++ b/Mathlib/Topology/Separation/Basic.lean @@ -77,7 +77,7 @@ occasionally the literature swaps definitions for e.g. T₃ and regular. points of the form `(a, a) : X × X`) is closed under the product topology. * `separatedNhds_of_finset_finset`: Any two disjoint finsets are `SeparatedNhds`. * Most topological constructions preserve Hausdorffness; - these results are part of the typeclass inference system (e.g. `Embedding.t2Space`) + these results are part of the typeclass inference system (e.g. `IsEmbedding.t2Space`) * `Set.EqOn.closure`: If two functions are equal on some set `s`, they are equal on its closure. * `IsCompact.isClosed`: All compact sets are closed. * `WeaklyLocallyCompactSpace.locallyCompactSpace`: If a topological space is both @@ -276,13 +276,19 @@ protected theorem Inducing.injective [TopologicalSpace Y] [T0Space X] {f : X → (hf.inseparable_iff.1 <| .of_eq h).eq /-- A topology `Inducing` map from a T₀ space is a topological embedding. -/ -protected theorem Inducing.embedding [TopologicalSpace Y] [T0Space X] {f : X → Y} - (hf : Inducing f) : Embedding f := +protected theorem Inducing.isEmbedding [TopologicalSpace Y] [T0Space X] {f : X → Y} + (hf : Inducing f) : IsEmbedding f := ⟨hf, hf.injective⟩ -lemma embedding_iff_inducing [TopologicalSpace Y] [T0Space X] {f : X → Y} : - Embedding f ↔ Inducing f := - ⟨Embedding.toInducing, Inducing.embedding⟩ +@[deprecated (since := "2024-10-26")] +alias Inducing.embedding := Inducing.isEmbedding + +lemma isEmbedding_iff_inducing [TopologicalSpace Y] [T0Space X] {f : X → Y} : + IsEmbedding f ↔ Inducing f := + ⟨IsEmbedding.toInducing, Inducing.isEmbedding⟩ + +@[deprecated (since := "2024-10-26")] +alias embedding_iff_inducing := isEmbedding_iff_inducing theorem t0Space_iff_nhds_injective (X : Type u) [TopologicalSpace X] : T0Space X ↔ Injective (𝓝 : X → Filter X) := @@ -394,12 +400,15 @@ theorem t0Space_of_injective_of_continuous [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] : T0Space X := ⟨fun _ _ h => hf <| (h.map hf').eq⟩ -protected theorem Embedding.t0Space [TopologicalSpace Y] [T0Space Y] {f : X → Y} - (hf : Embedding f) : T0Space X := +protected theorem IsEmbedding.t0Space [TopologicalSpace Y] [T0Space Y] {f : X → Y} + (hf : IsEmbedding f) : T0Space X := t0Space_of_injective_of_continuous hf.inj hf.continuous +@[deprecated (since := "2024-10-26")] +alias Embedding.t0Space := IsEmbedding.t0Space + instance Subtype.t0Space [T0Space X] {p : X → Prop} : T0Space (Subtype p) := - embedding_subtype_val.t0Space + IsEmbedding.subtypeVal.t0Space theorem t0Space_iff_or_not_mem_closure (X : Type u) [TopologicalSpace X] : T0Space X ↔ Pairwise fun a b : X => a ∉ closure ({b} : Set X) ∨ b ∉ closure ({a} : Set X) := by @@ -413,8 +422,7 @@ instance Pi.instT0Space {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace T0Space (∀ i, X i) := ⟨fun _ _ h => funext fun i => (h.map (continuous_apply i)).eq⟩ -instance ULift.instT0Space [T0Space X] : T0Space (ULift X) := - embedding_uLift_down.t0Space +instance ULift.instT0Space [T0Space X] : T0Space (ULift X) := IsEmbedding.uliftDown.t0Space theorem T0Space.of_cover (h : ∀ x y, Inseparable x y → ∃ s : Set X, x ∈ s ∧ y ∈ s ∧ T0Space s) : T0Space X := by @@ -678,13 +686,16 @@ theorem t1Space_of_injective_of_continuous [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] : T1Space X := t1Space_iff_specializes_imp_eq.2 fun _ _ h => hf (h.map hf').eq -protected theorem Embedding.t1Space [TopologicalSpace Y] [T1Space Y] {f : X → Y} - (hf : Embedding f) : T1Space X := +protected theorem IsEmbedding.t1Space [TopologicalSpace Y] [T1Space Y] {f : X → Y} + (hf : IsEmbedding f) : T1Space X := t1Space_of_injective_of_continuous hf.inj hf.continuous +@[deprecated (since := "2024-10-26")] +alias Embedding.t1Space := IsEmbedding.t1Space + instance Subtype.t1Space {X : Type u} [TopologicalSpace X] [T1Space X] {p : X → Prop} : T1Space (Subtype p) := - embedding_subtype_val.t1Space + IsEmbedding.subtypeVal.t1Space instance [TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y) := ⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ isClosed_singleton.prod isClosed_singleton⟩ @@ -694,7 +705,7 @@ instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, ⟨fun f => univ_pi_singleton f ▸ isClosed_set_pi fun _ _ => isClosed_singleton⟩ instance ULift.instT1Space [T1Space X] : T1Space (ULift X) := - embedding_uLift_down.t1Space + IsEmbedding.uliftDown.t1Space -- see Note [lower instance priority] instance (priority := 100) TotallyDisconnectedSpace.t1Space [h : TotallyDisconnectedSpace X] : @@ -1549,12 +1560,15 @@ theorem T2Space.of_injective_continuous [TopologicalSpace Y] [T2Space Y] {f : X /-- If the codomain of a topological embedding is a Hausdorff space, then so is its domain. See also `T2Space.of_continuous_injective`. -/ -theorem Embedding.t2Space [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Embedding f) : - T2Space X := +theorem IsEmbedding.t2Space [TopologicalSpace Y] [T2Space Y] {f : X → Y} + (hf : IsEmbedding f) : T2Space X := .of_injective_continuous hf.inj hf.continuous +@[deprecated (since := "2024-10-26")] +alias Embedding.t2Space := IsEmbedding.t2Space + instance ULift.instT2Space [T2Space X] : T2Space (ULift X) := - embedding_uLift_down.t2Space + IsEmbedding.uliftDown.t2Space instance [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X ⊕ Y) := by @@ -1722,7 +1736,7 @@ alias Function.LeftInverse.closed_range := Function.LeftInverse.isClosed_range theorem Function.LeftInverse.isClosedEmbedding [T2Space X] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosedEmbedding g := - ⟨h.embedding hf hg, h.isClosed_range hf hg⟩ + ⟨.of_leftInverse h hf hg, h.isClosed_range hf hg⟩ @[deprecated (since := "2024-10-20")] alias Function.LeftInverse.closedEmbedding := Function.LeftInverse.isClosedEmbedding @@ -2028,7 +2042,7 @@ theorem RegularSpace.inf {X} {t₁ t₂ : TopologicalSpace X} (h₁ : @RegularSp exact regularSpace_iInf (Bool.forall_bool.2 ⟨h₂, h₁⟩) instance {p : X → Prop} : RegularSpace (Subtype p) := - embedding_subtype_val.toInducing.regularSpace + IsEmbedding.subtypeVal.toInducing.regularSpace instance [TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y) := (regularSpace_induced (@Prod.fst X Y)).inf (regularSpace_induced (@Prod.snd X Y)) @@ -2143,12 +2157,15 @@ theorem T25Space.of_injective_continuous [TopologicalSpace Y] [T25Space Y] {f : t2_5 x y hne := (tendsto_lift'_closure_nhds hcont x).disjoint (t2_5 <| hinj.ne hne) (tendsto_lift'_closure_nhds hcont y) -theorem Embedding.t25Space [TopologicalSpace Y] [T25Space Y] {f : X → Y} (hf : Embedding f) : - T25Space X := +theorem IsEmbedding.t25Space [TopologicalSpace Y] [T25Space Y] {f : X → Y} + (hf : IsEmbedding f) : T25Space X := .of_injective_continuous hf.inj hf.continuous +@[deprecated (since := "2024-10-26")] +alias Embedding.t25Space := IsEmbedding.t25Space + instance Subtype.instT25Space [T25Space X] {p : X → Prop} : T25Space {x // p x} := - embedding_subtype_val.t25Space + IsEmbedding.subtypeVal.t25Space end T25 @@ -2172,16 +2189,19 @@ instance (priority := 100) T3Space.t25Space [T3Space X] : T25Space X := by simp only [← disjoint_nhds_nhdsSet, nhdsSet_singleton] at this exact this.elim id fun h => h.symm -protected theorem Embedding.t3Space [TopologicalSpace Y] [T3Space Y] {f : X → Y} - (hf : Embedding f) : T3Space X := +protected theorem IsEmbedding.t3Space [TopologicalSpace Y] [T3Space Y] {f : X → Y} + (hf : IsEmbedding f) : T3Space X := { toT0Space := hf.t0Space toRegularSpace := hf.toInducing.regularSpace } +@[deprecated (since := "2024-10-26")] +alias Embedding.t3Space := IsEmbedding.t3Space + instance Subtype.t3Space [T3Space X] {p : X → Prop} : T3Space (Subtype p) := - embedding_subtype_val.t3Space + IsEmbedding.subtypeVal.t3Space instance ULift.instT3Space [T3Space X] : T3Space (ULift X) := - embedding_uLift_down.t3Space + IsEmbedding.uliftDown.t3Space instance [TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y) := ⟨⟩ @@ -2286,7 +2306,7 @@ theorem T4Space.of_compactSpace_t2Space [CompactSpace X] [T2Space X] : /-- If the codomain of a closed embedding is a T₄ space, then so is the domain. -/ protected theorem IsClosedEmbedding.t4Space [TopologicalSpace Y] [T4Space Y] {f : X → Y} (hf : IsClosedEmbedding f) : T4Space X where - toT1Space := hf.toEmbedding.t1Space + toT1Space := hf.isEmbedding.t1Space toNormalSpace := hf.normalSpace @[deprecated (since := "2024-10-20")] @@ -2330,8 +2350,8 @@ instance (priority := 100) CompletelyNormalSpace.toNormalSpace normal s t hs ht hd := separatedNhds_iff_disjoint.2 <| completely_normal (by rwa [hs.closure_eq]) (by rwa [ht.closure_eq]) -theorem Embedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y] {e : X → Y} - (he : Embedding e) : CompletelyNormalSpace X := by +theorem IsEmbedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y] + {e : X → Y} (he : IsEmbedding e) : CompletelyNormalSpace X := by refine ⟨fun s t hd₁ hd₂ => ?_⟩ simp only [he.toInducing.nhdsSet_eq_comap] refine disjoint_comap (completely_normal ?_ ?_) @@ -2340,24 +2360,30 @@ theorem Embedding.completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSp · rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl, ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right] +@[deprecated (since := "2024-10-26")] +alias Embedding.completelyNormalSpace := IsEmbedding.completelyNormalSpace + /-- A subspace of a completely normal space is a completely normal space. -/ instance [CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x // p x } := - embedding_subtype_val.completelyNormalSpace + IsEmbedding.subtypeVal.completelyNormalSpace instance ULift.instCompletelyNormalSpace [CompletelyNormalSpace X] : CompletelyNormalSpace (ULift X) := - embedding_uLift_down.completelyNormalSpace + IsEmbedding.uliftDown.completelyNormalSpace /-- A T₅ space is a completely normal T₁ space. -/ class T5Space (X : Type u) [TopologicalSpace X] extends T1Space X, CompletelyNormalSpace X : Prop -theorem Embedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : Embedding e) : - T5Space X where +theorem IsEmbedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y} + (he : IsEmbedding e) : T5Space X where __ := he.t1Space completely_normal := by - have := Embedding.completelyNormalSpace he + have := he.completelyNormalSpace exact completely_normal +@[deprecated (since := "2024-10-26")] +alias Embedding.t5Space := IsEmbedding.t5Space + -- see Note [lower instance priority] /-- A `T₅` space is a `T₄` space. -/ instance (priority := 100) T5Space.toT4Space [T5Space X] : T4Space X where @@ -2365,10 +2391,10 @@ instance (priority := 100) T5Space.toT4Space [T5Space X] : T4Space X where /-- A subspace of a T₅ space is a T₅ space. -/ instance [T5Space X] {p : X → Prop} : T5Space { x // p x } := - embedding_subtype_val.t5Space + IsEmbedding.subtypeVal.t5Space instance ULift.instT5Space [T5Space X] : T5Space (ULift X) := - embedding_uLift_down.t5Space + IsEmbedding.uliftDown.t5Space open SeparationQuotient @@ -2528,7 +2554,7 @@ theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] : refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.closed_iff_image_closed.1 VisClopen.1, ?_⟩ let v : Set u := ((↑) : u → s) ⁻¹' V have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl - have f0 : Embedding ((↑) : u → H) := embedding_subtype_val.comp embedding_subtype_val + have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal have f1 : IsOpenEmbedding ((↑) : u → H) := by refine ⟨f0, ?_⟩ · have : Set.range ((↑) : u → H) = interior s := by diff --git a/Mathlib/Topology/Sets/Opens.lean b/Mathlib/Topology/Sets/Opens.lean index 1252c062af227..8d8d697d4c8f2 100644 --- a/Mathlib/Topology/Sets/Opens.lean +++ b/Mathlib/Topology/Sets/Opens.lean @@ -250,11 +250,11 @@ theorem isOpenEmbedding' (U : Opens α) : IsOpenEmbedding (Subtype.val : U → alias openEmbedding' := isOpenEmbedding' theorem isOpenEmbedding_of_le {U V : Opens α} (i : U ≤ V) : - IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i) := - { toEmbedding := embedding_inclusion i - isOpen_range := by - rw [Set.range_inclusion i] - exact U.isOpen.preimage continuous_subtype_val } + IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i) where + toIsEmbedding := .inclusion i + isOpen_range := by + rw [Set.range_inclusion i] + exact U.isOpen.preimage continuous_subtype_val @[deprecated (since := "2024-10-18")] alias openEmbedding_of_le := isOpenEmbedding_of_le diff --git a/Mathlib/Topology/Sober.lean b/Mathlib/Topology/Sober.lean index 29cbe4476433a..e01eb8028eeb8 100644 --- a/Mathlib/Topology/Sober.lean +++ b/Mathlib/Topology/Sober.lean @@ -200,7 +200,7 @@ theorem IsOpenEmbedding.quasiSober {f : α → β} (hf : IsOpenEmbedding f) [Qua simpa using subset_closure use y change _ = _ - rw [hf.toEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx] + rw [hf.isEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx] apply image_injective.mpr hf.inj ext z simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff] diff --git a/Mathlib/Topology/Support.lean b/Mathlib/Topology/Support.lean index c533d9dbd075b..2a3e19012527f 100644 --- a/Mathlib/Topology/Support.lean +++ b/Mathlib/Topology/Support.lean @@ -205,7 +205,7 @@ theorem comp_isClosedEmbedding (hf : HasCompactMulSupport f) {g : α' → α} (hg : IsClosedEmbedding g) : HasCompactMulSupport (f ∘ g) := by rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage] refine IsCompact.of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure ?_ - rw [hg.toEmbedding.closure_eq_preimage_closure_image] + rw [hg.isEmbedding.closure_eq_preimage_closure_image] exact preimage_mono (closure_mono <| image_preimage_subset _ _) @[deprecated (since := "2024-10-20")] diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index 70735e4ee49a4..6cd8c7e9d7af5 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/Mathlib/Topology/TietzeExtension.lean @@ -70,7 +70,7 @@ function on `X₁` with values in a `TietzeExtension` space `Y`. Then there exis continuous function `g : C(X, Y)` such that `g ∘ e = f`. -/ theorem ContinuousMap.exists_extension (he : IsClosedEmbedding e) (f : C(X₁, Y)) : ∃ (g : C(X, Y)), g.comp ⟨e, he.continuous⟩ = f := by - let e' : X₁ ≃ₜ Set.range e := Homeomorph.ofEmbedding _ he.toEmbedding + let e' : X₁ ≃ₜ Set.range e := Homeomorph.ofIsEmbedding _ he.isEmbedding obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.isClosed_range exact ⟨g, by ext x; simpa using congr($(hg) ⟨e' x, x, rfl⟩)⟩ diff --git a/Mathlib/Topology/UniformSpace/CompleteSeparated.lean b/Mathlib/Topology/UniformSpace/CompleteSeparated.lean index cc34886c49d41..5c4968e5a26e8 100644 --- a/Mathlib/Topology/UniformSpace/CompleteSeparated.lean +++ b/Mathlib/Topology/UniformSpace/CompleteSeparated.lean @@ -30,7 +30,7 @@ theorem IsComplete.isClosed [UniformSpace α] [T0Space α] {s : Set α} (h : IsC theorem IsUniformEmbedding.toIsClosedEmbedding [UniformSpace α] [UniformSpace β] [CompleteSpace α] [T0Space β] {f : α → β} (hf : IsUniformEmbedding f) : IsClosedEmbedding f := - ⟨hf.embedding, hf.isUniformInducing.isComplete_range.isClosed⟩ + ⟨hf.isEmbedding, hf.isUniformInducing.isComplete_range.isClosed⟩ @[deprecated (since := "2024-10-20")] alias IsUniformEmbedding.toClosedEmbedding := IsUniformEmbedding.toIsClosedEmbedding diff --git a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean index 565e1e1a1e8be..f57caaac0a946 100644 --- a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean +++ b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean @@ -330,16 +330,20 @@ theorem isUniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β @[deprecated (since := "2024-10-01")] alias uniformEmbedding_of_spaced_out := isUniformEmbedding_of_spaced_out -protected lemma IsUniformEmbedding.embedding {f : α → β} (h : IsUniformEmbedding f) : Embedding f := - { toInducing := h.isUniformInducing.inducing - inj := h.inj } +protected lemma IsUniformEmbedding.isEmbedding {f : α → β} (h : IsUniformEmbedding f) : + IsEmbedding f where + toInducing := h.toIsUniformInducing.inducing + inj := h.inj + +@[deprecated (since := "2024-10-26")] +alias IsUniformEmbedding.embedding := IsUniformEmbedding.isEmbedding @[deprecated (since := "2024-10-01")] -alias UniformEmbedding.embedding := IsUniformEmbedding.embedding +alias UniformEmbedding.embedding := IsUniformEmbedding.isEmbedding theorem IsUniformEmbedding.isDenseEmbedding {f : α → β} (h : IsUniformEmbedding f) (hd : DenseRange f) : IsDenseEmbedding f := - { h.embedding with dense := hd } + { h.isEmbedding with dense := hd } @[deprecated (since := "2024-10-01")] alias UniformEmbedding.isDenseEmbedding := IsUniformEmbedding.isDenseEmbedding @@ -352,7 +356,7 @@ theorem isClosedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopo (hf : Pairwise fun x y => (f x, f y) ∉ s) : IsClosedEmbedding f := by rcases @DiscreteTopology.eq_bot α _ _ with rfl; let _ : UniformSpace α := ⊥ exact - { (isUniformEmbedding_of_spaced_out hs hf).embedding with + { (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with isClosed_range := isClosed_range_of_spaced_out hs hf } @[deprecated (since := "2024-10-20")] @@ -557,12 +561,15 @@ alias uniformEmbedding_comap := isUniformEmbedding_comap /-- Pull back a uniform space structure by an embedding, adjusting the new uniform structure to make sure that its topology is defeq to the original one. -/ -def Embedding.comapUniformSpace {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) - (h : Embedding f) : UniformSpace α := +def IsEmbedding.comapUniformSpace {α β} [TopologicalSpace α] [u : UniformSpace β] + (f : α → β) (h : IsEmbedding f) : UniformSpace α := (u.comap f).replaceTopology h.induced +@[deprecated (since := "2024-10-26")] +alias Embedding.comapUniformSpace := IsEmbedding.comapUniformSpace + theorem Embedding.to_isUniformEmbedding {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) - (h : Embedding f) : @IsUniformEmbedding α β (h.comapUniformSpace f) u f := + (h : IsEmbedding f) : @IsUniformEmbedding α β (h.comapUniformSpace f) u f := let _ := h.comapUniformSpace f { comap_uniformity := rfl inj := h.inj } diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt index ddd9bf20bcedc..4ba393b331441 100644 --- a/scripts/no_lints_prime_decls.txt +++ b/scripts/no_lints_prime_decls.txt @@ -1122,7 +1122,7 @@ EllipticCurve.coe_inv_variableChange_Δ' EllipticCurve.coe_map_Δ' EllipticCurve.coe_variableChange_Δ' em' -Embedding.mk' +IsEmbedding.mk' EMetric.diam_pos_iff' EMetric.diam_union' EMetric.mem_ball'