feat(analysis/special_functions/exp_log): add continuity attribute …

…to `continuous_exp` (#7157)
leanprover-community · Apr 11, 2021 · fbf6219 · fbf6219
1 parent 1442f70
commit fbf6219
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/analysis/special_functions/exp_log.lean b/src/analysis/special_functions/exp_log.lean
@@ -70,7 +70,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 | 0 := rfl
 | (n+1) := by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
-lemma continuous_exp : continuous exp :=
+@[continuity] lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
 
 lemma times_cont_diff_exp : ∀ {n}, times_cont_diff ℂ n exp :=
@@ -200,7 +200,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 | 0 := rfl
 | (n+1) := by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
-lemma continuous_exp : continuous exp :=
+@[continuity] lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
 
 lemma measurable_exp : measurable exp := continuous_exp.measurable
@@ -513,7 +513,7 @@ begin
   exact exp_order_iso.symm.continuous.comp (continuous_subtype_mk _ continuous_subtype_coe.norm)
 end
 
-lemma continuous_log' : continuous (λ x : {x : ℝ // 0 < x}, log x) :=
+@[continuity] lemma continuous_log' : continuous (λ x : {x : ℝ // 0 < x}, log x) :=
 continuous_on_iff_continuous_restrict.1 $ continuous_on_log.mono $ λ x hx, ne_of_gt hx
 
 lemma continuous_at_log (hx : x ≠ 0) : continuous_at log x :=