diff --git a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean index 3bc2a9e12ec42c..eac472266901f4 100644 --- a/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean +++ b/Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean @@ -51,7 +51,7 @@ noncomputable def uniformEquiv_unitization_addEquiv_prod : WithLp 1 (Unitization 𝕜 A) ≃ᵤ WithLp 1 (𝕜 × A) := { unitization_addEquiv_prod 𝕜 A with uniformContinuous_invFun := uniformContinuous_comap' uniformContinuous_id - uniformContinuous_toFun := uniformContinuous_iff.mpr le_rfl } + uniformContinuous_toFun := uniformContinuous_iff_le_comap.mpr le_rfl } instance instCompleteSpace [CompleteSpace 𝕜] [CompleteSpace A] : CompleteSpace (WithLp 1 (Unitization 𝕜 A)) := diff --git a/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean b/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean index b82e2581436e08..2dda7201c9e185 100644 --- a/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean +++ b/Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean @@ -195,7 +195,7 @@ theorem coverEntropy_image_le_of_uniformContinuous [UniformSpace X] [UniformSpac {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) : coverEntropy T (φ '' F) ≤ coverEntropy S F := by rw [coverEntropy_image_of_comap _ h F] - exact coverEntropy_antitone S F (uniformContinuous_iff.1 h') + exact coverEntropy_antitone S F (uniformContinuous_iff_le_comap.1 h') /-- The entropy of `φ '' F` is at most the entropy of `F` if `φ` is uniformly continuous. This version uses a `liminf`. -/ @@ -203,7 +203,7 @@ theorem coverEntropyInf_image_le_of_uniformContinuous [UniformSpace X] [UniformS {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) : coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F := by rw [coverEntropyInf_image_of_comap _ h F] - exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h') + exact coverEntropyInf_antitone S F (uniformContinuous_iff_le_comap.1 h') lemma coverEntropy_image_le_of_uniformContinuousOn_invariant [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) {F G : Set X} diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean index 812dc6c398e1e4..455156e1b1096e 100644 --- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean +++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean @@ -338,8 +338,8 @@ def opUniformEquivRight letI : UniformSpace G := IsTopologicalGroup.rightUniformSpace G letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ refine ⟨MulOpposite.opEquiv, ?_, ?_⟩ - · simp [uniformContinuous_iff, ← comap_op_leftUniformSpace] - · simp [uniformContinuous_iff, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap] + · simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace] + · simp [uniformContinuous_iff_le_comap, ← comap_op_leftUniformSpace, ← UniformSpace.comap_comap] /-- The equivalence between a topological group `G` and `Gᵐᵒᵖ` as a uniform equivalence when `G` is equipped with the left uniformity and `Gᵐᵒᵖ` with the right uniformity. -/ @@ -352,8 +352,8 @@ def opUniformEquivLeft letI : UniformSpace G := IsTopologicalGroup.leftUniformSpace G letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ refine ⟨MulOpposite.opEquiv, ?_, ?_⟩ - · simp [uniformContinuous_iff, ← comap_op_rightUniformSpace] - · simp [uniformContinuous_iff, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap] + · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace] + · simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap] end MulOpposite @@ -381,11 +381,11 @@ def UniformEquiv.inv : @UniformEquiv G G (IsTopologicalGroup.rightUniformSpace G (IsTopologicalGroup.leftUniformSpace G) := by have A : @UniformContinuous G G (IsTopologicalGroup.rightUniformSpace G) (IsTopologicalGroup.leftUniformSpace G) (Equiv.inv G) := by - apply uniformContinuous_iff.2 + apply uniformContinuous_iff_le_comap.2 rw [← comap_inv_leftUniformSpace] have B : @UniformContinuous G G (IsTopologicalGroup.leftUniformSpace G) (IsTopologicalGroup.rightUniformSpace G) (Equiv.inv G) := by - apply uniformContinuous_iff.2 + apply uniformContinuous_iff_le_comap.2 rw [← comap_inv_leftUniformSpace, ← UniformSpace.comap_comap] simp exact @UniformEquiv.mk G G (IsTopologicalGroup.rightUniformSpace G) diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 890f5efd1ed61d..d0cc87e0dec70c 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -454,13 +454,16 @@ theorem UniformSpace.comap_mono {α γ} {f : α → γ} : Monotone fun u : UniformSpace γ => u.comap f := fun _ _ hu => Filter.comap_mono hu -theorem uniformContinuous_iff {α β} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} : - UniformContinuous f ↔ uα ≤ uβ.comap f := +theorem uniformContinuous_iff_le_comap {α β} {uα : UniformSpace α} {uβ : UniformSpace β} + {f : α → β} : UniformContinuous f ↔ uα ≤ uβ.comap f := Filter.map_le_iff_le_comap +@[deprecated (since := "2026-05-23")] +alias uniformContinuous_iff := uniformContinuous_iff_le_comap + theorem le_iff_uniformContinuous_id {u v : UniformSpace α} : u ≤ v ↔ @UniformContinuous _ _ u v id := by - rw [uniformContinuous_iff, uniformSpace_comap_id, id] + rw [uniformContinuous_iff_le_comap, uniformSpace_comap_id, id] theorem uniformContinuous_comap {f : α → β} [u : UniformSpace β] : @UniformContinuous α β (UniformSpace.comap f u) u f := @@ -520,7 +523,7 @@ variable [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β} { theorem UniformContinuous.continuous (hf : UniformContinuous f) : Continuous f := continuous_iff_le_induced.mpr <| UniformSpace.toTopologicalSpace_mono <| - uniformContinuous_iff.1 hf + uniformContinuous_iff_le_comap.1 hf lemma UniformContinuous.uniformContinuousOn (hf : UniformContinuous f) : UniformContinuousOn f s := diff --git a/Mathlib/Topology/UniformSpace/DiscreteUniformity.lean b/Mathlib/Topology/UniformSpace/DiscreteUniformity.lean index a7c38fef30a554..e9e3813a70882c 100644 --- a/Mathlib/Topology/UniformSpace/DiscreteUniformity.lean +++ b/Mathlib/Topology/UniformSpace/DiscreteUniformity.lean @@ -84,6 +84,6 @@ variable {x} in /-- On a space with a discrete uniformity, any function is uniformly continuous. -/ theorem uniformContinuous {Y : Type*} [UniformSpace Y] (f : X → Y) : UniformContinuous f := by - simp only [uniformContinuous_iff, DiscreteUniformity.eq_bot, bot_le] + simp only [uniformContinuous_iff_le_comap, DiscreteUniformity.eq_bot, bot_le] end DiscreteUniformity diff --git a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean index 3ed0b24930d838..b5e7ffb01774e7 100644 --- a/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean +++ b/Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean @@ -404,10 +404,10 @@ protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) : UniformContinuous (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) := by -- This is a direct consequence of `UniformFun.comap_eq` - refine uniformContinuous_iff.mpr ?_ + refine uniformContinuous_iff_le_comap.mpr ?_ calc 𝒰(α, γ, _) ≤ 𝒰(α, γ, ‹UniformSpace β›.comap f) := - UniformFun.mono (uniformContinuous_iff.mp hf) + UniformFun.mono (uniformContinuous_iff_le_comap.mp hf) _ = 𝒰(α, β, _).comap (f ∘ ·) := by exact UniformFun.comap_eq /-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ γ) ≃ᵤ (α →ᵤ β)` by @@ -892,8 +892,9 @@ More precisely, if `f : γ → β` is uniformly continuous, then protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) : UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by -- This is a direct consequence of `UniformOnFun.comap_eq` - rw [uniformContinuous_iff] - exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq + rw [uniformContinuous_iff_le_comap] + exact (UniformOnFun.mono (uniformContinuous_iff_le_comap.mp hf) + subset_rfl).trans_eq UniformOnFun.comap_eq /-- Post-composition by a uniform inducing is a uniform inducing for the uniform structures of `𝔖`-convergence. @@ -1120,9 +1121,9 @@ theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union, ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_) - · rw [← uniformContinuous_iff] + · rw [← uniformContinuous_iff_le_comap] exact UniformOnFun.precomp_uniformContinuous h_image₁ - · rw [← uniformContinuous_iff] + · rw [← uniformContinuous_iff_le_comap] exact UniformOnFun.precomp_uniformContinuous h_image₂ · simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf, ← UniformSpace.comap_comap] @@ -1145,7 +1146,7 @@ theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ -- With a better theory of ideals we may be able to simplify the following by replacing `𝔗 i` -- by `(φ i ⁻¹' ·) '' 𝔖`. refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_) - · rw [← uniformContinuous_iff] + · rw [← uniformContinuous_iff_le_comap] exact UniformOnFun.precomp_uniformContinuous (h_image i) · simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap] exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl