Subspace topology restrictions (#739)

* changing susbapce names

* updating changelog

* linting

* changing names

* fixing names

* update changelog

* changelog fix

* fix within-continuous notation

- various minor shortenings

* name improvements

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -3,11 +3,16 @@
 ## [Unreleased]
 
 ### Added
+- in `topology.v`:
+  + lemmas `continuous_subspaceT`, `subspaceT_continuous`
 
 ### Changed
 
 ### Renamed
 
+- in `topology.v`:
+  + renamed `continuous_subspaceT` to `continuous_in_subspaceT`
+
 ### Removed
 
 ### Infrastructure

theories/derive.v

@@ -1507,7 +1507,7 @@ have gdrvbl x : x \in `]a, b[%R -> derivable g x 1.
   by move=> /fdrvbl dfx; apply: derivableB => //; exact/derivable1_diffP.
 have gcont : {within `[a, b], continuous g}.
   move=> x; apply: continuousD _ ; first by move=>?; exact: fcont.
-  by apply/continuousN/continuous_subspaceT => ? ?; exact: scalel_continuous.
+  by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.

theories/exp.v

@@ -442,7 +442,7 @@ Proof.
 move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1.
 have [x1 x1Ix| |x1 _ /eqP] := @IVT _ (fun y => expR y - x) _ _ 0 x_ge0.
 - apply: continuousB => // y1; last exact: cst_continuous.
-  by apply/continuous_subspaceT=> ? _; exact: continuous_expR.
+  by apply/continuous_subspaceT=> ?; exact: continuous_expR.
 - rewrite expR0; have [_| |] := ltrgtP (1- x) (expR x - x).
   + by rewrite subr_le0 x_ge1 subr_ge0 (le_trans _ (expR_ge1Dx _)) ?ler_addr.
   + by rewrite ltr_add2r expR_lt1 ltNge x_ge0.

theories/realfun.v

@@ -32,7 +32,7 @@ Implicit Types (a b : R) (f g : R -> R).
 Lemma continuous_subspace_itv (I : interval R) (f : R -> R) :
   {in I, continuous f} -> {within [set` I], continuous f}.
 Proof.
-move=> ctsf; apply: continuous_subspaceT => x Ix; apply: ctsf.
+move=> ctsf; apply: continuous_in_subspaceT => x Ix; apply: ctsf.
 by move: Ix; rewrite inE.
 Qed.
 
@@ -51,10 +51,10 @@ gen have main : f / forall c, {in I, continuous f} -> {in I &, injective f} ->
   have intP := interval_is_interval aI bI.
   have cI : c \in I by rewrite intP// (ltW aLc) ltW.
   have ctsACf : {within `[a, c], continuous f}.
-    apply: continuous_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
+    apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
     by rewrite intP// axc/= (le_trans _ (ltW cLb))// axc.
   have ctsCBf : {within `[c,b], continuous f}.
-    apply: continuous_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
+    apply: continuous_in_subspaceT => x; rewrite inE => /itvP axc; apply: fC.
     by rewrite intP// axc andbT (le_trans (ltW aLc)) ?axc.
   have [aLb alb'] : a < b /\ a <= b by rewrite ltW (lt_trans aLc).
   have [faLfc|fcLfa|/eqP faEfc] /= := ltrgtP (f a) (f c).
@@ -487,7 +487,7 @@ move=> Hd.
 wlog xLy : x y / x <= y by move=> H; case: (leP x y) => [/H |/ltW /H].
 rewrite -(subKr (f y) (f x)).
 have [| _ _] := MVT_segment xLy; last by rewrite mul0r => ->; rewrite subr0.
-apply/continuous_subspaceT => r _.
+apply/continuous_subspaceT=> r.
 exact/differentiable_continuous/derivable1_diffP.
 Qed.
 

theories/topology.v

@@ -5772,8 +5772,8 @@ Global Instance subspace_proper_filter {T : topologicalType}
      (A : set T) (x : subspace A) :
    ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x.
 
-Notation "{ 'within'  A , 'continuous'  f }" :=
-  (continuous (f : (subspace A) -> _)).
+Notation "{ 'within' A , 'continuous' f }" :=
+  (continuous (f : subspace A -> _)).
 
 Section SubspaceRelative.
 Context {T : topologicalType}.
@@ -5812,19 +5812,26 @@ apply: (cvg_trans _ ctsf); apply: cvg_fmap2; apply: cvg_within.
 by rewrite /subspace; exact: nbhs_filter.
 Qed.
 
-Lemma continuous_subspaceT {U} A (f : T -> U) :
+Lemma continuous_in_subspaceT {U} A (f : T -> U) :
   {in A, continuous f} -> {within A, continuous f}.
 Proof.
 rewrite continuous_subspace_in ?in_setP => ctsf t At.
 by apply continuous_subspaceT_for => //=; apply: ctsf.
 Qed.
 
+Lemma continuous_subspaceT{U} A (f : T -> U) :
+  continuous f -> {within A, continuous f}.
+Proof.
+move=> ctsf; rewrite continuous_subspace_in => ? ?. 
+exact: continuous_in_subspaceT => ? ?.
+Qed.
+
 Lemma continuous_open_subspace {U} A (f : T -> U) :
   open A -> {within A, continuous f} = {in A, continuous f}.
 Proof.
 rewrite openE continuous_subspace_in /= => oA; rewrite propeqE ?in_setP.
-by split => + x /[dup] Ax /oA Aox; rewrite /filter_of /= => /(_ _ Ax);
-  rewrite -(nbhs_subspace_interior Aox).
+by split => + x /[dup] Ax /oA Aox => /(_ _ Ax);
+  rewrite /filter_of -(nbhs_subspace_interior Aox).
 Qed.
 
 Lemma continuous_inP {U} A (f : T -> U) : open A ->
@@ -5848,6 +5855,17 @@ rewrite [RHS]setIUr -V2W -V1W eqEsubset; split=> ?.
 by case=> [][] ? ?; split=> []; [left; split | left | right; split | right].
 Qed.
 
+Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) :
+  {within A, continuous f} -> continuous (f : subspace A -> subspace B).
+Proof.
+move=> /continuousP ctsf; apply/continuousP => O /open_subspaceP [V [oV VBOB]].
+rewrite -open_subspaceIT; apply/open_subspaceP.
+case/open_subspaceP: (ctsf _ oV) => W [oW fVA]; exists W; split => //.
+rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //.
+- by have /[!VBOB]-[] : (V `&` B) (f x) by split => //; exact: funS.
+- by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS.
+Qed.
+
 End SubspaceRelative.
 
 Section SubspaceUniform.
@@ -6051,7 +6069,7 @@ Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) :
   forall (x : X), \forall U \near powerset_filter_from (nbhs x),
     {within U, continuous f}.
 Proof.
-split; first by move=> ? ?; near=> U; apply: continuous_subspaceT => ? ?; exact.
+split; first by move=> ? ?; near=> U; apply: continuous_subspaceT=> ?; exact.
 move=> + x => /(_ x)/near_powerset_filter_fromP.
 case; first by move=> ? ?; exact: continuous_subspaceW.
 move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U.
@@ -6177,7 +6195,7 @@ Lemma precompact_pointwise_precompact (W : set {family compact, X -> Y}) :
 Proof.
 move=> + x; rewrite ?precompactE => pcptW.
 have : compact (prod_topo_apply x @` (closure W)).
-  apply: continuous_compact => //; apply: continuous_subspaceT => g _.
+  apply: continuous_compact => //; apply: continuous_subspaceT=> g.
   move=> E nbhsE; have := (@prod_topo_apply_continuous _ _ x g E nbhsE).
   exact: (@pointwise_cvg_compact_family _ _ (nbhs g)).
 move=> /[dup]/(compact_closed hsdf)/closure_id -> /subclosed_compact.
@@ -6308,7 +6326,7 @@ apply/continuous_localP => x'; apply/near_powerset_filter_fromP.
   by move=> ? ?; exact: continuous_subspaceW.
 case: (@lcptX x') => // U; rewrite withinET => nbhsU [cptU _].
 exists U => //; apply: (uniform_limit_continuous_subspace PG _ _).
-  by near=> g; apply: continuous_subspaceT => + _; near: g; exact: GW.
+  by near=> g; apply: continuous_subspaceT; near: g; exact: GW.
 by move/fam_cvgP/(_ _ cptU) : Gf.
 Unshelve. end_near. Qed.
 

theories/trigo.v

@@ -560,10 +560,9 @@ Qed.
 Lemma cos_exists : exists2 pih : R, 1 <= pih <= 2 & cos pih = 0.
 Proof.
 have /IVT[] : minr (cos 1) (cos 2) <= (0 : R) <= maxr (cos 1) (cos 2).
-  - rewrite /minr /maxr ltNge (ltW (lt_trans cos2_lt0 cos1_gt0))/=.
-    by rewrite (ltW cos2_lt0)/= (ltW cos1_gt0).
+  - by rewrite le_maxr (ltW cos1_gt0) le_minl (ltW cos2_lt0) orbC.
   - by rewrite ler1n.
-  - by move=> *; apply/continuous_subspaceT=> ? _; exact: continuous_cos.
+  - by apply/continuous_subspaceT => ?; exact: continuous_cos.
 by move=> pih /itvP pihI chpi_eq0; exists pih; rewrite ?pihI.
 Qed.
 
@@ -577,7 +576,7 @@ case: (x =P y) => // /eqP xDy.
 have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy.
 have /(Rolle xLLs)[x1 _|x1|x1 x1I [_ x1D]] : cos x = cos y by rewrite cy0.
 - exact: derivable_cos.
-- by apply/continuous_subspaceT=> ? _; exact: continuous_cos.
+- by apply/continuous_subspaceT => ?; exact: continuous_cos.
 - have [_ /esym/eqP] := is_derive_cos x1; rewrite x1D oppr_eq0 => /eqP Hs.
   suff : 0 < sin x1 by rewrite Hs ltxx.
   apply/sin2_gt0/andP; split.
@@ -641,13 +640,13 @@ wlog : x / 0 <= x => [Hw|x_ge0].
 move=> /andP[x_gt0 xLpi2]; case: (ler0P (cos x)) => // cx_le0.
 have /IVT[]// : minr (cos 0) (cos x) <= 0 <= maxr (cos 0) (cos x).
   by rewrite cos0 /minr /maxr !ifN ?cx_le0 //= -leNgt (le_trans cx_le0).
-- by move=> *; apply/continuous_subspaceT=> ? _; apply: continuous_cos.
-move=> x1 /itvP Hx1 cx1_eq0.
+- by apply/continuous_subspaceT => ?; exact: continuous_cos.
+move=> x1 /itvP xx1 cx1_eq0.
 suff x1E : x1 = pi/2.
-  have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite Hx1.
+  have : x1 < pi / 2 by apply: le_lt_trans xLpi2; rewrite xx1.
   by rewrite x1E ltxx.
 apply: cos_02_uniq=> //; last by case pihalf_02_cos_pihalf => _ ->.
-  by rewrite Hx1 ltW // (lt_trans _ pihalf_lt2) // (le_lt_trans _ xLpi2) // Hx1.
+  by rewrite xx1 ltW // (lt_trans _ pihalf_lt2) // (le_lt_trans _ xLpi2) // xx1.
 by rewrite divr_ge0 ?(ltW pihalf_lt2)// pi_ge0.
 Qed.
 
@@ -732,7 +731,7 @@ move=> x y; rewrite !in_itv/= le_eqVlt; case: eqP => [<- _|_] /=.
   rewrite y_gt0; apply/idP.
   suff : cos y != 1 by case: ltrgtP (cos_le1 y).
   rewrite -cos0 eq_sym; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //.
-    by apply/continuous_subspaceT=> ? _; exact: continuous_cos.
+    by apply/continuous_subspaceT => ?; exact: continuous_cos.
   case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0.
   suff : 0 < sin x1 by rewrite s_eq0 ltxx.
   by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < y)) ?x1I // yI.
@@ -747,7 +746,7 @@ rewrite le_eqVlt; case: eqP => /= [-> _ | _ /andP[y_gt0 y_ltpi]].
   rewrite cospi x_ltpi; apply/idP.
   suff : cos x != -1 by case: ltrgtP (cos_geN1 x).
   rewrite -cospi; apply/eqP => /Rolle [||x1|x1 /itvP x1I [_ x1D]] //.
-    by apply/continuous_subspaceT=> ? _; exact: continuous_cos.
+    by apply/continuous_subspaceT => ?; exact: continuous_cos.
   case: (is_derive_cos x1) => _ /eqP; rewrite x1D eq_sym oppr_eq0 => /eqP s_eq0.
   suff : 0 < sin x1 by rewrite s_eq0 ltxx.
   by apply: sin_gt0_pi; rewrite x1I /= (lt_le_trans (_ : _ < x)) ?x1I.
@@ -757,8 +756,8 @@ wlog xLy : x y x_gt0 x_ltpi y_gt0 y_ltpi / x <= y => [H | ].
 case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx.
 have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy.
 rewrite xLLs -subr_gt0 -opprB; rewrite -subr_gt0 in xLLs; apply/idP.
-have [x1|z /itvP zI ->] := @MVT_segment _ cos (-sin) _ _ xLy.
-  by apply/continuous_subspaceT=> ? _; exact: continuous_cos.
+have [x1|z /itvP zI ->] := @MVT_segment _ cos (- sin) _ _ xLy.
+  by apply/continuous_subspaceT => ?; exact: continuous_cos.
 rewrite -mulNr opprK mulr_gt0 //; apply: sin_gt0_pi.
 by rewrite (lt_le_trans x_gt0) ?zI //= (le_lt_trans _ y_ltpi) ?zI.
 Qed.
@@ -870,25 +869,22 @@ Proof. by move=> /is_derive_tan[]. Qed.
 
 Lemma ltr_tan : {in `](- (pi/2)), (pi/2)[ &, {mono tan : x y / x < y}}.
 Proof.
-move=> x y.
-wlog xLy : x y / x <= y => [H | ] xB yB.
+move=> x y; wlog xLy : x y / x <= y => [H xB yB|/itvP xB /itvP yB].
   case: (lerP x y) => [/H //->//|yLx].
   by rewrite !ltNge ltW ?(ltW yLx) // H // ltW.
 case: (x =P y) => [->| /eqP xDy]; first by rewrite ltxx.
 have xLLs : x < y by rewrite le_eqVlt (negPf xDy) in xLy.
 rewrite -subr_gt0 xLLs; rewrite -subr_gt0 in xLLs; apply/idP.
 have [x1 /itvP x1I|z |] := @MVT_segment _ tan (fun x => (cos x) ^-2) _ _ xLy.
 - apply: is_derive_tan.
-  rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _  _ x) ?x1I ?(itvP xB)//=.
-  by rewrite (@le_lt_trans _  _ y) ?x1I ?(itvP yB).
-- apply/continuous_subspaceT=> ? inI; apply: continuous_tan.
-  rewrite /= inE /<=%O/= in inI; move/andP: inI => /= [? ?].
-  rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _  _ x) ?zI ?(itvP xB)//=.
-  rewrite (@le_lt_trans _  _ y) ?zI ?(itvP yB) //.
+  rewrite gt_eqF // cos_gt0_pihalf // (@lt_le_trans _  _ x) ?x1I ?xB//=.
+  by rewrite (@le_lt_trans _  _ y) ?x1I ?yB.
+- apply/continuous_in_subspaceT => ? -/[!(@mem_setE R)] /itvP inI.
+  apply: continuous_tan; rewrite gt_eqF// cos_gt0_pihalf//.
+  by rewrite (@lt_le_trans _  _ x) ?xB ?inI// (@le_lt_trans _  _ y) ?yB ?inI.
 - move=> x1 /itvP x1I ->.
   rewrite mulr_gt0 // invr_gt0 // exprn_gte0 // cos_gt0_pihalf //.
-  rewrite (@lt_le_trans _  _ x) ?x1I ?(itvP xB)//=.
-  by rewrite (@le_lt_trans _  _ y) ?x1I ?(itvP yB).
+  by rewrite (@lt_le_trans _  _ x) ?x1I ?xB//= (@le_lt_trans _  _ y) ?x1I ?yB.
 Qed.
 
 Lemma tan_inj : {in `](- (pi/2)), (pi/2)[ &, injective tan}.
@@ -917,7 +913,7 @@ have /(IVT (@pi_ge0 _))[] // : minr (f 0) (f pi) <= 0 <= maxr (f 0) (f pi).
   rewrite /f cos0 cospi /minr /maxr ltr_add2r -subr_lt0 opprK (_ : 1 + 1 = 2)//.
   by rewrite ltrn0 subr_le0 subr_ge0.
 - move=> y y0pi.
-  by apply: continuousB; apply/continuous_subspaceT=> ? ?;
+  by apply: continuousB; apply/continuous_in_subspaceT => ? ?;
     [exact: continuous_cos|exact: cst_continuous].
 - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP cosx1E.
   by case: (He x1); rewrite !x1I.
@@ -1043,7 +1039,7 @@ have /IVT[] // :
   rewrite /f sinN sin_pihalf /minr /maxr ltr_add2r -subr_gt0 opprK.
   by rewrite (_ : 1 + 1 = 2)// ltr0n/= subr_le0 subr_ge0.
 - by rewrite -subr_ge0 opprK -splitr pi_ge0.
-- by move=> *; apply: continuousB; apply/continuous_subspaceT=> ? ?;
+- by move=> *; apply: continuousB; apply/continuous_in_subspaceT => ? ?;
    [exact: continuous_sin| exact: cst_continuous].
 - rewrite /f => x1 /itvP x1I /eqP; rewrite subr_eq0 => /eqP sinx1E.
   by case: (He x1); rewrite !x1I.