chore(analysis/normed_space/basic): add continuous_at.inv', `contin…

…uous.div` etc (#4667)

Also add `continuous_on_(cos/sin)`.

src/analysis/normed_space/basic.lean

@@ -758,14 +758,44 @@ lemma filter.tendsto.inv' [normed_field α] {l : filter β} {f : β → α} {y :
   tendsto (λx, (f x)⁻¹) l (𝓝 y⁻¹) :=
 (normed_field.tendsto_inv hy).comp h
 
+lemma continuous_at.inv' [topological_space α] [normed_field β] {f : α → β} {x : α}
+  (hf : continuous_at f x) (hx : f x ≠ 0) :
+  continuous_at (λ x, (f x)⁻¹) x :=
+hf.inv' hx
+
+lemma continuous_within_at.inv' [topological_space α] [normed_field β] {f : α → β} {x : α}
+  {s : set α} (hf : continuous_within_at f s x) (hx : f x ≠ 0) :
+  continuous_within_at (λ x, (f x)⁻¹) s x :=
+hf.inv' hx
+
+lemma continuous.inv' [topological_space α] [normed_field β] {f : α → β} (hf : continuous f)
+  (h0 : ∀ x, f x ≠ 0) : continuous (λ x, (f x)⁻¹) :=
+continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).inv' (h0 x)
+
+lemma continuous_on.inv' [topological_space α] [normed_field β] {f : α → β} {s : set α}
+  (hf : continuous_on f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
+  continuous_on (λ x, (f x)⁻¹) s :=
+λ x hx, (hf x hx).inv' (h0 x hx)
+
+lemma filter.tendsto.div_const [normed_field α] {l : filter β} {f : β → α} {x y : α}
+  (hf : tendsto f l (𝓝 x)) : tendsto (λa, f a / y) l (𝓝 (x / y)) :=
+hf.mul tendsto_const_nhds
+
 lemma filter.tendsto.div [normed_field α] {l : filter β} {f g : β → α} {x y : α}
   (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) (hy : y ≠ 0) :
   tendsto (λa, f a / g a) l (𝓝 (x / y)) :=
 hf.mul (hg.inv' hy)
 
-lemma filter.tendsto.div_const [normed_field α] {l : filter β} {f : β → α} {x y : α}
-  (hf : tendsto f l (𝓝 x)) : tendsto (λa, f a / y) l (𝓝 (x / y)) :=
-by { simp only [div_eq_inv_mul], exact tendsto_const_nhds.mul hf }
+lemma continuous_within_at.div [topological_space α] [normed_field β] {f : α → β} {g : α → β}
+  {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x)
+  (hnz : g x ≠ 0) :
+  continuous_within_at (λ x, f x / g x) s x :=
+hf.div hg hnz
+
+lemma continuous_on.div [topological_space α] [normed_field β] {f : α → β} {g : α → β}
+  {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) (hnz : ∀ x ∈ s, g x ≠ 0) :
+  continuous_on (λ x, f x / g x) s :=
+λ x hx, (hf x hx).div (hg x hx) (hnz x hx)
 
 /-- Continuity at a point of the result of dividing two functions
 continuous at that point, where the denominator is nonzero. -/
@@ -774,6 +804,11 @@ lemma continuous_at.div [topological_space α] [normed_field β] {f : α → β}
   continuous_at (λ x, f x / g x) x :=
 hf.div hg hnz
 
+lemma continuous.div [topological_space α] [normed_field β] {f : α → β} {g : α → β}
+  (hf : continuous f) (hg : continuous g) (h0 : ∀ x, g x ≠ 0) :
+  continuous (λ x, f x / g x) :=
+continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).div (hg.tendsto x) (h0 x)
+
 namespace real
 
 lemma norm_eq_abs (r : ℝ) : ∥r∥ = abs r := rfl

src/analysis/special_functions/trigonometric.lean

@@ -56,6 +56,8 @@ funext $ λ x, (has_deriv_at_sin x).deriv
 lemma continuous_sin : continuous sin :=
 differentiable_sin.continuous
 
+lemma continuous_on_sin {s : set ℂ} : continuous_on sin s := continuous_sin.continuous_on
+
 lemma measurable_sin : measurable sin := continuous_sin.measurable
 
 /-- The complex cosine function is everywhere differentiable, with the derivative `-sin x`. -/
@@ -83,6 +85,8 @@ funext $ λ x, deriv_cos
 lemma continuous_cos : continuous cos :=
 differentiable_cos.continuous
 
+lemma continuous_on_cos {s : set ℂ} : continuous_on cos s := continuous_cos.continuous_on
+
 lemma measurable_cos : measurable cos := continuous_cos.measurable
 
 /-- The complex hyperbolic sine function is everywhere differentiable, with the derivative `cosh x`. -/
@@ -331,6 +335,8 @@ funext $ λ _, deriv_cos
 lemma continuous_cos : continuous cos :=
 differentiable_cos.continuous
 
+lemma continuous_on_cos {s} : continuous_on cos s := continuous_cos.continuous_on
+
 lemma measurable_cos : measurable cos := continuous_cos.measurable
 
 lemma has_deriv_at_sinh (x : ℝ) : has_deriv_at sinh (cosh x) x :=
@@ -538,7 +544,7 @@ end
 namespace real
 
 lemma exists_cos_eq_zero : 0 ∈ cos '' Icc (1:ℝ) 2 :=
-intermediate_value_Icc' (by norm_num) continuous_cos.continuous_on
+intermediate_value_Icc' (by norm_num) continuous_on_cos
   ⟨le_of_lt cos_two_neg, le_of_lt cos_one_pos⟩
 
 /-- The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
@@ -806,7 +812,7 @@ by convert intermediate_value_Icc
   continuous_sin.continuous_on; simp only [sin_neg, sin_pi_div_two]
 
 lemma exists_cos_eq : (Icc (-1) 1 : set ℝ) ⊆ cos '' Icc 0 π :=
-by convert intermediate_value_Icc' real.pi_pos.le real.continuous_cos.continuous_on;
+by convert intermediate_value_Icc' real.pi_pos.le real.continuous_on_cos;
   simp only [real.cos_pi, real.cos_zero]
 
 lemma range_cos : range cos = (Icc (-1) 1 : set ℝ) :=
@@ -1855,12 +1861,11 @@ lemma differentiable_at_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π /
 @[simp] lemma deriv_tan {x : ℂ} (h : ∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) : deriv tan x = 1 / (cos x)^2 :=
 (has_deriv_at_tan h).deriv
 
-lemma continuous_tan : continuous (λ x : {x | cos x ≠ 0}, tan x) :=
-(continuous_sin.comp continuous_subtype_val).mul
-  (continuous.inv subtype.property (continuous_cos.comp continuous_subtype_val))
-
 lemma continuous_on_tan : continuous_on tan {x | cos x ≠ 0} :=
-by { rw continuous_on_iff_continuous_restrict, convert continuous_tan }
+continuous_on_sin.div continuous_on_cos $ λ x, id
+
+lemma continuous_tan : continuous (λ x : {x | cos x ≠ 0}, tan x) :=
+continuous_on_iff_continuous_restrict.1 continuous_on_tan
 
 end complex