generalize continuous_comp_cvg

CHANGELOG_UNRELEASED.md

@@ -41,6 +41,9 @@
   + `elementary_functions/trigonometry_functions.v`
   + `elementary_functions/trigonometry_integral.v`
 
+- in `topology_structure.v`:
+  + lemma `id_continuous`
+
 ### Changed
 
 - in `derive.v`:
@@ -84,6 +87,9 @@
 - in `esum.v`:
   + lemmma `le_esum`
 
+- from `pseudometric_normed_Zmodule.v` to `topology_structure.v`:
+  + lemma `continuous_comp_cvg`
+
 ### Deprecated
 
 ### Removed

theories/ftc.v

@@ -1857,8 +1857,8 @@ rewrite onemK onem1 => -> //; last 1 first.
 split => /=.
 - by move=> x xr1; exact: derivableB.
 - apply: cvg_at_right_filter; rewrite onemK.
-  apply: (@continuous_comp_cvg _ _ _ _ onem)=> //=.
-    by move=> x; apply: continuousB => //; exact: cst_continuous.
+  apply/continuous_comp_cvg => /=.
+    by apply: continuousB; [exact: cst_continuous |exact: id_continuous].
   by under eq_fun do rewrite -/(onem _) onemK; exact: cvg_id.
 - by apply: cvg_at_left_filter; exact: cvgB.
 Qed.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -850,20 +850,6 @@ Arguments cvgr_neq0 {R V T F FF f}.
 #[global] Hint Extern 0 (ProperFilter _^'+) =>
   (apply: at_right_proper_filter) : typeclass_instances.
 
-Lemma continuous_comp_cvg {R : numFieldType} (U V : pseudoMetricNormedZmodType R)
-  (f : U -> V) (g : R -> U) (r : R) (l : V) : continuous f ->
-  (f \o g) x @[x --> r] --> l -> f x @[x --> g r] --> l.
-Proof.
-move=> cf fgl; apply/(@cvgrPdist_le _ V) => /= e e0.
-have e20 : 0 < e / 2 by rewrite divr_gt0.
-move/(@cvgrPdist_le _ V) : fgl => /(_ _ e20) fgl.
-have /(@cvgrPdist_le _ V) /(_ _ e20) fgf := cf (g r).
-rewrite !near_simpl/=; near=> t.
-rewrite -(@subrK _ (f (g r)) l) -(addrA (_ + _)) (le_trans (ler_normD _ _))//.
-rewrite (splitr e) lerD//; last by near: t.
-by case: fgl => d /= d0; apply; rewrite /ball_/= subrr normr0.
-Unshelve. all: by end_near. Qed.
-
 Section closure_left_right_open.
 Variable R : realFieldType.
 Implicit Types z : R.

theories/topology_theory/topology_structure.v

@@ -319,6 +319,18 @@ move=> h_continuous fa fb; apply: (cvg_trans _ h_continuous).
 exact: (cvg_comp _ (fun x => h x.1 x.2) (cvg_pair fa fb)).
 Qed.
 
+Lemma continuous_comp_cvg {T V U : topologicalType}
+  (f : T -> V) (h : V -> U) (r : T) (l : U) :
+  {for f r, continuous h} ->
+  (h \o f) x @[x --> r] --> l -> h x @[x --> f r] --> l.
+Proof.
+move=> frh hfrl X; rewrite nbhsE => -[Y [oY Yl]].
+move/filterS; apply; apply: frh.
+rewrite nbhsE; exists Y => //; split => //.
+have /hfrl : nbhs l Y by exact: open_nbhs_nbhs.
+by rewrite nbhsE => -[W [oW Wr]]; exact.
+Qed.
+
 Lemma cvg_near_cst (T : Type) (U : topologicalType)
   (l : U) (f : T -> U) (F : set_system T) {FF : Filter F} :
   (\forall x \near F, f x = l) -> f @ F --> l.
@@ -362,6 +374,9 @@ Lemma cst_continuous {T U : topologicalType} (x : U) :
   continuous (fun _ : T => x).
 Proof. by move=> t; exact: cvg_cst. Qed.
 
+Lemma id_continuous {T : topologicalType} : continuous (@id T).
+Proof. by move=> t; exact: cvg_id. Qed.
+
 Section within_topologicalType.
 Context {T : topologicalType} (A : set T).
 Implicit Types B : set T.
@@ -1070,8 +1085,8 @@ HB.instance Definition _ {X Y : nbhsType} (f: X -> Y) (f_cts : continuous f) :=
   @isContinuous.Build X Y (mkcts f_cts) f_cts.
 
 Section continuous_comp.
-Context {X Y Z : topologicalType}.
-Context (f : continuousType X Y) (g : continuousType Y Z).
+Context {X Y Z : topologicalType}
+  (f : continuousType X Y) (g : continuousType Y Z).
 
 #[local] Lemma cts_fun_comp : continuous (g \o f).
 Proof. move=> x; apply: continuous_comp; exact: continuous_fun. Qed.
@@ -1083,10 +1098,7 @@ End continuous_comp.
 Section continuous_id.
 Context {X : topologicalType}.
 
-#[local] Lemma cts_id : continuous (@idfun X).
-Proof. by move=> ?. Qed.
-
-HB.instance Definition _ := @isContinuous.Build X X (@idfun X) cts_id.
+HB.instance Definition _ := @isContinuous.Build X X (@idfun X) id_continuous.
 
 End continuous_id.