Skip to content

[Merged by Bors] - chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap #39762

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
plp127 wants to merge 2 commits into from
Closed

[Merged by Bors] - chore(Topology/UniformSpace): rename uniformContinuous_iff to uniformContinuous_iff_le_comap #39762

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8354f86
rename
plp127 May 24, 2026
e994632
fix long line
plp127 May 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) :=
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,15 +195,15 @@ 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`. -/
theorem coverEntropyInf_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X}
{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}
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand All @@ -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

Expand Down Expand Up @@ -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)
Expand Down
11 changes: 7 additions & 4 deletions Mathlib/Topology/UniformSpace/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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 :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/UniformSpace/DiscreteUniformity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
15 changes: 8 additions & 7 deletions Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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]
Expand All @@ -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
Expand Down
Loading