chore: redistribute tags for fun_prop regarding continuity across t…

…he library (leanprover-community#10494) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
FormalMathematicsLab · Feb 14, 2024 · 98a6b53 · 98a6b53
1 parent f148b92
commit 98a6b53
Show file tree

Hide file tree

Showing 29 changed files with 135 additions and 286 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3444,7 +3444,6 @@ import Mathlib.Tactic.FunProp
 import Mathlib.Tactic.FunProp.AEMeasurable
 import Mathlib.Tactic.FunProp.Attr
 import Mathlib.Tactic.FunProp.ContDiff
-import Mathlib.Tactic.FunProp.Continuous
 import Mathlib.Tactic.FunProp.Core
 import Mathlib.Tactic.FunProp.Decl
 import Mathlib.Tactic.FunProp.Differentiable

diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean
@@ -1297,25 +1297,25 @@ section
 
 variable [TopologicalSpace α] {f : α → E}
 
-@[to_additive Continuous.norm]
+@[to_additive (attr := fun_prop) Continuous.norm]
 theorem Continuous.norm' : Continuous f → Continuous fun x => ‖f x‖ :=
   continuous_norm'.comp
 #align continuous.norm' Continuous.norm'
 #align continuous.norm Continuous.norm
 
-@[to_additive Continuous.nnnorm]
+@[to_additive (attr := fun_prop) Continuous.nnnorm]
 theorem Continuous.nnnorm' : Continuous f → Continuous fun x => ‖f x‖₊ :=
   continuous_nnnorm'.comp
 #align continuous.nnnorm' Continuous.nnnorm'
 #align continuous.nnnorm Continuous.nnnorm
 
-@[to_additive ContinuousAt.norm]
+@[to_additive (attr := fun_prop) ContinuousAt.norm]
 theorem ContinuousAt.norm' {a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖) a :=
   Tendsto.norm' h
 #align continuous_at.norm' ContinuousAt.norm'
 #align continuous_at.norm ContinuousAt.norm
 
-@[to_additive ContinuousAt.nnnorm]
+@[to_additive (attr := fun_prop) ContinuousAt.nnnorm]
 theorem ContinuousAt.nnnorm' {a : α} (h : ContinuousAt f a) : ContinuousAt (fun x => ‖f x‖₊) a :=
   Tendsto.nnnorm' h
 #align continuous_at.nnnorm' ContinuousAt.nnnorm'
@@ -1335,13 +1335,13 @@ theorem ContinuousWithinAt.nnnorm' {s : Set α} {a : α} (h : ContinuousWithinAt
 #align continuous_within_at.nnnorm' ContinuousWithinAt.nnnorm'
 #align continuous_within_at.nnnorm ContinuousWithinAt.nnnorm
 
-@[to_additive ContinuousOn.norm]
+@[to_additive (attr := fun_prop) ContinuousOn.norm]
 theorem ContinuousOn.norm' {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun x => ‖f x‖) s :=
   fun x hx => (h x hx).norm'
 #align continuous_on.norm' ContinuousOn.norm'
 #align continuous_on.norm ContinuousOn.norm
 
-@[to_additive ContinuousOn.nnnorm]
+@[to_additive (attr := fun_prop) ContinuousOn.nnnorm]
 theorem ContinuousOn.nnnorm' {s : Set α} (h : ContinuousOn f s) :
     ContinuousOn (fun x => ‖f x‖₊) s := fun x hx => (h x hx).nnnorm'
 #align continuous_on.nnnorm' ContinuousOn.nnnorm'

diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean
@@ -99,15 +99,18 @@ theorem ContinuousWithinAt.cexp (h : ContinuousWithinAt f s x) :
   h.cexp
 #align continuous_within_at.cexp ContinuousWithinAt.cexp
 
+@[fun_prop]
 nonrec
 theorem ContinuousAt.cexp (h : ContinuousAt f x) : ContinuousAt (fun y => exp (f y)) x :=
   h.cexp
 #align continuous_at.cexp ContinuousAt.cexp
 
+@[fun_prop]
 theorem ContinuousOn.cexp (h : ContinuousOn f s) : ContinuousOn (fun y => exp (f y)) s :=
   fun x hx => (h x hx).cexp
 #align continuous_on.cexp ContinuousOn.cexp
 
+@[fun_prop]
 theorem Continuous.cexp (h : Continuous f) : Continuous fun y => exp (f y) :=
   continuous_iff_continuousAt.2 fun _ => h.continuousAt.cexp
 #align continuous.cexp Continuous.cexp
@@ -146,15 +149,18 @@ theorem ContinuousWithinAt.exp (h : ContinuousWithinAt f s x) :
   h.exp
 #align continuous_within_at.exp ContinuousWithinAt.exp
 
+@[fun_prop]
 nonrec
 theorem ContinuousAt.exp (h : ContinuousAt f x) : ContinuousAt (fun y => exp (f y)) x :=
   h.exp
 #align continuous_at.exp ContinuousAt.exp
 
+@[fun_prop]
 theorem ContinuousOn.exp (h : ContinuousOn f s) : ContinuousOn (fun y => exp (f y)) s := fun x hx =>
   (h x hx).exp
 #align continuous_on.exp ContinuousOn.exp
 
+@[fun_prop]
 theorem Continuous.exp (h : Continuous f) : Continuous fun y => exp (f y) :=
   continuous_iff_continuousAt.2 fun _ => h.continuousAt.exp
 #align continuous.exp Continuous.exp

diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
@@ -435,10 +435,12 @@ theorem Filter.Tendsto.log {f : α → ℝ} {l : Filter α} {x : ℝ} (h : Tends
 
 variable [TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α}
 
+@[fun_prop]
 theorem Continuous.log (hf : Continuous f) (h₀ : ∀ x, f x ≠ 0) : Continuous fun x => log (f x) :=
   continuousOn_log.comp_continuous hf h₀
 #align continuous.log Continuous.log
 
+@[fun_prop]
 nonrec theorem ContinuousAt.log (hf : ContinuousAt f a) (h₀ : f a ≠ 0) :
     ContinuousAt (fun x => log (f x)) a :=
   hf.log h₀
@@ -449,6 +451,7 @@ nonrec theorem ContinuousWithinAt.log (hf : ContinuousWithinAt f s a) (h₀ : f
   hf.log h₀
 #align continuous_within_at.log ContinuousWithinAt.log
 
+@[fun_prop]
 theorem ContinuousOn.log (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) :
     ContinuousOn (fun x => log (f x)) s := fun x hx => (hf x hx).log (h₀ x hx)
 #align continuous_on.log ContinuousOn.log

diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean
@@ -494,15 +494,17 @@ nonrec theorem ContinuousWithinAt.sqrt (h : ContinuousWithinAt f s x) :
   h.sqrt
 #align continuous_within_at.sqrt ContinuousWithinAt.sqrt
 
+@[fun_prop]
 nonrec theorem ContinuousAt.sqrt (h : ContinuousAt f x) : ContinuousAt (fun x => sqrt (f x)) x :=
   h.sqrt
 #align continuous_at.sqrt ContinuousAt.sqrt
 
+@[fun_prop]
 theorem ContinuousOn.sqrt (h : ContinuousOn f s) : ContinuousOn (fun x => sqrt (f x)) s :=
   fun x hx => (h x hx).sqrt
 #align continuous_on.sqrt ContinuousOn.sqrt
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.sqrt (h : Continuous f) : Continuous fun x => sqrt (f x) :=
   continuous_sqrt.comp h
 #align continuous.sqrt Continuous.sqrt
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -55,7 +55,6 @@ import Mathlib.Tactic.FunProp
 import Mathlib.Tactic.FunProp.AEMeasurable
 import Mathlib.Tactic.FunProp.Attr
 import Mathlib.Tactic.FunProp.ContDiff
-import Mathlib.Tactic.FunProp.Continuous
 import Mathlib.Tactic.FunProp.Core
 import Mathlib.Tactic.FunProp.Decl
 import Mathlib.Tactic.FunProp.Differentiable

diff --git a/Mathlib/Tactic/FunProp/ContDiff.lean b/Mathlib/Tactic/FunProp/ContDiff.lean
@@ -9,7 +9,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 
 
 import Mathlib.Tactic.FunProp
-import Mathlib.Tactic.FunProp.Continuous
 import Mathlib.Tactic.FunProp.Differentiable
 
 /-!

diff --git a/Mathlib/Tactic/FunProp/Continuous.lean b/Mathlib/Tactic/FunProp/Continuous.lean
diff --git a/Mathlib/Tactic/FunProp/Differentiable.lean b/Mathlib/Tactic/FunProp/Differentiable.lean
@@ -15,7 +15,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 
 
 import Mathlib.Tactic.FunProp
-import Mathlib.Tactic.FunProp.Continuous
 
 /-!
 ## `funProp` minimal setup for Differentiable(At/On)

diff --git a/Mathlib/Tactic/FunProp/Measurable.lean b/Mathlib/Tactic/FunProp/Measurable.lean
@@ -10,7 +10,6 @@ import Mathlib.Topology.Constructions
 import Mathlib.Analysis.SpecialFunctions.Log.Basic
 
 import Mathlib.Tactic.FunProp
-import Mathlib.Tactic.FunProp.Continuous
 
 /-!
 ## `fun_prop` minimal setup for Measurable