diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean index 72bb5429eaa6f..0579779a304d6 100644 --- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean +++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean @@ -194,7 +194,7 @@ theorem uniformContinuous_map : UniformContinuous (map f) := pkg.uniformContinuous_extend #align abstract_completion.uniform_continuous_map AbstractCompletion.uniformContinuous_map --- @[continuity] -- Porting note: Add tag once implemented +@[continuity] theorem continuous_map : Continuous (map f) := pkg.continuous_extend #align abstract_completion.continuous_map AbstractCompletion.continuous_map diff --git a/Mathlib/Topology/UniformSpace/Equiv.lean b/Mathlib/Topology/UniformSpace/Equiv.lean index 2c19f8884e776..b3df76008b37d 100644 --- a/Mathlib/Topology/UniformSpace/Equiv.lean +++ b/Mathlib/Topology/UniformSpace/Equiv.lean @@ -141,7 +141,7 @@ protected theorem uniformContinuous (h : α ≃ᵤ β) : UniformContinuous h := h.uniformContinuous_toFun #align uniform_equiv.uniform_continuous UniformEquiv.uniformContinuous ---@[continuity] -- Porting note: missing attribute +@[continuity] protected theorem continuous (h : α ≃ᵤ β) : Continuous h := h.uniformContinuous.continuous #align uniform_equiv.continuous UniformEquiv.continuous @@ -151,7 +151,7 @@ protected theorem uniformContinuous_symm (h : α ≃ᵤ β) : UniformContinuous #align uniform_equiv.uniform_continuous_symm UniformEquiv.uniformContinuous_symm -- otherwise `by continuity` can't prove continuity of `h.to_equiv.symm` ---@[continuity] -- Porting note: missing attribute +@[continuity] protected theorem continuous_symm (h : α ≃ᵤ β) : Continuous h.symm := h.uniformContinuous_symm.continuous #align uniform_equiv.continuous_symm UniformEquiv.continuous_symm