From 3ca1060d7e48260d1b1b7a0733f887e455455226 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 3 Oct 2024 20:47:20 +0000 Subject: [PATCH] chore: Rename `UniformEmbedding` to `IsUniformEmbedding` (#17295) `Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards 1. renaming `Embedding` to `IsEmbedding` and similarly for neighborhing declarations (which `DenseEmbedding` is) 2. namespacing it inside `Topology` [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rename.20.60Inducing.60.20and.20.60Embedding.60.3F). See #15993 for context. --- .../Instances.lean | 24 +-- .../NonUnital.lean | 2 +- .../Restrict.lean | 30 +-- Mathlib/Analysis/CStarAlgebra/Multiplier.lean | 10 +- Mathlib/Analysis/Complex/Basic.lean | 9 +- .../InnerProductSpace/LinearPMap.lean | 2 +- .../Analysis/Normed/Algebra/Unitization.lean | 7 +- .../Normed/Algebra/UnitizationL1.lean | 2 +- .../Normed/Operator/ContinuousLinearMap.lean | 10 +- .../OperatorNorm/Completeness.lean | 2 +- Mathlib/Analysis/Quaternion.lean | 4 +- Mathlib/MeasureTheory/Function/LpSpace.lean | 2 +- .../Function/SimpleFuncDenseLp.lean | 10 +- .../Integral/IntegralEqImproper.lean | 4 +- .../MeasureTheory/Integral/SetIntegral.lean | 2 +- .../Algebra/Module/Alternating/Topology.lean | 34 ++-- Mathlib/Topology/Algebra/Module/Basic.lean | 17 +- .../Algebra/Module/FiniteDimension.lean | 6 +- .../Algebra/Module/Multilinear/Topology.lean | 32 +-- .../Algebra/Module/StrongTopology.lean | 38 ++-- .../Topology/Algebra/SeparationQuotient.lean | 5 +- Mathlib/Topology/Algebra/UniformField.lean | 6 +- Mathlib/Topology/Algebra/UniformGroup.lean | 5 +- Mathlib/Topology/ContinuousMap/Bounded.lean | 4 +- Mathlib/Topology/ContinuousMap/Compact.lean | 7 +- .../ContinuousMap/ContinuousMapZero.lean | 32 +-- Mathlib/Topology/EMetricSpace/Basic.lean | 26 ++- Mathlib/Topology/EMetricSpace/Defs.lean | 2 +- Mathlib/Topology/Instances/Int.lean | 9 +- Mathlib/Topology/Instances/Nat.lean | 9 +- Mathlib/Topology/Instances/PNat.lean | 5 +- Mathlib/Topology/Instances/Rat.lean | 27 ++- .../Topology/MetricSpace/Antilipschitz.lean | 9 +- Mathlib/Topology/MetricSpace/Basic.lean | 25 ++- Mathlib/Topology/MetricSpace/Closeds.lean | 13 +- Mathlib/Topology/MetricSpace/Dilation.lean | 10 +- Mathlib/Topology/MetricSpace/Isometry.lean | 15 +- .../Topology/MetricSpace/Pseudo/Basic.lean | 17 +- Mathlib/Topology/UniformSpace/Ascoli.lean | 3 +- Mathlib/Topology/UniformSpace/Basic.lean | 2 +- .../UniformSpace/CompactConvergence.lean | 37 ++-- .../Topology/UniformSpace/CompareReals.lean | 2 +- .../UniformSpace/CompleteSeparated.lean | 7 +- Mathlib/Topology/UniformSpace/Completion.lean | 14 +- Mathlib/Topology/UniformSpace/Equiv.lean | 12 +- .../UniformConvergenceTopology.lean | 15 +- .../UniformSpace/UniformEmbedding.lean | 185 ++++++++++++------ scripts/no_lints_prime_decls.txt | 4 +- 48 files changed, 479 insertions(+), 275 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean index d1e7e6f1539c8..a085109299f03 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean @@ -218,7 +218,7 @@ lemma QuasispectrumRestricts.isSelfAdjoint (a : A) (ha : QuasispectrumRestricts instance IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop) := QuasispectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM - Complex.isometry_ofReal.uniformEmbedding (.zero _) + Complex.isometry_ofReal.isUniformEmbedding (.zero _) (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts) end SelfAdjointNonUnital @@ -264,7 +264,7 @@ lemma SpectrumRestricts.isSelfAdjoint (a : A) (ha : SpectrumRestricts a Complex. instance IsSelfAdjoint.instContinuousFunctionalCalculus : ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop) := SpectrumRestricts.cfc (q := IsStarNormal) (p := IsSelfAdjoint) Complex.reCLM - Complex.isometry_ofReal.uniformEmbedding (.zero _) + Complex.isometry_ofReal.isUniformEmbedding (.zero _) (fun _ ↦ isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts) lemma IsSelfAdjoint.spectrum_nonempty {A : Type*} [Ring A] [StarRing A] @@ -313,7 +313,7 @@ open NNReal in instance Nonneg.instNonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus ℝ≥0 (fun x : A ↦ 0 ≤ x) := QuasispectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal - uniformEmbedding_subtype_val le_rfl + isUniformEmbedding_subtype_val le_rfl (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts) open NNReal in @@ -359,7 +359,7 @@ open NNReal in instance Nonneg.instContinuousFunctionalCalculus : ContinuousFunctionalCalculus ℝ≥0 (fun x : A ↦ 0 ≤ x) := SpectrumRestricts.cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal - uniformEmbedding_subtype_val le_rfl (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts) + isUniformEmbedding_subtype_val le_rfl (fun _ ↦ nonneg_iff_isSelfAdjoint_and_spectrumRestricts) end Nonneg @@ -605,14 +605,14 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] lemma cfcHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) : cfcHom ha = ha.spectrumRestricts.starAlgHom (cfcHom ha.isStarNormal) (f := Complex.reCLM) := - ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding + ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal lemma cfc_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : cfc f a = cfc (fun x ↦ f x.re : ℂ → ℂ) a := by replace ha : IsSelfAdjoint a := ha -- hack to avoid issues caused by autoParam exact ha.spectrumRestricts.cfc_eq_restrict (f := Complex.reCLM) - Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal f + Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f end RealEqComplex @@ -626,14 +626,14 @@ variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module lemma cfcₙHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) : cfcₙHom ha = (ha.quasispectrumRestricts.2).nonUnitalStarAlgHom (cfcₙHom ha.isStarNormal) (f := Complex.reCLM) := - ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding + ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal lemma cfcₙ_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : cfcₙ f a = cfcₙ (fun x ↦ f x.re : ℂ → ℂ) a := by replace ha : IsSelfAdjoint a := ha -- hack to avoid issues caused by autoParam exact ha.quasispectrumRestricts.2.cfcₙ_eq_restrict (f := Complex.reCLM) - Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal f + Complex.isometry_ofReal.isUniformEmbedding ha ha.isStarNormal f end RealEqComplexNonUnital @@ -650,13 +650,13 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] lemma cfcHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) : cfcHom ha = (SpectrumRestricts.nnreal_of_nonneg ha).starAlgHom (cfcHom (IsSelfAdjoint.of_nonneg ha)) := by - apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict uniformEmbedding_subtype_val + apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict isUniformEmbedding_subtype_val lemma cfc_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac) : cfc f a = cfc (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict - uniformEmbedding_subtype_val ha (.of_nonneg ha) + isUniformEmbedding_subtype_val ha (.of_nonneg ha) end NNRealEqReal @@ -675,13 +675,13 @@ lemma cfcₙHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) : cfcₙHom ha = (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) := by apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict - uniformEmbedding_subtype_val + isUniformEmbedding_subtype_val lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac) : cfcₙ f a = cfcₙ (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict - uniformEmbedding_subtype_val ha (.of_nonneg ha) + isUniformEmbedding_subtype_val ha (.of_nonneg ha) end NNRealEqRealNonUnital diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean index 3ebb272f0dee6..3bcd0795b06d8 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean @@ -692,7 +692,7 @@ lemma closedEmbedding_cfcₙHom_of_cfcHom {a : A} (ha : p a) : let f : C(spectrum R a, σₙ R a) := ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum R a⟩ refine (cfcHom_closedEmbedding ha).comp <| - (UniformInducing.uniformEmbedding ⟨?_⟩).toClosedEmbedding + (UniformInducing.isUniformEmbedding ⟨?_⟩).toClosedEmbedding have := uniformSpace_eq_inf_precomp_of_cover (β := R) f (0 : C(Unit, σₙ R a)) (map_continuous f).isProperMap (map_continuous 0).isProperMap <| by simp only [← Subtype.val_injective.image_injective.eq_iff, f, ContinuousMap.coe_mk, diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean index 9a2bf73293ea6..cf36028a7922e 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean @@ -84,17 +84,17 @@ variable [CompleteSpace R] lemma closedEmbedding_starAlgHom {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A} (hφ : ClosedEmbedding φ) {f : C(S, R)} (h : SpectrumRestricts a f) - (halg : UniformEmbedding (algebraMap R S)) : + (halg : IsUniformEmbedding (algebraMap R S)) : ClosedEmbedding (h.starAlgHom φ) := - hφ.comp <| UniformEmbedding.toClosedEmbedding <| .comp - (ContinuousMap.uniformEmbedding_comp _ halg) - (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.uniformEmbedding) + hφ.comp <| IsUniformEmbedding.toClosedEmbedding <| .comp + (ContinuousMap.isUniformEmbedding_comp _ halg) + (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.isUniformEmbedding) /-- Given a `ContinuousFunctionalCalculus S q`. If we form the predicate `p` for `a : A` characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via `f : C(S, R)`, then we can get a restricted functional calculus `ContinuousFunctionalCalculus R p`. -/ -protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (h0 : p 0) +protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0) (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) : ContinuousFunctionalCalculus R p where predicate_zero := h0 @@ -133,14 +133,14 @@ protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) ( variable [ContinuousFunctionalCalculus R p] [UniqueContinuousFunctionalCalculus R A] -lemma cfcHom_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) +lemma cfcHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) : cfcHom hpa = h.starAlgHom (cfcHom hqa) := by apply cfcHom_eq_of_continuous_of_map_id · exact h.closedEmbedding_starAlgHom (cfcHom_closedEmbedding hqa) halg |>.continuous · exact h.starAlgHom_id (cfcHom_id hqa) -lemma cfc_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) +lemma cfc_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) (g : R → R) : cfc g a = cfc (fun x ↦ algebraMap R S (g (f x))) a := by by_cases hg : ContinuousOn g (spectrum R a) @@ -218,12 +218,12 @@ variable [CompleteSpace R] lemma closedEmbedding_nonUnitalStarAlgHom {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A} (hφ : ClosedEmbedding φ) {f : C(S, R)} (h : QuasispectrumRestricts a f) - (halg : UniformEmbedding (algebraMap R S)) : + (halg : IsUniformEmbedding (algebraMap R S)) : ClosedEmbedding (h.nonUnitalStarAlgHom φ) := by have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _) - refine hφ.comp <| UniformEmbedding.toClosedEmbedding <| .comp - (ContinuousMapZero.uniformEmbedding_comp _ halg) - (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.uniformEmbedding) + refine hφ.comp <| IsUniformEmbedding.toClosedEmbedding <| .comp + (ContinuousMapZero.isUniformEmbedding_comp _ halg) + (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding) variable [IsScalarTower R A A] [SMulCommClass R A A] @@ -231,7 +231,7 @@ variable [IsScalarTower R A A] [SMulCommClass R A A] characterized by: `q a` and the quasispectrum of `a` restricts to the scalar subring `R` via `f : C(S, R)`, then we can get a restricted functional calculus `NonUnitalContinuousFunctionalCalculus R p`. -/ -protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) (h0 : p 0) +protected theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0) (h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) : NonUnitalContinuousFunctionalCalculus R p where predicate_zero := h0 @@ -275,15 +275,15 @@ protected theorem cfc (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) ( variable [NonUnitalContinuousFunctionalCalculus R p] variable [UniqueNonUnitalContinuousFunctionalCalculus R A] -lemma cfcₙHom_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} +lemma cfcₙHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) : cfcₙHom hpa = h.nonUnitalStarAlgHom (cfcₙHom hqa) := by apply cfcₙHom_eq_of_continuous_of_map_id · exact h.closedEmbedding_nonUnitalStarAlgHom (cfcₙHom_closedEmbedding hqa) halg |>.continuous · exact h.nonUnitalStarAlgHom_id (cfcₙHom_id hqa) -lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : UniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) - (hqa : q a) (h : QuasispectrumRestricts a f) (g : R → R) : +lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} + (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) (g : R → R) : cfcₙ g a = cfcₙ (fun x ↦ algebraMap R S (g (f x))) a := by by_cases hg : ContinuousOn g (σₙ R a) ∧ g 0 = 0 · obtain ⟨hg, hg0⟩ := hg diff --git a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean b/Mathlib/Analysis/CStarAlgebra/Multiplier.lean index 248d3fa9e31ac..d9c622e26c2c4 100644 --- a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean +++ b/Mathlib/Analysis/CStarAlgebra/Multiplier.lean @@ -534,11 +534,15 @@ instance instNormedSpace : NormedSpace 𝕜 𝓜(𝕜, A) := instance instNormedAlgebra : NormedAlgebra 𝕜 𝓜(𝕜, A) := { DoubleCentralizer.instAlgebra, DoubleCentralizer.instNormedSpace with } -theorem uniformEmbedding_toProdMulOpposite : UniformEmbedding (@toProdMulOpposite 𝕜 A _ _ _ _ _) := - uniformEmbedding_comap toProdMulOpposite_injective +theorem isUniformEmbedding_toProdMulOpposite : + IsUniformEmbedding (toProdMulOpposite (𝕜 := 𝕜) (A := A)) := + isUniformEmbedding_comap toProdMulOpposite_injective + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toProdMulOpposite := isUniformEmbedding_toProdMulOpposite instance [CompleteSpace A] : CompleteSpace 𝓜(𝕜, A) := by - rw [completeSpace_iff_isComplete_range uniformEmbedding_toProdMulOpposite.toUniformInducing] + rw [completeSpace_iff_isComplete_range isUniformEmbedding_toProdMulOpposite.toUniformInducing] apply IsClosed.isComplete simp only [range_toProdMulOpposite, Set.setOf_forall] refine isClosed_iInter fun x => isClosed_iInter fun y => isClosed_eq ?_ ?_ diff --git a/Mathlib/Analysis/Complex/Basic.lean b/Mathlib/Analysis/Complex/Basic.lean index 28550b2fd6baa..b2b77580329f5 100644 --- a/Mathlib/Analysis/Complex/Basic.lean +++ b/Mathlib/Analysis/Complex/Basic.lean @@ -208,11 +208,14 @@ theorem antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) equivRea AddMonoidHomClass.antilipschitz_of_bound equivRealProdLm fun z ↦ by simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using abs_le_sqrt_two_mul_max z -theorem uniformEmbedding_equivRealProd : UniformEmbedding equivRealProd := - antilipschitz_equivRealProd.uniformEmbedding lipschitz_equivRealProd.uniformContinuous +theorem isUniformEmbedding_equivRealProd : IsUniformEmbedding equivRealProd := + antilipschitz_equivRealProd.isUniformEmbedding lipschitz_equivRealProd.uniformContinuous + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_equivRealProd := isUniformEmbedding_equivRealProd instance : CompleteSpace ℂ := - (completeSpace_congr uniformEmbedding_equivRealProd).mpr inferInstance + (completeSpace_congr isUniformEmbedding_equivRealProd).mpr inferInstance instance instT2Space : T2Space ℂ := TopologicalSpace.t2Space_of_metrizableSpace diff --git a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean index 4fa2bc6e39428..4ab4ac3e7b9f6 100644 --- a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean +++ b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean @@ -103,7 +103,7 @@ variable (hT : Dense (T.domain : Set E)) /-- The unique continuous extension of the operator `adjointDomainMkCLM` to `E`. -/ def adjointDomainMkCLMExtend (y : T.adjointDomain) : E →L[𝕜] 𝕜 := (T.adjointDomainMkCLM y).extend (Submodule.subtypeL T.domain) hT.denseRange_val - uniformEmbedding_subtype_val.toUniformInducing + isUniformEmbedding_subtype_val.toUniformInducing @[simp] theorem adjointDomainMkCLMExtend_apply (y : T.adjointDomain) (x : T.domain) : diff --git a/Mathlib/Analysis/Normed/Algebra/Unitization.lean b/Mathlib/Analysis/Normed/Algebra/Unitization.lean index 8b5d489952f9a..19b11e9819409 100644 --- a/Mathlib/Analysis/Normed/Algebra/Unitization.lean +++ b/Mathlib/Analysis/Normed/Algebra/Unitization.lean @@ -208,11 +208,14 @@ def uniformEquivProd : (Unitization 𝕜 A) ≃ᵤ (𝕜 × A) := instance instBornology : Bornology (Unitization 𝕜 A) := Bornology.induced <| addEquiv 𝕜 A -theorem uniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] : - UniformEmbedding (addEquiv 𝕜 A) where +theorem isUniformEmbedding_addEquiv {𝕜} [NontriviallyNormedField 𝕜] : + IsUniformEmbedding (addEquiv 𝕜 A) where comap_uniformity := rfl inj := (addEquiv 𝕜 A).injective +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_addEquiv := isUniformEmbedding_addEquiv + /-- `Unitization 𝕜 A` is complete whenever `𝕜` and `A` are also. -/ instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] : CompleteSpace (Unitization 𝕜 A) := diff --git a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean index 4a0ab143ce2a1..bb8f42626297c 100644 --- a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean +++ b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean @@ -50,7 +50,7 @@ noncomputable def uniformEquiv_unitization_addEquiv_prod : instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] : CompleteSpace (WithLp 1 (Unitization 𝕜 A)) := - completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).uniformEmbedding |>.mpr + completeSpace_congr (uniformEquiv_unitization_addEquiv_prod 𝕜 A).isUniformEmbedding |>.mpr CompleteSpace.prod variable {𝕜 A} diff --git a/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean b/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean index eedbaba72b905..64c5ba0eb60b5 100644 --- a/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean +++ b/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean @@ -153,9 +153,13 @@ variable [Ring 𝕜] [Ring 𝕜₂] variable [NormedAddCommGroup E] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] variable {σ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ] F) (x y z : E) -theorem ContinuousLinearMap.uniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) : - UniformEmbedding f := - (AddMonoidHomClass.antilipschitz_of_bound f hf).uniformEmbedding f.uniformContinuous +theorem ContinuousLinearMap.isUniformEmbedding_of_bound {K : ℝ≥0} (hf : ∀ x, ‖x‖ ≤ K * ‖f x‖) : + IsUniformEmbedding f := + (AddMonoidHomClass.antilipschitz_of_bound f hf).isUniformEmbedding f.uniformContinuous + +@[deprecated (since := "2024-10-01")] +alias ContinuousLinearMap.uniformEmbedding_of_bound := + ContinuousLinearMap.isUniformEmbedding_of_bound end Normed diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean index 716b0f8e64316..9c9517852f03e 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean @@ -230,7 +230,7 @@ variable {N : ℝ≥0} (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) [RingHomIsometri /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the norm of the extension of `f` along `e` is bounded by `N * ‖f‖`. -/ theorem opNorm_extend_le : - ‖f.extend e h_dense (uniformEmbedding_of_bound _ h_e).toUniformInducing‖ ≤ N * ‖f‖ := by + ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).toUniformInducing‖ ≤ N * ‖f‖ := by -- Add `opNorm_le_of_dense`? refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_) · cases le_total 0 N with diff --git a/Mathlib/Analysis/Quaternion.lean b/Mathlib/Analysis/Quaternion.lean index e342a1859bb60..3466df2251849 100644 --- a/Mathlib/Analysis/Quaternion.lean +++ b/Mathlib/Analysis/Quaternion.lean @@ -195,8 +195,8 @@ theorem continuous_im : Continuous fun q : ℍ => q.im := by simpa only [← sub_self_re] using continuous_id.sub (continuous_coe.comp continuous_re) instance : CompleteSpace ℍ := - haveI : UniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm := - linearIsometryEquivTuple.toContinuousLinearEquiv.symm.uniformEmbedding + haveI : IsUniformEmbedding linearIsometryEquivTuple.toLinearEquiv.toEquiv.symm := + linearIsometryEquivTuple.toContinuousLinearEquiv.symm.isUniformEmbedding (completeSpace_congr this).1 inferInstance section infinite_sum diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index ed9015bf0ac57..5410247494af6 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'.uniformEmbedding hg).embedding.aestronglyMeasurable_comp_iff.1 hL.1 + (hg'.isUniformEmbedding hg).embedding.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/SimpleFuncDenseLp.lean b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean index 29f9a7d7b2d9b..72dd2f1509641 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean @@ -679,16 +679,18 @@ variable [Fact (1 ≤ p)] protected theorem uniformContinuous : UniformContinuous ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := uniformContinuous_comap -protected theorem uniformEmbedding : UniformEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := - uniformEmbedding_comap Subtype.val_injective +lemma isUniformEmbedding : IsUniformEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := + isUniformEmbedding_comap Subtype.val_injective + +@[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding protected theorem uniformInducing : UniformInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := - simpleFunc.uniformEmbedding.toUniformInducing + simpleFunc.isUniformEmbedding.toUniformInducing lemma isDenseEmbedding (hp_ne_top : p ≠ ∞) : IsDenseEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) := by borelize E - apply simpleFunc.uniformEmbedding.isDenseEmbedding + apply simpleFunc.isUniformEmbedding.isDenseEmbedding intro f rw [mem_closure_iff_seq_limit] have hfi' : Memℒp f p μ := Lp.memℒp f diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean index 902812d6d999d..ac2ffb0b0ce8f 100644 --- a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean +++ b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean @@ -712,7 +712,7 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi rw [← top_le_iff, ← volume_Ici (a := b)] exact measure_mono hb rwa [B, ← Embedding.tendsto_nhds_iff] at A - exact (Completion.uniformEmbedding_coe E).embedding + exact (Completion.isUniformEmbedding_coe E).embedding variable [CompleteSpace E] @@ -909,7 +909,7 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Iic rw [← volume_Iic (a := b)] exact measure_mono hb rwa [B, ← Embedding.tendsto_nhds_iff] at A - exact (Completion.uniformEmbedding_coe E).embedding + exact (Completion.isUniformEmbedding_coe E).embedding variable [CompleteSpace E] diff --git a/Mathlib/MeasureTheory/Integral/SetIntegral.lean b/Mathlib/MeasureTheory/Integral/SetIntegral.lean index 4af2e6de396cb..be099131dfc9b 100644 --- a/Mathlib/MeasureTheory/Integral/SetIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/SetIntegral.lean @@ -1260,7 +1260,7 @@ variable [NormedSpace ℝ F] [NormedSpace ℝ E] theorem integral_comp_comm (L : E ≃L[𝕜] F) (φ : X → E) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) := by have : CompleteSpace E ↔ CompleteSpace F := - completeSpace_congr (e := L.toEquiv) L.uniformEmbedding + completeSpace_congr (e := L.toEquiv) L.isUniformEmbedding obtain ⟨_, _⟩|⟨_, _⟩ := iff_iff_and_or_not_and_not.mp this · exact L.toContinuousLinearMap.integral_comp_comm' L.antilipschitz _ · simp [integral, *] diff --git a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean index 747f1739055fe..9f613d081db1f 100644 --- a/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean +++ b/Mathlib/Topology/Algebra/Module/Alternating/Topology.lean @@ -47,14 +47,17 @@ variable [UniformSpace F] [UniformAddGroup F] instance instUniformSpace : UniformSpace (E [⋀^ι]→L[𝕜] F) := .comap toContinuousMultilinearMap inferInstance -lemma uniformEmbedding_toContinuousMultilinearMap : - UniformEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → _) where +lemma isUniformEmbedding_toContinuousMultilinearMap : + IsUniformEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → _) where inj := toContinuousMultilinearMap_injective comap_uniformity := rfl +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toContinuousMultilinearMap := isUniformEmbedding_toContinuousMultilinearMap + lemma uniformContinuous_toContinuousMultilinearMap : UniformContinuous (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → _) := - uniformEmbedding_toContinuousMultilinearMap.uniformContinuous + isUniformEmbedding_toContinuousMultilinearMap.uniformContinuous theorem uniformContinuous_coe_fun [ContinuousSMul 𝕜 E] : UniformContinuous (DFunLike.coe : (E [⋀^ι]→L[𝕜] F) → (ι → E) → F) := @@ -66,13 +69,13 @@ theorem uniformContinuous_eval_const [ContinuousSMul 𝕜 E] (x : ι → E) : uniformContinuous_pi.1 uniformContinuous_coe_fun x instance instUniformAddGroup : UniformAddGroup (E [⋀^ι]→L[𝕜] F) := - uniformEmbedding_toContinuousMultilinearMap.uniformAddGroup + isUniformEmbedding_toContinuousMultilinearMap.uniformAddGroup (toContinuousMultilinearMapLinear (R := ℕ)) instance instUniformContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : UniformContinuousConstSMul M (E [⋀^ι]→L[𝕜] F) := - uniformEmbedding_toContinuousMultilinearMap.uniformContinuousConstSMul fun _ _ ↦ rfl + isUniformEmbedding_toContinuousMultilinearMap.uniformContinuousConstSMul fun _ _ ↦ rfl section CompleteSpace @@ -83,7 +86,7 @@ theorem completeSpace (h : RestrictGenTopology {s : Set (ι → E) | IsVonNBound CompleteSpace (E [⋀^ι]→L[𝕜] F) := by have := ContinuousMultilinearMap.completeSpace (F := F) h rw [completeSpace_iff_isComplete_range - uniformEmbedding_toContinuousMultilinearMap.toUniformInducing] + isUniformEmbedding_toContinuousMultilinearMap.toUniformInducing] apply isClosed_range_toContinuousMultilinearMap.isComplete instance instCompleteSpace [TopologicalAddGroup E] [SequentialSpace (ι → E)] : @@ -97,15 +100,18 @@ section RestrictScalars variable (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [ContinuousSMul 𝕜 E] -theorem uniformEmbedding_restrictScalars : - UniformEmbedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := by - rw [← uniformEmbedding_toContinuousMultilinearMap.of_comp_iff] - exact (ContinuousMultilinearMap.uniformEmbedding_restrictScalars 𝕜').comp - uniformEmbedding_toContinuousMultilinearMap +theorem isUniformEmbedding_restrictScalars : + IsUniformEmbedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := by + rw [← isUniformEmbedding_toContinuousMultilinearMap.of_comp_iff] + exact (ContinuousMultilinearMap.isUniformEmbedding_restrictScalars 𝕜').comp + isUniformEmbedding_toContinuousMultilinearMap + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_restrictScalars := isUniformEmbedding_restrictScalars theorem uniformContinuous_restrictScalars : UniformContinuous (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := - (uniformEmbedding_restrictScalars 𝕜').uniformContinuous + (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous end RestrictScalars @@ -117,7 +123,7 @@ lemma embedding_toContinuousMultilinearMap : Embedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) := letI := TopologicalAddGroup.toUniformSpace F haveI := comm_topologicalAddGroup_is_uniform (G := F) - uniformEmbedding_toContinuousMultilinearMap.embedding + isUniformEmbedding_toContinuousMultilinearMap.embedding @[continuity, fun_prop] lemma continuous_toContinuousMultilinearMap : @@ -179,7 +185,7 @@ theorem embedding_restrictScalars : Embedding (restrictScalars 𝕜' : E [⋀^ι]→L[𝕜] F → E [⋀^ι]→L[𝕜'] F) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (uniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).embedding @[continuity, fun_prop] theorem continuous_restrictScalars : diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 99adb17d2c59c..76d6e898d399b 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -1942,22 +1942,27 @@ protected theorem preimage_symm_preimage (e : M₁ ≃SL[σ₁₂] M₂) (s : Se e ⁻¹' (e.symm ⁻¹' s) = s := e.symm.symm_preimage_preimage s -protected theorem uniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] +lemma isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [UniformAddGroup E₁] - [UniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) : UniformEmbedding e := - e.toLinearEquiv.toEquiv.uniformEmbedding e.toContinuousLinearMap.uniformContinuous + [UniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) : IsUniformEmbedding e := + e.toLinearEquiv.toEquiv.isUniformEmbedding e.toContinuousLinearMap.uniformContinuous e.symm.toContinuousLinearMap.uniformContinuous -protected theorem _root_.LinearEquiv.uniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] +@[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding + +protected theorem _root_.LinearEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [UniformAddGroup E₁] [UniformAddGroup E₂] (e : E₁ ≃ₛₗ[σ₁₂] E₂) - (h₁ : Continuous e) (h₂ : Continuous e.symm) : UniformEmbedding e := - ContinuousLinearEquiv.uniformEmbedding + (h₁ : Continuous e) (h₂ : Continuous e.symm) : IsUniformEmbedding e := + ContinuousLinearEquiv.isUniformEmbedding ({ e with continuous_toFun := h₁ continuous_invFun := h₂ } : E₁ ≃SL[σ₁₂] E₂) +@[deprecated (since := "2024-10-01")] +alias _root_.LinearEquiv.uniformEmbedding := _root_.LinearEquiv.isUniformEmbedding + /-- Create a `ContinuousLinearEquiv` from two `ContinuousLinearMap`s that are inverse of each other. -/ def equivOfInverse (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁) (h₁ : Function.LeftInverse f₂ f₁) diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 3c7e1401aa012..2cf817161d306 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -204,13 +204,13 @@ private theorem continuous_equivFun_basis_aux [T2Space E] {ι : Type v} [Fintype intro s s_dim letI : UniformAddGroup s := s.toAddSubgroup.uniformAddGroup let b := Basis.ofVectorSpace 𝕜 s - have U : UniformEmbedding b.equivFun.symm.toEquiv := by + have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by rw [← s_dim] exact (finrank_eq_card_basis b).symm have : Continuous b.equivFun := IH b this exact - b.equivFun.symm.uniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this + b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this have : IsComplete (s : Set E) := completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance) exact this.isClosed @@ -490,7 +490,7 @@ variable (𝕜 E : Type*) [NontriviallyNormedField 𝕜] include 𝕜 in theorem FiniteDimensional.complete [FiniteDimensional 𝕜 E] : CompleteSpace E := by set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm - have : UniformEmbedding e.toEquiv.symm := e.symm.uniformEmbedding + have : IsUniformEmbedding e.toEquiv.symm := e.symm.isUniformEmbedding exact (completeSpace_congr this).1 inferInstance variable {𝕜 E} diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean index a403ef7dca6bd..c73eb8c4be001 100644 --- a/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean +++ b/Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean @@ -65,18 +65,21 @@ section UniformAddGroup variable [UniformSpace F] [UniformAddGroup F] -lemma uniformEmbedding_toUniformOnFun : - UniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) where +lemma isUniformEmbedding_toUniformOnFun : + IsUniformEmbedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) where inj := DFunLike.coe_injective comap_uniformity := rfl +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toUniformOnFun := isUniformEmbedding_toUniformOnFun + lemma embedding_toUniformOnFun : Embedding (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → _) := - uniformEmbedding_toUniformOnFun.embedding + isUniformEmbedding_toUniformOnFun.embedding theorem uniformContinuous_coe_fun [∀ i, ContinuousSMul 𝕜 (E i)] : UniformContinuous (DFunLike.coe : ContinuousMultilinearMap 𝕜 E F → (Π i, E i) → F) := (UniformOnFun.uniformContinuous_toFun isVonNBounded_covers).comp - uniformEmbedding_toUniformOnFun.uniformContinuous + isUniformEmbedding_toUniformOnFun.uniformContinuous theorem uniformContinuous_eval_const [∀ i, ContinuousSMul 𝕜 (E i)] (x : Π i, E i) : UniformContinuous fun f : ContinuousMultilinearMap 𝕜 E F ↦ f x := @@ -85,13 +88,13 @@ theorem uniformContinuous_eval_const [∀ i, ContinuousSMul 𝕜 (E i)] (x : Π instance instUniformAddGroup : UniformAddGroup (ContinuousMultilinearMap 𝕜 E F) := let φ : ContinuousMultilinearMap 𝕜 E F →+ (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F := { toFun := toUniformOnFun, map_add' := fun _ _ ↦ rfl, map_zero' := rfl } - uniformEmbedding_toUniformOnFun.uniformAddGroup φ + isUniformEmbedding_toUniformOnFun.uniformAddGroup φ instance instUniformContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F] [ContinuousConstSMul M F] : UniformContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) := haveI := uniformContinuousConstSMul_of_continuousConstSMul M F - uniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl + isUniformEmbedding_toUniformOnFun.uniformContinuousConstSMul fun _ _ ↦ rfl section CompleteSpace @@ -104,7 +107,7 @@ theorem completeSpace (h : RestrictGenTopology {s : Set (Π i, E i) | IsVonNBoun have H : ∀ {m : Π i, E i}, Continuous fun f : (Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F ↦ toFun _ f m := (uniformContinuous_eval (isVonNBounded_covers) _).continuous - rw [completeSpace_iff_isComplete_range uniformEmbedding_toUniformOnFun.toUniformInducing, + rw [completeSpace_iff_isComplete_range isUniformEmbedding_toUniformOnFun.toUniformInducing, range_toUniformOnFun] simp only [setOf_and, setOf_forall] apply_rules [IsClosed.isComplete, IsClosed.inter] @@ -126,19 +129,22 @@ variable (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' [∀ i, Module 𝕜' (E i)] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] [∀ i, ContinuousSMul 𝕜 (E i)] -theorem uniformEmbedding_restrictScalars : - UniformEmbedding +theorem isUniformEmbedding_restrictScalars : + IsUniformEmbedding (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := by letI : NontriviallyNormedField 𝕜 := ⟨let ⟨x, hx⟩ := @NontriviallyNormedField.non_trivial 𝕜' _; ⟨algebraMap 𝕜' 𝕜 x, by simpa⟩⟩ - rw [← uniformEmbedding_toUniformOnFun.of_comp_iff] - convert uniformEmbedding_toUniformOnFun using 4 with s + rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff] + convert isUniformEmbedding_toUniformOnFun using 4 with s exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩ +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_restrictScalars := isUniformEmbedding_restrictScalars + theorem uniformContinuous_restrictScalars : UniformContinuous (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := - (uniformEmbedding_restrictScalars 𝕜').uniformContinuous + (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous end RestrictScalars @@ -207,7 +213,7 @@ theorem embedding_restrictScalars : (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (uniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).embedding @[continuity, fun_prop] theorem continuous_restrictScalars : diff --git a/Mathlib/Topology/Algebra/Module/StrongTopology.lean b/Mathlib/Topology/Algebra/Module/StrongTopology.lean index 437453ea31e0d..6bb9968ff157e 100644 --- a/Mathlib/Topology/Algebra/Module/StrongTopology.lean +++ b/Mathlib/Topology/Algebra/Module/StrongTopology.lean @@ -117,14 +117,17 @@ theorem uniformity_toTopologicalSpace_eq [UniformSpace F] [UniformAddGroup F] ( UniformConvergenceCLM.instTopologicalSpace σ F 𝔖 := rfl -theorem uniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : - UniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] F) DFunLike.coe := +theorem isUniformEmbedding_coeFn [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) : + IsUniformEmbedding (α := UniformConvergenceCLM σ F 𝔖) (β := E →ᵤ[𝔖] F) DFunLike.coe := ⟨⟨rfl⟩, DFunLike.coe_injective⟩ +@[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) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) := - UniformEmbedding.embedding (uniformEmbedding_coeFn _ _ _) + IsUniformEmbedding.embedding (isUniformEmbedding_coeFn _ _ _) instance instAddCommGroup [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : AddCommGroup (UniformConvergenceCLM σ F 𝔖) := ContinuousLinearMap.addCommGroup @@ -133,7 +136,7 @@ instance instUniformAddGroup [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (S UniformAddGroup (UniformConvergenceCLM σ F 𝔖) := by let φ : (UniformConvergenceCLM σ F 𝔖) →+ E →ᵤ[𝔖] F := ⟨⟨(DFunLike.coe : (UniformConvergenceCLM σ F 𝔖) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩ - exact (uniformEmbedding_coeFn _ _ _).uniformAddGroup φ + exact (isUniformEmbedding_coeFn _ _ _).uniformAddGroup φ instance instTopologicalAddGroup [TopologicalSpace F] [TopologicalAddGroup F] (𝔖 : Set (Set E)) : TopologicalAddGroup (UniformConvergenceCLM σ F 𝔖) := by @@ -189,7 +192,7 @@ instance instUniformContinuousConstSMul (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] [UniformSpace F] [UniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) : UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖) := - (uniformEmbedding_coeFn σ F 𝔖).toUniformInducing.uniformContinuousConstSMul fun _ _ ↦ by rfl + (isUniformEmbedding_coeFn σ F 𝔖).toUniformInducing.uniformContinuousConstSMul fun _ _ ↦ by rfl instance instContinuousConstSMul (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] @@ -276,9 +279,13 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F fun SV => { f : E →SL[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2 } := ContinuousLinearMap.hasBasis_nhds_zero_of_basis (𝓝 0).basis_sets -theorem uniformEmbedding_toUniformOnFun [UniformSpace F] [UniformAddGroup F] : - UniformEmbedding fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f := - UniformConvergenceCLM.uniformEmbedding_coeFn .. +theorem isUniformEmbedding_toUniformOnFun [UniformSpace F] [UniformAddGroup F] : + IsUniformEmbedding + fun f : E →SL[σ] F ↦ UniformOnFun.ofFun {s | Bornology.IsVonNBounded 𝕜₁ s} f := + UniformConvergenceCLM.isUniformEmbedding_coeFn .. + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toUniformOnFun := isUniformEmbedding_toUniformOnFun instance uniformContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F] @@ -362,15 +369,18 @@ variable [UniformSpace F] [UniformAddGroup F] [Module 𝕜 F] (𝕜' : Type*) [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜' 𝕜] [Module 𝕜' E] [IsScalarTower 𝕜' 𝕜 E] [Module 𝕜' F] [IsScalarTower 𝕜' 𝕜 F] -theorem uniformEmbedding_restrictScalars : - UniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := by - rw [← uniformEmbedding_toUniformOnFun.of_comp_iff] - convert uniformEmbedding_toUniformOnFun using 4 with s +theorem isUniformEmbedding_restrictScalars : + IsUniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := by + rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff] + convert isUniformEmbedding_toUniformOnFun using 4 with s exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩ +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_restrictScalars := isUniformEmbedding_restrictScalars + theorem uniformContinuous_restrictScalars : UniformContinuous (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := - (uniformEmbedding_restrictScalars 𝕜').uniformContinuous + (isUniformEmbedding_restrictScalars 𝕜').uniformContinuous end UniformSpace @@ -382,7 +392,7 @@ theorem embedding_restrictScalars : Embedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F)) := letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform - (uniformEmbedding_restrictScalars _).embedding + (isUniformEmbedding_restrictScalars _).embedding @[continuity, fun_prop] theorem continuous_restrictScalars : diff --git a/Mathlib/Topology/Algebra/SeparationQuotient.lean b/Mathlib/Topology/Algebra/SeparationQuotient.lean index 19e68ba576e4f..070cdf516d506 100644 --- a/Mathlib/Topology/Algebra/SeparationQuotient.lean +++ b/Mathlib/Topology/Algebra/SeparationQuotient.lean @@ -435,10 +435,13 @@ theorem outCLM_uniformInducing : UniformInducing (outCLM K E) := by rw [← uniformInducing_mk.uniformInducing_comp_iff, mk_comp_outCLM] exact uniformInducing_id -theorem outCLM_uniformEmbedding : UniformEmbedding (outCLM K E) where +theorem outCLM_isUniformEmbedding : IsUniformEmbedding (outCLM K E) where inj := outCLM_injective K E toUniformInducing := outCLM_uniformInducing K E +@[deprecated (since := "2024-10-01")] +alias outCLM_uniformEmbedding := outCLM_isUniformEmbedding + theorem outCLM_uniformContinuous : UniformContinuous (outCLM K E) := (outCLM_uniformInducing K E).uniformContinuous diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean index 27cc2841c5eb2..6746d27d74d8b 100644 --- a/Mathlib/Topology/Algebra/UniformField.lean +++ b/Mathlib/Topology/Algebra/UniformField.lean @@ -55,7 +55,7 @@ namespace UniformSpace namespace Completion instance (priority := 100) [T0Space K] : Nontrivial (hat K) := - ⟨⟨0, 1, fun h => zero_ne_one <| (uniformEmbedding_coe K).inj h⟩⟩ + ⟨⟨0, 1, fun h => zero_ne_one <| (isUniformEmbedding_coe K).inj h⟩⟩ variable {K} @@ -145,7 +145,7 @@ theorem mul_hatInv_cancel {x : hat K} (x_ne : x ≠ 0) : x * hatInv x = 1 := by rwa [closure_singleton, mem_singleton_iff] at fxclo instance instField : Field (hat K) where - exists_pair_ne := ⟨0, 1, fun h => zero_ne_one ((uniformEmbedding_coe K).inj h)⟩ + exists_pair_ne := ⟨0, 1, fun h => zero_ne_one ((isUniformEmbedding_coe K).inj h)⟩ mul_inv_cancel := fun x x_ne => by simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne] inv_zero := by simp only [Inv.inv, ite_true] -- TODO: use a better defeq @@ -176,7 +176,7 @@ variable (L : Type*) [Field L] [UniformSpace L] [CompletableTopField L] instance Subfield.completableTopField (K : Subfield L) : CompletableTopField K where nice F F_cau inf_F := by let i : K →+* L := K.subtype - have hi : UniformInducing i := uniformEmbedding_subtype_val.toUniformInducing + have hi : UniformInducing i := isUniformEmbedding_subtype_val.toUniformInducing rw [← hi.cauchy_map_iff] at F_cau ⊢ rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)] apply CompletableTopField.nice _ F_cau diff --git a/Mathlib/Topology/Algebra/UniformGroup.lean b/Mathlib/Topology/Algebra/UniformGroup.lean index 21f75fd7a2065..daf8079c33a30 100644 --- a/Mathlib/Topology/Algebra/UniformGroup.lean +++ b/Mathlib/Topology/Algebra/UniformGroup.lean @@ -179,13 +179,16 @@ theorem uniformity_translate_mul (a : α) : ((𝓤 α).map fun x : α × α => ( ) @[to_additive] -theorem uniformEmbedding_translate_mul (a : α) : UniformEmbedding fun x : α => x * a := +theorem isUniformEmbedding_translate_mul (a : α) : IsUniformEmbedding fun x : α => x * a := { comap_uniformity := by nth_rw 1 [← uniformity_translate_mul a, comap_map] rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩ simp only [Prod.mk.injEq, mul_left_inj, imp_self] inj := mul_left_injective a } +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_translate_mul := isUniformEmbedding_translate_mul + namespace MulOpposite @[to_additive] diff --git a/Mathlib/Topology/ContinuousMap/Bounded.lean b/Mathlib/Topology/ContinuousMap/Bounded.lean index 205125c91bfb4..a1fa188b5cc16 100644 --- a/Mathlib/Topology/ContinuousMap/Bounded.lean +++ b/Mathlib/Topology/ContinuousMap/Bounded.lean @@ -246,7 +246,7 @@ theorem inducing_coeFn : Inducing (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) UniformFun.tendsto_iff_tendstoUniformly] simp [comp_def] --- TODO: upgrade to a `UniformEmbedding` +-- TODO: upgrade to a `IsUniformEmbedding` theorem embedding_coeFn : Embedding (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) → α →ᵤ β) := ⟨inducing_coeFn, fun _ _ h => ext fun x => congr_fun h x⟩ @@ -524,7 +524,7 @@ theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β) fun f hf => ?_ · haveI : CompactSpace s := isCompact_iff_compactSpace.1 hs refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_ - rw [uniformEmbedding_subtype_val.toUniformInducing.equicontinuous_iff] + rw [isUniformEmbedding_subtype_val.toUniformInducing.equicontinuous_iff] exact H.comp (A.restrictPreimage F) · let g := codRestrict s f fun x => in_s f x hf rw [show f = F g by ext; rfl] at hf ⊢ diff --git a/Mathlib/Topology/ContinuousMap/Compact.lean b/Mathlib/Topology/ContinuousMap/Compact.lean index eb72857ce4102..f68ff46c4011d 100644 --- a/Mathlib/Topology/ContinuousMap/Compact.lean +++ b/Mathlib/Topology/ContinuousMap/Compact.lean @@ -59,9 +59,12 @@ theorem uniformInducing_equivBoundedOfCompact : UniformInducing (equivBoundedOfC ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩, fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩) -theorem uniformEmbedding_equivBoundedOfCompact : UniformEmbedding (equivBoundedOfCompact α β) := +theorem isUniformEmbedding_equivBoundedOfCompact : IsUniformEmbedding (equivBoundedOfCompact α β) := { uniformInducing_equivBoundedOfCompact α β with inj := (equivBoundedOfCompact α β).injective } +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_equivBoundedOfCompact := isUniformEmbedding_equivBoundedOfCompact + /-- When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are additively equivalent to `C(α, 𝕜)`. -/ @@ -83,7 +86,7 @@ theorem addEquivBoundedOfCompact_apply [AddMonoid β] [LipschitzAdd β] : rfl instance metricSpace : MetricSpace C(α, β) := - (uniformEmbedding_equivBoundedOfCompact α β).comapMetricSpace _ + (isUniformEmbedding_equivBoundedOfCompact α β).comapMetricSpace _ /-- When `α` is compact, and `β` is a metric space, the bounded continuous maps `α →ᵇ β` are isometric to `C(α, β)`. diff --git a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean index fd74c5bccfa7c..7dcfc9a8fff16 100644 --- a/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean +++ b/Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean @@ -268,20 +268,26 @@ variable [Zero R] [UniformSpace R] protected instance instUniformSpace : UniformSpace C(X, R)₀ := .comap toContinuousMap inferInstance -lemma uniformEmbedding_toContinuousMap : - UniformEmbedding ((↑) : C(X, R)₀ → C(X, R)) where +lemma isUniformEmbedding_toContinuousMap : + IsUniformEmbedding ((↑) : C(X, R)₀ → C(X, R)) where comap_uniformity := rfl inj _ _ h := ext fun x ↦ congr($(h) x) +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toContinuousMap := isUniformEmbedding_toContinuousMap + instance [T1Space R] [CompleteSpace C(X, R)] : CompleteSpace C(X, R)₀ := - completeSpace_iff_isComplete_range uniformEmbedding_toContinuousMap.toUniformInducing + completeSpace_iff_isComplete_range isUniformEmbedding_toContinuousMap.toUniformInducing |>.mpr closedEmbedding_toContinuousMap.isClosed_range.isComplete -lemma uniformEmbedding_comp {Y : Type*} [UniformSpace Y] [Zero Y] (g : C(Y, R)₀) - (hg : UniformEmbedding g) : UniformEmbedding (g.comp · : C(X, Y)₀ → C(X, R)₀) := - uniformEmbedding_toContinuousMap.of_comp_iff.mp <| - ContinuousMap.uniformEmbedding_comp g.toContinuousMap hg |>.comp - uniformEmbedding_toContinuousMap +lemma isUniformEmbedding_comp {Y : Type*} [UniformSpace Y] [Zero Y] (g : C(Y, R)₀) + (hg : IsUniformEmbedding g) : IsUniformEmbedding (g.comp · : C(X, Y)₀ → C(X, R)₀) := + isUniformEmbedding_toContinuousMap.of_comp_iff.mp <| + ContinuousMap.isUniformEmbedding_comp g.toContinuousMap hg |>.comp + isUniformEmbedding_toContinuousMap + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_comp := isUniformEmbedding_comp /-- The uniform equivalence `C(X, R)₀ ≃ᵤ C(Y, R)₀` induced by a homeomorphism of the domains sending `0 : X` to `0 : Y`. -/ @@ -291,12 +297,12 @@ def _root_.UniformEquiv.arrowCongrLeft₀ {Y : Type*} [TopologicalSpace Y] [Zero invFun g := g.comp ⟨f.toContinuousMap, hf⟩ left_inv g := ext fun _ ↦ congrArg g <| f.left_inv _ right_inv g := ext fun _ ↦ congrArg g <| f.right_inv _ - uniformContinuous_toFun := uniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <| + uniformContinuous_toFun := isUniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <| ContinuousMap.uniformContinuous_comp_left f.symm.toContinuousMap |>.comp - uniformEmbedding_toContinuousMap.uniformContinuous - uniformContinuous_invFun := uniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <| + isUniformEmbedding_toContinuousMap.uniformContinuous + uniformContinuous_invFun := isUniformEmbedding_toContinuousMap.uniformContinuous_iff.mpr <| ContinuousMap.uniformContinuous_comp_left f.toContinuousMap |>.comp - uniformEmbedding_toContinuousMap.uniformContinuous + isUniformEmbedding_toContinuousMap.uniformContinuous end UniformSpace @@ -340,7 +346,7 @@ section Norm variable {α : Type*} {𝕜 : Type*} {R : Type*} [TopologicalSpace α] [CompactSpace α] [Zero α] noncomputable instance [MetricSpace R] [Zero R]: MetricSpace C(α, R)₀ := - ContinuousMapZero.uniformEmbedding_toContinuousMap.comapMetricSpace _ + ContinuousMapZero.isUniformEmbedding_toContinuousMap.comapMetricSpace _ noncomputable instance [NormedAddCommGroup R] : Norm C(α, R)₀ where norm f := ‖(f : C(α, R))‖ diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean index 20efe03e7d47a..deca954dd5665 100644 --- a/Mathlib/Topology/EMetricSpace/Basic.lean +++ b/Mathlib/Topology/EMetricSpace/Basic.lean @@ -66,20 +66,27 @@ theorem uniformInducing_iff [PseudoEMetricSpace β] {f : α → β} : simp only [subset_def, Prod.forall]; rfl /-- ε-δ characterization of uniform embeddings on pseudoemetric spaces -/ -nonrec theorem uniformEmbedding_iff [PseudoEMetricSpace β] {f : α → β} : - UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ +nonrec theorem isUniformEmbedding_iff [PseudoEMetricSpace β] {f : α → β} : + IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ := - (uniformEmbedding_iff _).trans <| and_comm.trans <| Iff.rfl.and uniformInducing_iff + (isUniformEmbedding_iff _).trans <| and_comm.trans <| Iff.rfl.and uniformInducing_iff + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_iff := isUniformEmbedding_iff /-- If a map between pseudoemetric spaces is a uniform embedding then the edistance between `f x` and `f y` is controlled in terms of the distance between `x` and `y`. In fact, this lemma holds for a `UniformInducing` map. TODO: generalize? -/ -theorem controlled_of_uniformEmbedding [PseudoEMetricSpace β] {f : α → β} (h : UniformEmbedding f) : +theorem controlled_of_isUniformEmbedding [PseudoEMetricSpace β] {f : α → β} + (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ := - ⟨uniformContinuous_iff.1 h.uniformContinuous, (uniformEmbedding_iff.1 h).2.2⟩ + ⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩ + +@[deprecated (since := "2024-10-01")] +alias controlled_of_uniformEmbedding := controlled_of_isUniformEmbedding /-- ε-δ characterization of Cauchy sequences on pseudoemetric spaces -/ protected theorem cauchy_iff {f : Filter α} : @@ -231,11 +238,14 @@ instance (priority := 100) EMetricSpace.instT0Space : T0Space γ where /-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x` and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/ -theorem EMetric.uniformEmbedding_iff' [EMetricSpace β] {f : γ → β} : - UniformEmbedding f ↔ +theorem EMetric.isUniformEmbedding_iff' [EMetricSpace β] {f : γ → β} : + IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ := by - rw [uniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff] + rw [isUniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff] + +@[deprecated (since := "2024-10-01")] +alias EMetric.uniformEmbedding_iff' := EMetric.isUniformEmbedding_iff' /-- If a `PseudoEMetricSpace` is a T₀ space, then it is an `EMetricSpace`. -/ -- Porting note: made `reducible`; diff --git a/Mathlib/Topology/EMetricSpace/Defs.lean b/Mathlib/Topology/EMetricSpace/Defs.lean index 12ff875ac5f87..2b6096cad74f3 100644 --- a/Mathlib/Topology/EMetricSpace/Defs.lean +++ b/Mathlib/Topology/EMetricSpace/Defs.lean @@ -25,7 +25,7 @@ to `EMetricSpace` at the end. -/ assert_not_exists Nat.instLocallyFiniteOrder -assert_not_exists UniformEmbedding +assert_not_exists IsUniformEmbedding assert_not_exists TendstoUniformlyOnFilter open Set Filter diff --git a/Mathlib/Topology/Instances/Int.lean b/Mathlib/Topology/Instances/Int.lean index 4e93d2e862ea6..5ee25d7b929f2 100644 --- a/Mathlib/Topology/Instances/Int.lean +++ b/Mathlib/Topology/Instances/Int.lean @@ -39,13 +39,16 @@ theorem pairwise_one_le_dist : Pairwise fun m n : ℤ => 1 ≤ dist m n := by intro m n hne rw [dist_eq]; norm_cast; rwa [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero] -theorem uniformEmbedding_coe_real : UniformEmbedding ((↑) : ℤ → ℝ) := - uniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist +theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℤ → ℝ) := + isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_coe_real := isUniformEmbedding_coe_real theorem closedEmbedding_coe_real : ClosedEmbedding ((↑) : ℤ → ℝ) := closedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist -instance : MetricSpace ℤ := Int.uniformEmbedding_coe_real.comapMetricSpace _ +instance : MetricSpace ℤ := Int.isUniformEmbedding_coe_real.comapMetricSpace _ theorem preimage_ball (x : ℤ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r := rfl diff --git a/Mathlib/Topology/Instances/Nat.lean b/Mathlib/Topology/Instances/Nat.lean index 2e4857faf7c51..e90ce1cbe65b7 100644 --- a/Mathlib/Topology/Instances/Nat.lean +++ b/Mathlib/Topology/Instances/Nat.lean @@ -31,13 +31,16 @@ theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl theorem pairwise_one_le_dist : Pairwise fun m n : ℕ => 1 ≤ dist m n := fun _ _ hne => Int.pairwise_one_le_dist <| mod_cast hne -theorem uniformEmbedding_coe_real : UniformEmbedding ((↑) : ℕ → ℝ) := - uniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist +theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℕ → ℝ) := + isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_coe_real := isUniformEmbedding_coe_real theorem closedEmbedding_coe_real : ClosedEmbedding ((↑) : ℕ → ℝ) := closedEmbedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist -instance : MetricSpace ℕ := Nat.uniformEmbedding_coe_real.comapMetricSpace _ +instance : MetricSpace ℕ := Nat.isUniformEmbedding_coe_real.comapMetricSpace _ theorem preimage_ball (x : ℕ) (r : ℝ) : (↑) ⁻¹' ball (x : ℝ) r = ball x r := rfl diff --git a/Mathlib/Topology/Instances/PNat.lean b/Mathlib/Topology/Instances/PNat.lean index 3a05c74ac7076..dd79778f35d9b 100644 --- a/Mathlib/Topology/Instances/PNat.lean +++ b/Mathlib/Topology/Instances/PNat.lean @@ -24,7 +24,10 @@ theorem dist_eq (x y : ℕ+) : dist x y = |(↑x : ℝ) - ↑y| := rfl @[simp, norm_cast] theorem dist_coe (x y : ℕ+) : dist (↑x : ℕ) (↑y : ℕ) = dist x y := rfl -theorem uniformEmbedding_coe : UniformEmbedding ((↑) : ℕ+ → ℕ) := uniformEmbedding_subtype_val +theorem isUniformEmbedding_coe : IsUniformEmbedding ((↑) : ℕ+ → ℕ) := isUniformEmbedding_subtype_val + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_coe := isUniformEmbedding_coe instance : DiscreteTopology ℕ+ := inferInstanceAs (DiscreteTopology { n : ℕ // 0 < n }) diff --git a/Mathlib/Topology/Instances/Rat.lean b/Mathlib/Topology/Instances/Rat.lean index 22cc2d6c6f682..a5585543b41fe 100644 --- a/Mathlib/Topology/Instances/Rat.lean +++ b/Mathlib/Topology/Instances/Rat.lean @@ -30,11 +30,14 @@ theorem dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := theorem uniformContinuous_coe_real : UniformContinuous ((↑) : ℚ → ℝ) := uniformContinuous_comap -theorem uniformEmbedding_coe_real : UniformEmbedding ((↑) : ℚ → ℝ) := - uniformEmbedding_comap Rat.cast_injective +theorem isUniformEmbedding_coe_real : IsUniformEmbedding ((↑) : ℚ → ℝ) := + isUniformEmbedding_comap Rat.cast_injective + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_coe_real := isUniformEmbedding_coe_real theorem isDenseEmbedding_coe_real : IsDenseEmbedding ((↑) : ℚ → ℝ) := - uniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast + isUniformEmbedding_coe_real.isDenseEmbedding Rat.denseRange_cast @[deprecated (since := "2024-09-30")] alias denseEmbedding_coe_real := isDenseEmbedding_coe_real @@ -51,8 +54,11 @@ end Rat theorem Nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y := by rw [← Nat.dist_cast_real, ← Rat.dist_cast]; congr -theorem Nat.uniformEmbedding_coe_rat : UniformEmbedding ((↑) : ℕ → ℚ) := - uniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist +theorem Nat.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℕ → ℚ) := + isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist + +@[deprecated (since := "2024-10-01")] +alias Nat.uniformEmbedding_coe_rat := Nat.isUniformEmbedding_coe_rat theorem Nat.closedEmbedding_coe_rat : ClosedEmbedding ((↑) : ℕ → ℚ) := closedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Nat.pairwise_one_le_dist @@ -61,8 +67,11 @@ theorem Nat.closedEmbedding_coe_rat : ClosedEmbedding ((↑) : ℕ → ℚ) := theorem Int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y := by rw [← Int.dist_cast_real, ← Rat.dist_cast]; congr -theorem Int.uniformEmbedding_coe_rat : UniformEmbedding ((↑) : ℤ → ℚ) := - uniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist +theorem Int.isUniformEmbedding_coe_rat : IsUniformEmbedding ((↑) : ℤ → ℚ) := + isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist + +@[deprecated (since := "2024-10-01")] +alias Int.uniformEmbedding_coe_rat := Int.isUniformEmbedding_coe_rat theorem Int.closedEmbedding_coe_rat : ClosedEmbedding ((↑) : ℤ → ℚ) := closedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist @@ -72,7 +81,7 @@ namespace Rat instance : NoncompactSpace ℚ := Int.closedEmbedding_coe_rat.noncompactSpace theorem uniformContinuous_add : UniformContinuous fun p : ℚ × ℚ => p.1 + p.2 := - Rat.uniformEmbedding_coe_real.toUniformInducing.uniformContinuous_iff.2 <| by + Rat.isUniformEmbedding_coe_real.toUniformInducing.uniformContinuous_iff.2 <| by simp only [Function.comp_def, Rat.cast_add] exact Real.uniformContinuous_add.comp (Rat.uniformContinuous_coe_real.prod_map Rat.uniformContinuous_coe_real) @@ -97,7 +106,7 @@ instance : TopologicalRing ℚ := inferInstance nonrec theorem totallyBounded_Icc (a b : ℚ) : TotallyBounded (Icc a b) := by simpa only [preimage_cast_Icc] - using totallyBounded_preimage Rat.uniformEmbedding_coe_real.toUniformInducing + using totallyBounded_preimage Rat.isUniformEmbedding_coe_real.toUniformInducing (totallyBounded_Icc (a : ℝ) b) end Rat diff --git a/Mathlib/Topology/MetricSpace/Antilipschitz.lean b/Mathlib/Topology/MetricSpace/Antilipschitz.lean index 88e3996a46af3..ac87aa46237ea 100644 --- a/Mathlib/Topology/MetricSpace/Antilipschitz.lean +++ b/Mathlib/Topology/MetricSpace/Antilipschitz.lean @@ -147,11 +147,12 @@ protected theorem uniformInducing (hf : AntilipschitzWith K f) (hfc : UniformCon UniformInducing f := ⟨le_antisymm hf.comap_uniformity_le hfc.le_comap⟩ -protected theorem uniformEmbedding {α : Type*} {β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] - {K : ℝ≥0} {f : α → β} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : - UniformEmbedding f := +lemma isUniformEmbedding {α β : Type*} [EMetricSpace α] [PseudoEMetricSpace β] {K : ℝ≥0} {f : α → β} + (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsUniformEmbedding f := ⟨hf.uniformInducing hfc, hf.injective⟩ +@[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding + theorem isComplete_range [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : IsComplete (range f) := (hf.uniformInducing hfc).isComplete_range @@ -164,7 +165,7 @@ theorem isClosed_range {α β : Type*} [PseudoEMetricSpace α] [EMetricSpace β] theorem closedEmbedding {α : Type*} {β : Type*} [EMetricSpace α] [EMetricSpace β] {K : ℝ≥0} {f : α → β} [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : ClosedEmbedding f := - { (hf.uniformEmbedding hfc).embedding with isClosed_range := hf.isClosed_range hfc } + { (hf.isUniformEmbedding hfc).embedding with isClosed_range := hf.isClosed_range hfc } theorem subtype_coe (s : Set α) : AntilipschitzWith 1 ((↑) : s → α) := AntilipschitzWith.id.restrict s diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean index f3b2468b6e50b..028c1ab133161 100644 --- a/Mathlib/Topology/MetricSpace/Basic.lean +++ b/Mathlib/Topology/MetricSpace/Basic.lean @@ -32,11 +32,14 @@ instance (priority := 100) _root_.MetricSpace.instT0Space : T0Space γ where /-- A map between metric spaces is a uniform embedding if and only if the distance between `f x` and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/ -theorem uniformEmbedding_iff' [MetricSpace β] {f : γ → β} : - UniformEmbedding f ↔ +theorem isUniformEmbedding_iff' [MetricSpace β] {f : γ → β} : + IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ := by - rw [uniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff] + rw [isUniformEmbedding_iff_uniformInducing, uniformInducing_iff, uniformContinuous_iff] + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_iff' := isUniformEmbedding_iff' /-- If a `PseudoMetricSpace` is a T₀ space, then it is a `MetricSpace`. -/ abbrev _root_.MetricSpace.ofT0PseudoMetricSpace (α : Type*) [PseudoMetricSpace α] [T0Space α] : @@ -60,10 +63,13 @@ theorem closedEmbedding_of_pairwise_le_dist {α : Type*} [TopologicalSpace α] [ /-- If `f : β → α` sends any two distinct points to points at distance at least `ε > 0`, then `f` is a uniform embedding with respect to the discrete uniformity on `β`. -/ -theorem uniformEmbedding_bot_of_pairwise_le_dist {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α} +theorem isUniformEmbedding_bot_of_pairwise_le_dist {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) : - @UniformEmbedding _ _ ⊥ (by infer_instance) f := - uniformEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf + @IsUniformEmbedding _ _ ⊥ (by infer_instance) f := + isUniformEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_bot_of_pairwise_le_dist := isUniformEmbedding_bot_of_pairwise_le_dist end Metric @@ -94,10 +100,13 @@ abbrev MetricSpace.induced {γ β} (f : γ → β) (hf : Function.Injective f) ( /-- Pull back a metric space structure by a uniform embedding. This is a version of `MetricSpace.induced` useful in case if the domain already has a `UniformSpace` structure. -/ -abbrev UniformEmbedding.comapMetricSpace {α β} [UniformSpace α] [m : MetricSpace β] (f : α → β) - (h : UniformEmbedding f) : MetricSpace α := +abbrev IsUniformEmbedding.comapMetricSpace {α β} [UniformSpace α] [m : MetricSpace β] (f : α → β) + (h : IsUniformEmbedding f) : MetricSpace α := .replaceUniformity (.induced f h.inj m) h.comap_uniformity.symm +@[deprecated (since := "2024-10-03")] +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 : α → β) diff --git a/Mathlib/Topology/MetricSpace/Closeds.lean b/Mathlib/Topology/MetricSpace/Closeds.lean index 67b9d4cbf3244..cf5140b7380c9 100644 --- a/Mathlib/Topology/MetricSpace/Closeds.lean +++ b/Mathlib/Topology/MetricSpace/Closeds.lean @@ -232,9 +232,12 @@ instance NonemptyCompacts.emetricSpace : EMetricSpace (NonemptyCompacts α) wher rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this /-- `NonemptyCompacts.toCloseds` is a uniform embedding (as it is an isometry) -/ -theorem NonemptyCompacts.ToCloseds.uniformEmbedding : - UniformEmbedding (@NonemptyCompacts.toCloseds α _ _) := - Isometry.uniformEmbedding fun _ _ => rfl +theorem NonemptyCompacts.ToCloseds.isUniformEmbedding : + IsUniformEmbedding (@NonemptyCompacts.toCloseds α _ _) := + Isometry.isUniformEmbedding fun _ _ => rfl + +@[deprecated (since := "2024-10-01")] +alias NonemptyCompacts.ToCloseds.uniformEmbedding := NonemptyCompacts.ToCloseds.isUniformEmbedding /-- The range of `NonemptyCompacts.toCloseds` is closed in a complete space -/ theorem NonemptyCompacts.isClosed_in_closeds [CompleteSpace α] : @@ -278,14 +281,14 @@ theorem NonemptyCompacts.isClosed_in_closeds [CompleteSpace α] : from the same statement for closed subsets -/ instance NonemptyCompacts.completeSpace [CompleteSpace α] : CompleteSpace (NonemptyCompacts α) := (completeSpace_iff_isComplete_range - NonemptyCompacts.ToCloseds.uniformEmbedding.toUniformInducing).2 <| + NonemptyCompacts.ToCloseds.isUniformEmbedding.toUniformInducing).2 <| NonemptyCompacts.isClosed_in_closeds.isComplete /-- In a compact space, the type of nonempty compact subsets is compact. This follows from the same statement for closed subsets -/ instance NonemptyCompacts.compactSpace [CompactSpace α] : CompactSpace (NonemptyCompacts α) := ⟨by - rw [NonemptyCompacts.ToCloseds.uniformEmbedding.embedding.isCompact_iff, image_univ] + rw [NonemptyCompacts.ToCloseds.isUniformEmbedding.embedding.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 c68a245846375..b94867562a459 100644 --- a/Mathlib/Topology/MetricSpace/Dilation.lean +++ b/Mathlib/Topology/MetricSpace/Dilation.lean @@ -420,14 +420,16 @@ variable [EMetricSpace α] variable [FunLike F α β] /-- A dilation from a metric space is a uniform embedding -/ -protected theorem uniformEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : - UniformEmbedding f := - (antilipschitz f).uniformEmbedding (lipschitz f).uniformContinuous +lemma isUniformEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) : + IsUniformEmbedding f := + (antilipschitz f).isUniformEmbedding (lipschitz f).uniformContinuous + +@[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.uniformEmbedding f).embedding + (Dilation.isUniformEmbedding f).embedding /-- A dilation from a complete emetric space is a closed embedding -/ protected theorem closedEmbedding [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) : diff --git a/Mathlib/Topology/MetricSpace/Isometry.lean b/Mathlib/Topology/MetricSpace/Isometry.lean index fc48af3ac67e9..8b05b577ab5bf 100644 --- a/Mathlib/Topology/MetricSpace/Isometry.lean +++ b/Mathlib/Topology/MetricSpace/Isometry.lean @@ -162,12 +162,14 @@ protected theorem injective (h : Isometry f) : Injective f := h.antilipschitz.injective /-- An isometry from an emetric space is a uniform embedding -/ -protected theorem uniformEmbedding (hf : Isometry f) : UniformEmbedding f := - hf.antilipschitz.uniformEmbedding hf.lipschitz.uniformContinuous +lemma isUniformEmbedding (hf : Isometry f) : IsUniformEmbedding f := + hf.antilipschitz.isUniformEmbedding hf.lipschitz.uniformContinuous + +@[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.uniformEmbedding.embedding + hf.isUniformEmbedding.embedding /-- An isometry from a complete emetric space is a closed embedding -/ theorem closedEmbedding [CompleteSpace α] [EMetricSpace γ] {f : α → γ} (hf : Isometry f) : @@ -226,11 +228,14 @@ end Isometry -- namespace /-- A uniform embedding from a uniform space to a metric space is an isometry with respect to the induced metric space structure on the source space. -/ -theorem UniformEmbedding.to_isometry {α β} [UniformSpace α] [MetricSpace β] {f : α → β} - (h : UniformEmbedding f) : (letI := h.comapMetricSpace f; Isometry f) := +theorem IsUniformEmbedding.to_isometry {α β} [UniformSpace α] [MetricSpace β] {f : α → β} + (h : IsUniformEmbedding f) : (letI := h.comapMetricSpace f; Isometry f) := let _ := h.comapMetricSpace f Isometry.of_dist_eq fun _ _ => rfl +@[deprecated (since := "2024-10-01")] +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 : α → β} diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean b/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean index 65722ebb2e6b9..346e0e97d3e23 100644 --- a/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean +++ b/Mathlib/Topology/MetricSpace/Pseudo/Basic.lean @@ -68,17 +68,24 @@ nonrec theorem uniformInducing_iff [PseudoMetricSpace β] {f : α → β} : ((uniformity_basis_dist.comap _).le_basis_iff uniformity_basis_dist).trans <| by simp only [subset_def, Prod.forall, gt_iff_lt, preimage_setOf_eq, Prod.map_apply, mem_setOf] -nonrec theorem uniformEmbedding_iff [PseudoMetricSpace β] {f : α → β} : - UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ +nonrec theorem isUniformEmbedding_iff [PseudoMetricSpace β] {f : α → β} : + IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ := by - rw [uniformEmbedding_iff, and_comm, uniformInducing_iff] + rw [isUniformEmbedding_iff, and_comm, uniformInducing_iff] + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_iff := isUniformEmbedding_iff /-- If a map between pseudometric spaces is a uniform embedding then the distance between `f x` and `f y` is controlled in terms of the distance between `x` and `y`. -/ -theorem controlled_of_uniformEmbedding [PseudoMetricSpace β] {f : α → β} (h : UniformEmbedding f) : +theorem controlled_of_isUniformEmbedding [PseudoMetricSpace β] {f : α → β} + (h : IsUniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ := - ⟨uniformContinuous_iff.1 h.uniformContinuous, (uniformEmbedding_iff.1 h).2.2⟩ + ⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformEmbedding_iff.1 h).2.2⟩ + +@[deprecated (since := "2024-10-01")] +alias controlled_of_uniformEmbedding := controlled_of_isUniformEmbedding theorem totallyBounded_iff {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε := diff --git a/Mathlib/Topology/UniformSpace/Ascoli.lean b/Mathlib/Topology/UniformSpace/Ascoli.lean index 75e7105788ec2..0b702ae3a22f7 100644 --- a/Mathlib/Topology/UniformSpace/Ascoli.lean +++ b/Mathlib/Topology/UniformSpace/Ascoli.lean @@ -495,7 +495,8 @@ theorem ArzelaAscoli.isCompact_of_equicontinuous rw [isCompact_iff_compactSpace] at hS1 ⊢ exact (Equiv.toHomeomorphOfInducing _ h).symm.compactSpace rw [← inducing_subtype_val.of_comp_iff, ← EquicontinuousOn.inducing_uniformOnFun_iff_pi _ _ _] - · exact ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact.inducing.comp inducing_subtype_val + · exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.inducing.comp + inducing_subtype_val · exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton) · exact fun _ ↦ id · exact fun K _ ↦ hS2.equicontinuousOn K diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 4d5a67fa923b1..d2dc3a7e09b3f 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -17,7 +17,7 @@ generalize to uniform spaces, e.g. * uniform continuity (in this file) * completeness (in `Cauchy.lean`) -* extension of uniform continuous functions to complete spaces (in `UniformEmbedding.lean`) +* extension of uniform continuous functions to complete spaces (in `IsUniformEmbedding.lean`) * totally bounded sets (in `Cauchy.lean`) * totally bounded complete sets are compact (in `Cauchy.lean`) diff --git a/Mathlib/Topology/UniformSpace/CompactConvergence.lean b/Mathlib/Topology/UniformSpace/CompactConvergence.lean index 7f50b07c0cc1d..c316d5316d094 100644 --- a/Mathlib/Topology/UniformSpace/CompactConvergence.lean +++ b/Mathlib/Topology/UniformSpace/CompactConvergence.lean @@ -171,11 +171,14 @@ instance compactConvergenceUniformSpace : UniformSpace C(α, β) := nhds_induced, tendsto_comap_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn] rfl -theorem uniformEmbedding_toUniformOnFunIsCompact : - UniformEmbedding (toUniformOnFunIsCompact : C(α, β) → α →ᵤ[{K | IsCompact K}] β) where +theorem isUniformEmbedding_toUniformOnFunIsCompact : + IsUniformEmbedding (toUniformOnFunIsCompact : C(α, β) → α →ᵤ[{K | IsCompact K}] β) where comap_uniformity := rfl inj := DFunLike.coe_injective +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_toUniformOnFunIsCompact := isUniformEmbedding_toUniformOnFunIsCompact + -- The following definitions and theorems -- used to be a part of the construction of the `UniformSpace C(α, β)` structure -- before it was migrated to `UniformOnFun` @@ -184,7 +187,7 @@ theorem _root_.Filter.HasBasis.compactConvergenceUniformity {ι : Type*} {pi : {s : ι → Set (β × β)} (h : (𝓤 β).HasBasis pi s) : HasBasis (𝓤 C(α, β)) (fun p : Set α × ι => IsCompact p.1 ∧ pi p.2) fun p => { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ s p.2 } := by - rw [← uniformEmbedding_toUniformOnFunIsCompact.comap_uniformity] + rw [← isUniformEmbedding_toUniformOnFunIsCompact.comap_uniformity] exact .comap _ <| UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K} ⟨∅, isCompact_empty⟩ (directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h @@ -260,27 +263,30 @@ variable {γ δ : Type*} [TopologicalSpace γ] [UniformSpace δ] theorem uniformContinuous_comp (g : C(β, δ)) (hg : UniformContinuous g) : UniformContinuous (ContinuousMap.comp g : C(α, β) → C(α, δ)) := - uniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <| + isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <| UniformOnFun.postcomp_uniformContinuous hg |>.comp - uniformEmbedding_toUniformOnFunIsCompact.uniformContinuous + isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous theorem uniformInducing_comp (g : C(β, δ)) (hg : UniformInducing g) : UniformInducing (ContinuousMap.comp g : C(α, β) → C(α, δ)) := - uniformEmbedding_toUniformOnFunIsCompact.toUniformInducing.of_comp_iff.mp <| + isUniformEmbedding_toUniformOnFunIsCompact.toUniformInducing.of_comp_iff.mp <| UniformOnFun.postcomp_uniformInducing hg |>.comp - uniformEmbedding_toUniformOnFunIsCompact.toUniformInducing + isUniformEmbedding_toUniformOnFunIsCompact.toUniformInducing + +theorem isUniformEmbedding_comp (g : C(β, δ)) (hg : IsUniformEmbedding g) : + IsUniformEmbedding (ContinuousMap.comp g : C(α, β) → C(α, δ)) := + isUniformEmbedding_toUniformOnFunIsCompact.of_comp_iff.mp <| + UniformOnFun.postcomp_isUniformEmbedding hg |>.comp + isUniformEmbedding_toUniformOnFunIsCompact -theorem uniformEmbedding_comp (g : C(β, δ)) (hg : UniformEmbedding g) : - UniformEmbedding (ContinuousMap.comp g : C(α, β) → C(α, δ)) := - uniformEmbedding_toUniformOnFunIsCompact.of_comp_iff.mp <| - UniformOnFun.postcomp_uniformEmbedding hg |>.comp - uniformEmbedding_toUniformOnFunIsCompact +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_comp := isUniformEmbedding_comp theorem uniformContinuous_comp_left (g : C(α, γ)) : UniformContinuous (fun f ↦ f.comp g : C(γ, β) → C(α, β)) := - uniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <| + isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <| UniformOnFun.precomp_uniformContinuous (fun _ hK ↦ hK.image g.continuous) |>.comp - uniformEmbedding_toUniformOnFunIsCompact.uniformContinuous + isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous /-- Any pair of a homeomorphism `X ≃ₜ Z` and an isomorphism `Y ≃ᵤ T` of uniform spaces gives rise to an isomorphism `C(X, Y) ≃ᵤ C(Z, T)`. -/ @@ -372,7 +378,8 @@ Sufficient conditions on `α` to satisfy this condition are (weak) local compact `ContinuousMap.instCompleteSpaceOfSequentialSpace`). -/ lemma completeSpace_of_restrictGenTopology (h : RestrictGenTopology {K : Set α | IsCompact K}) : CompleteSpace C(α, β) := by - rw [completeSpace_iff_isComplete_range uniformEmbedding_toUniformOnFunIsCompact.toUniformInducing, + rw [completeSpace_iff_isComplete_range + isUniformEmbedding_toUniformOnFunIsCompact.toUniformInducing, range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete] exact (UniformOnFun.isClosed_setOf_continuous h).completeSpace_coe diff --git a/Mathlib/Topology/UniformSpace/CompareReals.lean b/Mathlib/Topology/UniformSpace/CompareReals.lean index 7a90e73b4afcc..7f1c135164444 100644 --- a/Mathlib/Topology/UniformSpace/CompareReals.lean +++ b/Mathlib/Topology/UniformSpace/CompareReals.lean @@ -72,7 +72,7 @@ def rationalCauSeqPkg : @AbstractCompletion ℚ <| (@AbsoluteValue.abs ℚ _).un (separation := by infer_instance) (uniformInducing := by rw [Rat.uniformSpace_eq] - exact Rat.uniformEmbedding_coe_real.toUniformInducing) + exact Rat.isUniformEmbedding_coe_real.toUniformInducing) (dense := Rat.isDenseEmbedding_coe_real.dense) namespace CompareReals diff --git a/Mathlib/Topology/UniformSpace/CompleteSeparated.lean b/Mathlib/Topology/UniformSpace/CompleteSeparated.lean index 4bfc074965c87..2fcb34197b931 100644 --- a/Mathlib/Topology/UniformSpace/CompleteSeparated.lean +++ b/Mathlib/Topology/UniformSpace/CompleteSeparated.lean @@ -27,11 +27,14 @@ theorem IsComplete.isClosed [UniformSpace α] [T0Space α] {s : Set α} (h : IsC rcases h f this inf_le_right with ⟨y, ys, fy⟩ rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)] -theorem UniformEmbedding.toClosedEmbedding [UniformSpace α] [UniformSpace β] [CompleteSpace α] - [T0Space β] {f : α → β} (hf : UniformEmbedding f) : +theorem IsUniformEmbedding.toClosedEmbedding [UniformSpace α] [UniformSpace β] [CompleteSpace α] + [T0Space β] {f : α → β} (hf : IsUniformEmbedding f) : ClosedEmbedding f := ⟨hf.embedding, hf.toUniformInducing.isComplete_range.isClosed⟩ +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.toClosedEmbedding := IsUniformEmbedding.toClosedEmbedding + namespace IsDenseInducing open Filter diff --git a/Mathlib/Topology/UniformSpace/Completion.lean b/Mathlib/Topology/UniformSpace/Completion.lean index 0f386364453d4..2ca3f3f72a834 100644 --- a/Mathlib/Topology/UniformSpace/Completion.lean +++ b/Mathlib/Topology/UniformSpace/Completion.lean @@ -154,10 +154,13 @@ theorem uniformInducing_pureCauchy : UniformInducing (pureCauchy : α → Cauchy _ = 𝓤 α := by simp [this] ⟩ -theorem uniformEmbedding_pureCauchy : UniformEmbedding (pureCauchy : α → CauchyFilter α) := +theorem isUniformEmbedding_pureCauchy : IsUniformEmbedding (pureCauchy : α → CauchyFilter α) := { uniformInducing_pureCauchy with inj := fun _a₁ _a₂ h => pure_injective <| Subtype.ext_iff_val.1 h } +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_pureCauchy := isUniformEmbedding_pureCauchy + theorem denseRange_pureCauchy : DenseRange (pureCauchy : α → CauchyFilter α) := fun f => by have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs => let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs @@ -184,7 +187,7 @@ theorem isDenseInducing_pureCauchy : IsDenseInducing (pureCauchy : α → Cauchy uniformInducing_pureCauchy.isDenseInducing denseRange_pureCauchy theorem isDenseEmbedding_pureCauchy : IsDenseEmbedding (pureCauchy : α → CauchyFilter α) := - uniformEmbedding_pureCauchy.isDenseEmbedding denseRange_pureCauchy + isUniformEmbedding_pureCauchy.isDenseEmbedding denseRange_pureCauchy @[deprecated (since := "2024-09-30")] alias denseEmbedding_pureCauchy := isDenseEmbedding_pureCauchy @@ -359,12 +362,15 @@ theorem uniformContinuous_coe : UniformContinuous ((↑) : α → Completion α) theorem continuous_coe : Continuous ((↑) : α → Completion α) := cPkg.continuous_coe -theorem uniformEmbedding_coe [T0Space α] : UniformEmbedding ((↑) : α → Completion α) := +theorem isUniformEmbedding_coe [T0Space α] : IsUniformEmbedding ((↑) : α → Completion α) := { comap_uniformity := comap_coe_eq_uniformity α inj := separated_pureCauchy_injective } +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_coe := isUniformEmbedding_coe + theorem coe_injective [T0Space α] : Function.Injective ((↑) : α → Completion α) := - UniformEmbedding.inj (uniformEmbedding_coe _) + IsUniformEmbedding.inj (isUniformEmbedding_coe _) variable {α} diff --git a/Mathlib/Topology/UniformSpace/Equiv.lean b/Mathlib/Topology/UniformSpace/Equiv.lean index d4be20cb620ad..a52b28256431d 100644 --- a/Mathlib/Topology/UniformSpace/Equiv.lean +++ b/Mathlib/Topology/UniformSpace/Equiv.lean @@ -203,14 +203,16 @@ protected theorem uniformInducing (h : α ≃ᵤ β) : UniformInducing h := theorem comap_eq (h : α ≃ᵤ β) : UniformSpace.comap h ‹_› = ‹_› := h.uniformInducing.comap_uniformSpace -protected theorem uniformEmbedding (h : α ≃ᵤ β) : UniformEmbedding h := - ⟨h.uniformInducing, h.injective⟩ +theorem isUniformEmbedding (h : α ≃ᵤ β) : IsUniformEmbedding h := ⟨h.uniformInducing, h.injective⟩ + +@[deprecated (since := "2024-10-01")] alias uniformEmbedding := isUniformEmbedding theorem completeSpace_iff (h : α ≃ᵤ β) : CompleteSpace α ↔ CompleteSpace β := - completeSpace_congr h.uniformEmbedding + completeSpace_congr h.isUniformEmbedding /-- Uniform equiv given a uniform embedding. -/ -noncomputable def ofUniformEmbedding (f : α → β) (hf : UniformEmbedding f) : α ≃ᵤ Set.range f where +noncomputable def ofIsUniformEmbedding (f : α → β) (hf : IsUniformEmbedding f) : + α ≃ᵤ Set.range f where uniformContinuous_toFun := hf.toUniformInducing.uniformContinuous.subtype_mk _ uniformContinuous_invFun := by rw [hf.toUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe, @@ -218,6 +220,8 @@ noncomputable def ofUniformEmbedding (f : α → β) (hf : UniformEmbedding f) : exact uniformContinuous_subtype_val toEquiv := Equiv.ofInjective f hf.inj +@[deprecated (since := "2024-10-03")] alias ofUniformEmbedding := ofIsUniformEmbedding + /-- If two sets are equal, then they are uniformly equivalent. -/ def setCongr {s t : Set α} (h : s = t) : s ≃ᵤ t where uniformContinuous_toFun := uniformContinuous_subtype_val.subtype_mk _ diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index 4eae4a2c7b4eb..851e5d68e405e 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -377,11 +377,15 @@ a uniform embedding for the uniform structures of uniform convergence. More precisely, if `f : γ → β` is a uniform embedding, then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is a uniform embedding. -/ -protected theorem postcomp_uniformEmbedding [UniformSpace γ] {f : γ → β} (hf : UniformEmbedding f) : - UniformEmbedding (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) where +protected theorem postcomp_isUniformEmbedding [UniformSpace γ] {f : γ → β} + (hf : IsUniformEmbedding f) : + IsUniformEmbedding (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) where toUniformInducing := UniformFun.postcomp_uniformInducing hf.toUniformInducing inj _ _ H := funext fun _ ↦ hf.inj (congrFun H _) +@[deprecated (since := "2024-10-01")] +alias postcomp_uniformEmbedding := UniformFun.postcomp_isUniformEmbedding + -- Porting note: had to add a type annotation at `((f ∘ ·) : ((α → γ) → (α → β)))` /-- If `u` is a uniform structures on `β` and `f : γ → β`, then `𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)`. -/ @@ -877,11 +881,14 @@ uniform structures of `𝔖`-convergence. More precisely, if `f : γ → β` is a uniform embedding, then `(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform embedding. -/ -protected theorem postcomp_uniformEmbedding [UniformSpace γ] {f : γ → β} (hf : UniformEmbedding f) : - UniformEmbedding (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) where +protected theorem postcomp_isUniformEmbedding [UniformSpace γ] {f : γ → β} + (hf : IsUniformEmbedding f) : IsUniformEmbedding (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) where toUniformInducing := UniformOnFun.postcomp_uniformInducing hf.toUniformInducing inj _ _ H := funext fun _ ↦ hf.inj (congrFun H _) +@[deprecated (since := "2024-10-01")] +alias postcomp_uniformEmbedding := UniformOnFun.postcomp_isUniformEmbedding + /-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)` by post-composing. -/ protected def congrRight [UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) := diff --git a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean index 048ea735a5df4..adad8bcab4c26 100644 --- a/Mathlib/Topology/UniformSpace/UniformEmbedding.lean +++ b/Mathlib/Topology/UniformSpace/UniformEmbedding.lean @@ -27,7 +27,7 @@ variable {α : Type u} {β : Type v} {γ : Type w} [UniformSpace α] [UniformSpa /-- A map `f : α → β` between uniform spaces is called *uniform inducing* if the uniformity filter on `α` is the pullback of the uniformity filter on `β` under `Prod.map f f`. If `α` is a separated -space, then this implies that `f` is injective, hence it is a `UniformEmbedding`. -/ +space, then this implies that `f` is injective, hence it is a `IsUniformEmbedding`. -/ @[mk_iff] structure UniformInducing (f : α → β) : Prop where /-- The uniformity filter on the domain is the pullback of the uniformity filter on the codomain @@ -130,70 +130,109 @@ protected theorem UniformInducing.injective [T0Space α] {f : α → β} (h : Un /-- A map `f : α → β` between uniform spaces is a *uniform embedding* if it is uniform inducing and injective. If `α` is a separated space, then the latter assumption follows from the former. -/ @[mk_iff] -structure UniformEmbedding (f : α → β) extends UniformInducing f : Prop where +structure IsUniformEmbedding (f : α → β) extends UniformInducing f : Prop where /-- A uniform embedding is injective. -/ inj : Function.Injective f -theorem uniformEmbedding_iff' {f : α → β} : - UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α := by - rw [uniformEmbedding_iff, and_comm, uniformInducing_iff'] +@[deprecated (since := "2024-10-03")] alias UniformEmbedding := IsUniformEmbedding -theorem Filter.HasBasis.uniformEmbedding_iff' {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} +theorem isUniformEmbedding_iff' {f : α → β} : + IsUniformEmbedding f ↔ + Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α := by + rw [isUniformEmbedding_iff, and_comm, uniformInducing_iff'] + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_iff' := isUniformEmbedding_iff' + +theorem Filter.HasBasis.isUniformEmbedding_iff' {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} : - UniformEmbedding f ↔ Injective f ∧ + IsUniformEmbedding f ↔ Injective f ∧ (∀ i, p' i → ∃ j, p j ∧ ∀ x y, (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) := by - rw [uniformEmbedding_iff, and_comm, h.uniformInducing_iff h'] + rw [isUniformEmbedding_iff, and_comm, h.uniformInducing_iff h'] + +@[deprecated (since := "2024-10-01")] +alias Filter.HasBasis.uniformEmbedding_iff' := Filter.HasBasis.isUniformEmbedding_iff' -theorem Filter.HasBasis.uniformEmbedding_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} +theorem Filter.HasBasis.isUniformEmbedding_iff {ι ι'} {p : ι → Prop} {p' : ι' → Prop} {s s'} (h : (𝓤 α).HasBasis p s) (h' : (𝓤 β).HasBasis p' s') {f : α → β} : - UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ + IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ (∀ j, p j → ∃ i, p' i ∧ ∀ x y, (f x, f y) ∈ s' i → (x, y) ∈ s j) := by - simp only [h.uniformEmbedding_iff' h', h.uniformContinuous_iff h'] + simp only [h.isUniformEmbedding_iff' h', h.uniformContinuous_iff h'] -theorem uniformEmbedding_subtype_val {p : α → Prop} : - UniformEmbedding (Subtype.val : Subtype p → α) := +@[deprecated (since := "2024-10-01")] +alias Filter.HasBasis.uniformEmbedding_iff := Filter.HasBasis.isUniformEmbedding_iff + +theorem isUniformEmbedding_subtype_val {p : α → Prop} : + IsUniformEmbedding (Subtype.val : Subtype p → α) := { comap_uniformity := rfl inj := Subtype.val_injective } -theorem uniformEmbedding_set_inclusion {s t : Set α} (hst : s ⊆ t) : - UniformEmbedding (inclusion hst) where +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_subtype_val := isUniformEmbedding_subtype_val + +theorem isUniformEmbedding_set_inclusion {s t : Set α} (hst : s ⊆ t) : + IsUniformEmbedding (inclusion hst) where comap_uniformity := by rw [uniformity_subtype, uniformity_subtype, comap_comap]; rfl inj := inclusion_injective hst -theorem UniformEmbedding.comp {g : β → γ} (hg : UniformEmbedding g) {f : α → β} - (hf : UniformEmbedding f) : UniformEmbedding (g ∘ f) := +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_set_inclusion := isUniformEmbedding_set_inclusion + +theorem IsUniformEmbedding.comp {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} + (hf : IsUniformEmbedding f) : IsUniformEmbedding (g ∘ f) := { hg.toUniformInducing.comp hf.toUniformInducing with inj := hg.inj.comp hf.inj } -theorem UniformEmbedding.of_comp_iff {g : β → γ} (hg : UniformEmbedding g) {f : α → β} : - UniformEmbedding (g ∘ f) ↔ UniformEmbedding f := by - simp_rw [uniformEmbedding_iff, hg.toUniformInducing.of_comp_iff, hg.inj.of_comp_iff f] +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.comp := IsUniformEmbedding.comp -theorem Equiv.uniformEmbedding {α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β) - (h₁ : UniformContinuous f) (h₂ : UniformContinuous f.symm) : UniformEmbedding f := - uniformEmbedding_iff'.2 ⟨f.injective, h₁, by rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]⟩ +theorem IsUniformEmbedding.of_comp_iff {g : β → γ} (hg : IsUniformEmbedding g) {f : α → β} : + IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f := by + simp_rw [isUniformEmbedding_iff, hg.toUniformInducing.of_comp_iff, hg.inj.of_comp_iff f] -theorem uniformEmbedding_inl : UniformEmbedding (Sum.inl : α → α ⊕ β) := - uniformEmbedding_iff'.2 ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs => +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.of_comp_iff := IsUniformEmbedding.of_comp_iff + +theorem Equiv.isUniformEmbedding {α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β) + (h₁ : UniformContinuous f) (h₂ : UniformContinuous f.symm) : IsUniformEmbedding f := + isUniformEmbedding_iff'.2 ⟨f.injective, h₁, by rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]⟩ + +@[deprecated (since := "2024-10-01")] +alias Equiv.uniformEmbedding := Equiv.isUniformEmbedding + +theorem isUniformEmbedding_inl : IsUniformEmbedding (Sum.inl : α → α ⊕ β) := + isUniformEmbedding_iff'.2 ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs => ⟨Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr), union_mem_sup (image_mem_map hs) range_mem_map, fun x h => by simpa [Prod.map_apply'] using h⟩⟩ -theorem uniformEmbedding_inr : UniformEmbedding (Sum.inr : β → α ⊕ β) := - uniformEmbedding_iff'.2 ⟨Sum.inr_injective, uniformContinuous_inr, fun s hs => +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_inl := isUniformEmbedding_inl + +theorem isUniformEmbedding_inr : IsUniformEmbedding (Sum.inr : β → α ⊕ β) := + isUniformEmbedding_iff'.2 ⟨Sum.inr_injective, uniformContinuous_inr, fun s hs => ⟨range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s, union_mem_sup range_mem_map (image_mem_map hs), fun x h => by simpa [Prod.map_apply'] using h⟩⟩ +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_inr := isUniformEmbedding_inr + /-- If the domain of a `UniformInducing` map `f` is a T₀ space, then `f` is injective, -hence it is a `UniformEmbedding`. -/ -protected theorem UniformInducing.uniformEmbedding [T0Space α] {f : α → β} - (hf : UniformInducing f) : UniformEmbedding f := +hence it is a `IsUniformEmbedding`. -/ +protected theorem UniformInducing.isUniformEmbedding [T0Space α] {f : α → β} + (hf : UniformInducing f) : IsUniformEmbedding f := ⟨hf, hf.inducing.injective⟩ -theorem uniformEmbedding_iff_uniformInducing [T0Space α] {f : α → β} : - UniformEmbedding f ↔ UniformInducing f := - ⟨UniformEmbedding.toUniformInducing, UniformInducing.uniformEmbedding⟩ +@[deprecated (since := "2024-10-01")] +alias UniformInducing.uniformEmbedding := UniformInducing.isUniformEmbedding + +theorem isUniformEmbedding_iff_uniformInducing [T0Space α] {f : α → β} : + IsUniformEmbedding f ↔ UniformInducing f := + ⟨IsUniformEmbedding.toUniformInducing, UniformInducing.isUniformEmbedding⟩ + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_iff_uniformInducing := isUniformEmbedding_iff_uniformInducing /-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed `s ∈ 𝓤 β`, then `f` is uniform inducing with respect to the discrete uniformity on `α`: @@ -210,28 +249,37 @@ theorem comap_uniformity_of_spaced_out {α} {f : α → β} {s : Set (β × β)} /-- If a map `f : α → β` sends any two distinct points to point that are **not** related by a fixed `s ∈ 𝓤 β`, then `f` is a uniform embedding with respect to the discrete uniformity on `α`. -/ -theorem uniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β) - (hf : Pairwise fun x y => (f x, f y) ∉ s) : @UniformEmbedding α β ⊥ ‹_› f := by +theorem isUniformEmbedding_of_spaced_out {α} {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β) + (hf : Pairwise fun x y => (f x, f y) ∉ s) : @IsUniformEmbedding α β ⊥ ‹_› f := by let _ : UniformSpace α := ⊥; have := discreteTopology_bot α - exact UniformInducing.uniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩ + exact UniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩ + +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_of_spaced_out := isUniformEmbedding_of_spaced_out -protected theorem UniformEmbedding.embedding {f : α → β} (h : UniformEmbedding f) : Embedding f := +protected lemma IsUniformEmbedding.embedding {f : α → β} (h : IsUniformEmbedding f) : Embedding f := { toInducing := h.toUniformInducing.inducing inj := h.inj } -theorem UniformEmbedding.isDenseEmbedding {f : α → β} (h : UniformEmbedding f) (hd : DenseRange f) : - IsDenseEmbedding f := +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.embedding := IsUniformEmbedding.embedding + +theorem IsUniformEmbedding.isDenseEmbedding {f : α → β} (h : IsUniformEmbedding f) + (hd : DenseRange f) : IsDenseEmbedding f := { h.embedding with dense := hd } +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.isDenseEmbedding := IsUniformEmbedding.isDenseEmbedding + @[deprecated (since := "2024-09-30")] -alias UniformEmbedding.denseEmbedding := UniformEmbedding.isDenseEmbedding +alias IsUniformEmbedding.denseEmbedding := IsUniformEmbedding.isDenseEmbedding theorem closedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopology α] [T0Space β] {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β) (hf : Pairwise fun x y => (f x, f y) ∉ s) : ClosedEmbedding f := by rcases @DiscreteTopology.eq_bot α _ _ with rfl; let _ : UniformSpace α := ⊥ exact - { (uniformEmbedding_of_spaced_out hs hf).embedding with + { (isUniformEmbedding_of_spaced_out hs hf).embedding with isClosed_range := isClosed_range_of_spaced_out hs hf } theorem closure_image_mem_nhds_of_uniformInducing {s : Set (α × α)} {e : α → β} (b : β) @@ -248,18 +296,24 @@ theorem closure_image_mem_nhds_of_uniformInducing {s : Set (α × α)} {e : α rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩ exact ⟨e x, hxV, mem_image_of_mem e hxU⟩ -theorem uniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : UniformEmbedding e) - (de : IsDenseEmbedding e) : UniformEmbedding (IsDenseEmbedding.subtypeEmb p e) := +theorem isUniformEmbedding_subtypeEmb (p : α → Prop) {e : α → β} (ue : IsUniformEmbedding e) + (de : IsDenseEmbedding e) : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) := { comap_uniformity := by simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype, ue.comap_uniformity.symm] inj := (de.subtype p).inj } -theorem UniformEmbedding.prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] - {e₁ : α → α'} {e₂ : β → β'} (h₁ : UniformEmbedding e₁) (h₂ : UniformEmbedding e₂) : - UniformEmbedding fun p : α × β => (e₁ p.1, e₂ p.2) := +@[deprecated (since := "2024-10-01")] +alias uniformEmbedding_subtypeEmb := isUniformEmbedding_subtypeEmb + +theorem IsUniformEmbedding.prod {α' : Type*} {β' : Type*} [UniformSpace α'] [UniformSpace β'] + {e₁ : α → α'} {e₂ : β → β'} (h₁ : IsUniformEmbedding e₁) (h₂ : IsUniformEmbedding e₂) : + IsUniformEmbedding fun p : α × β => (e₁ p.1, e₂ p.2) := { h₁.toUniformInducing.prod h₂.toUniformInducing with inj := h₁.inj.prodMap h₂.inj } +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.prod := IsUniformEmbedding.prod + /-- A set is complete iff its image under a uniform inducing map is complete. -/ theorem isComplete_image_iff {m : α → β} {s : Set α} (hm : UniformInducing m) : IsComplete (m '' s) ↔ IsComplete s := by @@ -273,15 +327,18 @@ theorem isComplete_image_iff {m : α → β} {s : Set α} (hm : UniformInducing theorem UniformInducing.isComplete_iff {f : α → β} {s : Set α} (hf : UniformInducing f) : IsComplete (f '' s) ↔ IsComplete s := isComplete_image_iff hf -/-- If `f : X → Y` is an `UniformEmbedding`, the image `f '' s` of a set `s` is complete +/-- If `f : X → Y` is an `IsUniformEmbedding`, the image `f '' s` of a set `s` is complete if and only if `s` is complete. -/ -theorem UniformEmbedding.isComplete_iff {f : α → β} {s : Set α} (hf : UniformEmbedding f) : +theorem IsUniformEmbedding.isComplete_iff {f : α → β} {s : Set α} (hf : IsUniformEmbedding f) : IsComplete (f '' s) ↔ IsComplete s := hf.toUniformInducing.isComplete_iff +@[deprecated (since := "2024-10-01")] +alias UniformEmbedding.isComplete_iff := IsUniformEmbedding.isComplete_iff + /-- Sets of a subtype are complete iff their image under the coercion is complete. -/ theorem Subtype.isComplete_iff {p : α → Prop} {s : Set { x // p x }} : IsComplete s ↔ IsComplete ((↑) '' s : Set α) := - uniformEmbedding_subtype_val.isComplete_iff.symm + isUniformEmbedding_subtype_val.isComplete_iff.symm alias ⟨isComplete_of_complete_image, _⟩ := isComplete_image_iff @@ -312,12 +369,12 @@ instance SeparationQuotient.instCompleteSpace [CompleteSpace α] : /-- See also `UniformInducing.completeSpace_congr` for a version that works for non-injective maps. -/ -theorem completeSpace_congr {e : α ≃ β} (he : UniformEmbedding e) : +theorem completeSpace_congr {e : α ≃ β} (he : IsUniformEmbedding e) : CompleteSpace α ↔ CompleteSpace β := he.completeSpace_congr e.surjective theorem completeSpace_coe_iff_isComplete {s : Set α} : CompleteSpace s ↔ IsComplete s := by - rw [completeSpace_iff_isComplete_range uniformEmbedding_subtype_val.toUniformInducing, + rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.toUniformInducing, Subtype.range_coe] alias ⟨_, IsComplete.completeSpace_coe⟩ := completeSpace_coe_iff_isComplete @@ -394,28 +451,34 @@ theorem totallyBounded_preimage {f : α → β} {s : Set β} (hf : UniformInduci instance CompleteSpace.sum [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α ⊕ β) := by rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr] - exact uniformEmbedding_inl.toUniformInducing.isComplete_range.union - uniformEmbedding_inr.toUniformInducing.isComplete_range + exact isUniformEmbedding_inl.toUniformInducing.isComplete_range.union + isUniformEmbedding_inr.toUniformInducing.isComplete_range end -theorem uniformEmbedding_comap {α : Type*} {β : Type*} {f : α → β} [u : UniformSpace β] - (hf : Function.Injective f) : @UniformEmbedding α β (UniformSpace.comap f u) u f := - @UniformEmbedding.mk _ _ (UniformSpace.comap f u) _ _ +theorem isUniformEmbedding_comap {α : Type*} {β : Type*} {f : α → β} [u : UniformSpace β] + (hf : Function.Injective f) : @IsUniformEmbedding α β (UniformSpace.comap f u) u f := + @IsUniformEmbedding.mk _ _ (UniformSpace.comap f u) _ _ (@UniformInducing.mk _ _ (UniformSpace.comap f u) _ _ rfl) hf +@[deprecated (since := "2024-10-01")] +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 α := (u.comap f).replaceTopology h.induced -theorem Embedding.to_uniformEmbedding {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) - (h : Embedding f) : @UniformEmbedding α β (h.comapUniformSpace f) u f := +theorem Embedding.to_isUniformEmbedding {α β} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) + (h : Embedding f) : @IsUniformEmbedding α β (h.comapUniformSpace f) u f := let _ := h.comapUniformSpace f { comap_uniformity := rfl inj := h.inj } +@[deprecated (since := "2024-10-01")] +alias Embedding.to_uniformEmbedding := Embedding.to_isUniformEmbedding + section UniformExtension variable {α : Type*} {β : Type*} {γ : Type*} [UniformSpace α] [UniformSpace β] [UniformSpace γ] @@ -434,13 +497,13 @@ theorem uniformly_extend_exists [CompleteSpace γ] (a : α) : ∃ c, Tendsto f ( CompleteSpace.complete this theorem uniform_extend_subtype [CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} - {s : Set α} (hf : UniformContinuous fun x : Subtype p => f x.val) (he : UniformEmbedding e) + {s : Set α} (hf : UniformContinuous fun x : Subtype p => f x.val) (he : IsUniformEmbedding e) (hd : ∀ x : β, x ∈ closure (range e)) (hb : closure (e '' s) ∈ 𝓝 b) (hs : IsClosed s) (hp : ∀ x ∈ s, p x) : ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c) := by have de : IsDenseEmbedding e := he.isDenseEmbedding hd have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p - have ue' : UniformEmbedding (IsDenseEmbedding.subtypeEmb p e) := - uniformEmbedding_subtypeEmb _ he de + have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) := + isUniformEmbedding_subtypeEmb _ he de have : b ∈ closure (e '' { x | p x }) := (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb) let ⟨c, hc⟩ := uniformly_extend_exists ue'.toUniformInducing de'.dense hf ⟨b, this⟩ diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt index 61a8f1beba401..de0b42c05c8e5 100644 --- a/scripts/no_lints_prime_decls.txt +++ b/scripts/no_lints_prime_decls.txt @@ -1315,7 +1315,7 @@ Filter.HasBasis.prod_nhds' Filter.HasBasis.sup' Filter.HasBasis.to_hasBasis' Filter.HasBasis.to_image_id' -Filter.HasBasis.uniformEmbedding_iff' +Filter.HasBasis.isUniformEmbedding_iff' Filter.iInf_neBot_iff_of_directed' Filter.iInf_sets_eq_finite' Filter.isScalarTower' @@ -4727,7 +4727,7 @@ uniformContinuous_mul_left' uniformContinuous_mul_right' uniformContinuous_nnnorm' uniformContinuous_norm' -uniformEmbedding_iff' +isUniformEmbedding_iff' UniformGroup.mk' uniformInducing_iff' UniformInducing.mk'