more stuff about continuous HB

theories/homotopy.v

@@ -27,6 +27,25 @@ Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 Local Open Scope quotient_scope.
 
+HB.mixin Record IsContinuous {T U : topologicalType} (f : T -> U) :=
+  { continuous_fun : continuous f }.
+
+HB.structure Definition JustContinuous {T U : topologicalType} 
+  := {f of @IsContinuous T U f}.
+
+HB.structure Definition ContinuousFun {T U : topologicalType} 
+    (A : set T) (B : set U) := 
+  {f of 
+    @IsContinuous (subspace_topologicalType A) U f & 
+    @Fun (subspace_topologicalType A) U A B f
+  }.
+
+Notation "{ 'continuous' A >-> B }" := 
+  (@ContinuousFun.type _ _ A B) : form_scope.
+Notation "[ 'continuous' 'of' f ]" := 
+  ([the (@ContinuousFun.type _ _ _ _) of (f: _ -> _)]) : form_scope.
+
+
 HB.mixin Record IsParametrization {R : realType} (f : R -> R) := 
   { 
     parametrize_cts : {within `[0,1], continuous f};
@@ -156,26 +175,50 @@ Lemma inv_parametrization_can_l: {in `[0,1], cancel inv_parametrization f}.
 Proof.  by move=> z zI; apply: funK; rewrite mem_setE. Qed.
 
 End Inverses.
-End Parametrizations.
 
-HB.mixin Record IsContinuous {T U : topologicalType} (f : T -> U) :=
-  { continuous_fun : continuous f }.
+Definition rev_param (x : R) : R := `1- x.
 
-HB.structure Definition JustContinuous {T U : topologicalType} 
-  := {f of @IsContinuous T U f}.
+Local Lemma rev_param_funS : set_fun `[0,1]%classic `[0,1]%classic rev_param.
+Proof.
+rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP. 
+split; [exact: onem_ge0| exact: onem_le1].
+Qed.
 
-HB.structure Definition ContinuousFun {T U : topologicalType} 
-    (A : set T) (B : set U) := 
-  {f of 
-    @IsContinuous (subspace_topologicalType A) U f & 
-    @Fun (subspace_topologicalType A) U A B f
-  }.
+HB.instance Definition _ := IsFun.Build R R _ _ _ rev_param_funS.
 
-Notation "{ 'continuous' A >-> B }" := 
-  (@ContinuousFun.type _ _ A B) : form_scope.
-Notation "[ 'continuous' 'of' f ]" := 
-  ([the (@ContinuousFun.type _ _ _ _) of (f: _ -> _)]) : form_scope.
+Lemma rev_param_continuous : {within `[0,1], continuous rev_param}. 
+Proof.
+move=> z; apply: continuous_subspaceT.
+move=> ?; apply: (@continuousD R R R ); first exact: cvg_cst.
+exact: opp_continuous.
+Qed.
 
+Section Reversal.
+Local Open Scope fun_scope.
+Variables (f : {parametrization R}).
+
+Let g := rev_param \o f \o rev_param.
+
+Local Lemma rev_rev_continuous : {within `[0,1], continuous g}. 
+Proof.
+move=> x.
+apply: (@continuous_comp (subspace_topologicalType `[0,1]) (subspace_topologicalType `[0,1]) R).
+  exact/subspaceT_continuous/rev_param_continuous.
+apply: (@continuous_comp (subspace_topologicalType `[0,1]) (subspace_topologicalType `[0,1]) _). 
+  exact/subspaceT_continuous/parametrize_cts.
+exact: rev_param_continuous.
+Qed.
+
+Local Lemma rev_rev_init : g 0 = 0. 
+Proof. by rewrite /g /= /rev_param /= onem0 parametrize_final onem1. Qed.
+
+Local Lemma rev_rev_final : g 1 = 1. 
+Proof. by rewrite /g /= /rev_param /= onem1 parametrize_init onem0. Qed.
+
+HB.instance Definition _ := @IsParametrization.Build
+  _ _ rev_rev_continuous rev_rev_init rev_rev_final.
+End Reversal.
+End Parametrizations.
 Section Reparametrization.
 
 Context {R : realType} {T : topologicalType} (B : set T).
@@ -245,7 +288,7 @@ Qed.
 
 Canonical pi_path_image_mono := PiMono1 path_image_mono.
 
-Definition path_precompose (h : R -> R) := lift_op1 Path (fun f => f \o h).
+Definition path_reverse (h : R -> R) := lift_op1 Path (fun f => f \o rev_param).
 
 End Reparametrization.
 

theories/topology.v

@@ -5822,6 +5822,13 @@ move=> ctsf; rewrite continuous_subspace_in => ? ?.
 exact: continuous_in_subspaceT.
 Qed.
 
+Lemma continuous_subspaceTE {U} (f : T -> U) : 
+  {within [set: T], continuous f} = continuous f.
+Proof. 
+rewrite propeqE; split; last exact: continuous_subspaceT. 
+by move=> + x Q nQ /= => /(_ x Q nQ) /=; rewrite nbhs_simpl /= ?nbhs_subspaceT.
+Qed.
+
 Lemma continuous_open_subspace {U} A (f : T -> U) :
   open A -> {within A, continuous f} = {in A, continuous f}.
 Proof.