chore(topology/*): add a few more trivial continuous_(within_)at le…

…mmas (#1842)

src/topology/algebra/group.lean

@@ -59,6 +59,17 @@ lemma filter.tendsto.inv [topological_group α] {f : β → α} {x : filter β}
   (hf : tendsto f x (𝓝 a)) : tendsto (λx, (f x)⁻¹) x (𝓝 a⁻¹) :=
 tendsto.comp (continuous_iff_continuous_at.mp (topological_group.continuous_inv α) a) hf
 
+@[to_additive]
+lemma continuous_at.inv [topological_group α] [topological_space β] {f : β → α} {x : β}
+  (hf : continuous_at f x) : continuous_at (λx, (f x)⁻¹) x :=
+hf.inv
+
+@[to_additive]
+lemma continuous_within_at.inv [topological_group α] [topological_space β] {f : β → α}
+  {s : set β} {x : β} (hf : continuous_within_at f s x) :
+  continuous_within_at (λx, (f x)⁻¹) s x :=
+hf.inv
+
 @[to_additive topological_add_group]
 instance [topological_group α] [topological_space β] [group β] [topological_group β] :
   topological_group (α × β) :=

src/topology/algebra/monoid.lean

@@ -73,6 +73,18 @@ lemma filter.tendsto.mul {f : β → α} {g : β → α} {x : filter β} {a b :
   tendsto (λx, f x * g x) x (𝓝 (a * b)) :=
 tendsto.comp (by rw [←nhds_prod_eq]; exact tendsto_mul) (hf.prod_mk hg)
 
+@[to_additive]
+lemma continuous_at.mul [topological_space β] {f : β → α} {g : β → α} {x : β}
+  (hf : continuous_at f x) (hg : continuous_at g x) :
+  continuous_at (λx, f x * g x) x :=
+hf.mul hg
+
+@[to_additive]
+lemma continuous_within_at.mul [topological_space β] {f : β → α} {g : β → α} {s : set β} {x : β}
+  (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
+  continuous_within_at (λx, f x * g x) s x :=
+hf.mul hg
+
 @[to_additive]
 lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} :
   ∀l:list γ, (∀c∈l, tendsto (f c) x (𝓝 (a c))) →

src/topology/basic.lean

@@ -695,6 +695,12 @@ lemma continuous_iff_continuous_at {f : α → β} : continuous f ↔ ∀ x, con
 lemma continuous_const {b : β} : continuous (λa:α, b) :=
 continuous_iff_continuous_at.mpr $ assume a, tendsto_const_nhds
 
+lemma continuous_at_const {x : α} {b : β} : continuous_at (λ a:α, b) x :=
+continuous_const.continuous_at
+
+lemma continuous_at_id {x : α} : continuous_at id x :=
+continuous_id.continuous_at
+
 lemma continuous_iff_is_closed {f : α → β} :
   continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
 ⟨assume hf s hs, hf (-s) hs,

src/topology/continuous_on.lean

@@ -437,8 +437,18 @@ h.congr_of_mem_nhds_within (mem_sets_of_superset self_mem_nhds_within h₁) hx
 lemma continuous_on_const {s : set α} {c : β} : continuous_on (λx, c) s :=
 continuous_const.continuous_on
 
+lemma continuous_within_at_const {b : β} {s : set α} {x : α} :
+  continuous_within_at (λ _:α, b) s x :=
+continuous_const.continuous_within_at
+
+lemma continuous_on_id {s : set α} : continuous_on id s :=
+continuous_id.continuous_on
+
+lemma continuous_within_at_id {s : set α} {x : α} : continuous_within_at id s x :=
+continuous_id.continuous_within_at
+
 lemma continuous_on_open_iff {f : α → β} {s : set α} (hs : is_open s) :
-  continuous_on f s ↔ (∀t, _root_.is_open t → is_open (s ∩ f⁻¹' t)) :=
+  continuous_on f s ↔ (∀t, is_open t → is_open (s ∩ f⁻¹' t)) :=
 begin
   rw continuous_on_iff',
   split,