chore(*): add 3 fun_prop attrs (#14040)

leanprover-community · Jun 25, 2024 · e571678 · e571678
1 parent 92882dd
commit e571678
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Dynamics/Flow.lean b/Mathlib/Dynamics/Flow.lean
@@ -112,7 +112,7 @@ theorem ext : ∀ {ϕ₁ ϕ₂ : Flow τ α}, (∀ t x, ϕ₁ t x = ϕ₂ t x)
     exact h _ _
 #align flow.ext Flow.ext
 
-@[continuity]
+@[continuity, fun_prop]
 protected theorem continuous {β : Type*} [TopologicalSpace β] {t : β → τ} (ht : Continuous t)
     {f : β → α} (hf : Continuous f) : Continuous fun x => ϕ (t x) (f x) :=
   ϕ.cont'.comp (ht.prod_mk hf)

diff --git a/Mathlib/Topology/Algebra/GroupWithZero.lean b/Mathlib/Topology/Algebra/GroupWithZero.lean
@@ -71,7 +71,7 @@ theorem ContinuousOn.div_const (hf : ContinuousOn f s) (y : G₀) :
   simpa only [div_eq_mul_inv] using hf.mul continuousOn_const
 #align continuous_on.div_const ContinuousOn.div_const
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.div_const (hf : Continuous f) (y : G₀) : Continuous fun x => f x / y := by
   simpa only [div_eq_mul_inv] using hf.mul continuous_const
 #align continuous.div_const Continuous.div_const

diff --git a/Mathlib/Topology/Homeomorph.lean b/Mathlib/Topology/Homeomorph.lean
@@ -146,7 +146,7 @@ theorem refl_symm : (Homeomorph.refl X).symm = Homeomorph.refl X :=
   rfl
 #align homeomorph.refl_symm Homeomorph.refl_symm
 
-@[continuity]
+@[continuity, fun_prop]
 protected theorem continuous (h : X ≃ₜ Y) : Continuous h :=
   h.continuous_toFun
 #align homeomorph.continuous Homeomorph.continuous