fixed connected continuous

cleanup topology

fixing notations

minor cleanups

fixing build

more merge fixes

cleaning up names

fix build

renaming openC and closedC

updating changelog

updating changelog

CHANGELOG_UNRELEASED.md

@@ -8,6 +8,42 @@
   + lemmas `esum_ninftyP`, `esum_pinftyP`
   + lemmas `addeoo`, `daddeoo`
   + lemmas `desum_pinftyP`, `desum_ninftyP`
+  + lemmas `lee_pemull`, `lee_nemul`, `lee_pemulr`, `lee_nemulr`
+- in `sequences.v`:
+  + lemmas `ereal_cvgM_gt0_pinfty`, `ereal_cvgM_lt0_pinfty`, `ereal_cvgM_gt0_ninfty`,
+    `ereal_cvgM_lt0_ninfty`, `ereal_cvgM`
+- in `ereal.v`:
+  + lemma `fin_numM`
+  + definition `mule_def`, notation `x *? y`
+  + lemma `mule_defC`
+  + notations `\*` in `ereal_scope`, and `ereal_dual_scope`
+- in `ereal.v`:
+  + lemmas `mule_def_fin`, `mule_def_neq0_infty`, `mule_def_infty_neq0`, `neq0_mule_def`
+  + notation `\-` in `ereal_scope` and `ereal_dual_scope`
+  + lemma `fin_numB`
+  + lemmas `mule_eq_pinfty`, `mule_eq_ninfty`
+  + lemmas `fine_eq0`, `abse_eq0`
+- in `topology.v`:
+  + lemma `filter_pair_set`
+- in `topology.v`:
+  + definition `prod_topo_apply`
+  + lemmas `prod_topo_applyE`, `prod_topo_apply_continuous`, `hausdorff_product`
+- in `topology.v`:
+  + `closedC` renamed `open_closedC`
+  + `openC` renamed `closed_openC`
+  + lemmas `closedC`, `openC` 
+  + notation `'{within A, continuous f}`
+  + lemmas `continuous_subspace_in`, `nbhs_subspace_interior`
+  + lemmas`closed_subspaceP`, `closed_subspaceW`, `closure_subspaceW`
+  + lemmas `nbhs_subspace_subset`, `continuous_subspaceW`, `nbhs_subspaceT`,
+      `continuous_subspaceT_for`, `continuous_subspaceT`, `continuous_open_subspace`
+  + generalized `connected_continuous_connected`, `continuous_compact`
+- in `derive.v`
+  + lemma `MVT_segment`
+  + generalized `EVT_max`, `EVT_min`, `Rolle`, `MVT`, `ler0_derive1_nincr`, 
+        `le0r_derive1_ndecr` with subspace topology
+- in `normedtype.v`
+  + generalized `IVT` with subspace topology
 
 ### Changed
 

theories/derive.v

@@ -1301,16 +1301,15 @@ Qed.
 End Derive.
 
 Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : (* TODO : Filter not infered *)
-  a <= b -> {in `[a, b]%R, continuous f} -> exists2 c, c \in `[a, b]%R &
+  a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R &
   forall t, t \in `[a, b]%R -> f t <= f c.
 Proof.
 move=> leab fcont; set imf := [set t | (f @` `[a, b]) t].
 have imf_sup : has_sup imf.
-  split.
-    by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
-  have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
-    apply/compact_bounded/continuous_compact; last exact: segment_compact.
-    by move=> ?; rewrite inE => /fcont.
+  split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
+  have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]). 
+    apply/compact_bounded/continuous_compact =>//. 
+    by exact: segment_compact.
   exists (M + 1); apply/ubP => y /imfltM yleM.
   apply: le_trans (yleM _ _); last by rewrite ltr_addl.
   by rewrite ler_norm.
@@ -1322,14 +1321,15 @@ have {}imf_ltsup : forall t, t \in `[a, b]%R -> f t < sup imf.
   rewrite falseE; apply: imf_ltsup; exists t => //.
   apply/eqP; rewrite eq_le supleft andbT.
   by move/ubP : (sup_upper_bound imf_sup); apply; exact: imageP.
-have invf_continuous : {in `[a, b]%R, continuous (fun t => (sup imf - f t)^-1 : R)}.
-  move=> t tab; apply: cvgV => //.
-    by rewrite subr_eq0 gt_eqF // imf_ltsup.
-  by apply: cvgD; [apply: cst_continuous|apply: cvgN; apply: fcont].
-have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] :
-   bounded_set ((fun t => (sup imf - f t)^-1) @` `[a, b]).
+set g := (fun t => (sup imf - f t)^-1 : R).
+have invf_continuous : {within `[a, b], continuous g}.
+  rewrite continuous_subspace_in=> t tab; apply: cvgV => //=.
+    rewrite subr_eq0 gt_eqF // imf_ltsup // in_itv //=.
+    by rewrite inE in tab; exact tab.
+  by apply: cvgD; [apply: cst_continuous | apply: cvgN; apply (fcont t)].
+have /ex_strict_bound_gt0 [k k_gt0 /= imVfltk] : bounded_set (g @` `[a, b]).
   apply/compact_bounded/continuous_compact; last exact: segment_compact.
-  by move=> ?; rewrite inE => /invf_continuous.
+  exact: invf_continuous.
 have : exists2 y, imf y & sup imf - k^-1 < y.
   by apply: sup_adherent => //; rewrite invr_gt0.
 move=> [y] -[t tab <-] {y}.
@@ -1340,12 +1340,12 @@ by rewrite (le_lt_trans (ler_norm _) _) ?imVfltk//; apply: imageP.
 Qed.
 
 Lemma EVT_min (R : realType) (f : R -> R) (a b : R) :
-  a <= b -> {in `[a, b]%R, continuous f} -> exists2 c, c \in `[a, b]%R &
+  a <= b -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R &
   forall t, t \in `[a, b]%R -> f c <= f t.
 Proof.
 move=> leab fcont.
-have /(EVT_max leab) [c clr fcmax] : {in `[a, b]%R, continuous (- f)}.
-  by move=> ? /fcont; apply: continuousN.
+have /(EVT_max leab) [c clr fcmax] : {within `[a, b], continuous (- f)}.
+  move=> ?; apply: continuousN => ?; exact: fcont.
 by exists c => // ? /fcmax; rewrite ler_opp2.
 Qed.
 
@@ -1458,7 +1458,7 @@ Qed.
 
 Lemma Rolle (R : realType) (f : R -> R) (a b : R) :
   a < b -> (forall x, x \in `]a, b[%R -> derivable f x 1) ->
-  {in `[a, b]%R, continuous f} -> f a = f b ->
+  {within `[a, b], continuous f} -> f a = f b ->
   exists2 c, c \in `]a, b[%R & is_derive c 1 f 0.
 Proof.
 move=> ltab fdrvbl fcont faefb.
@@ -1489,61 +1489,82 @@ by case: cmaxeaVb => ->; case: cmineaVb => ->.
 Qed.
 
 Lemma MVT (R : realType) (f df : R -> R) (a b : R) :
-  a <= b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
-  {in `[a, b]%R, continuous f} ->
-  exists2 c, c \in `[a, b]%R & f b - f a = df c * (b - a).
+  a < b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
+  {within `[a, b], continuous f} ->
+  exists2 c, c \in `]a, b[%R & f b - f a = df c * (b - a).
 Proof.
-move=> leab fdrvbl fcont; move: leab; rewrite le_eqVlt => /orP [/eqP aeb|altb].
-  by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0].
+move=> altb fdrvbl fcont.
 set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl : forall x, x \in `]a, b[%R -> derivable g x 1.
   by move=> x /fdrvbl dfx; apply: derivableB => //; apply/derivable1_diffP.
-have gcont : {in `[a, b]%R, continuous g}.
-  move=> x /fcont fx; apply: continuousD fx _; apply: continuousN.
-  exact: scalel_continuous.
+have gcont : {within `[a, b], continuous g}.
+  move=> x; apply: continuousD _ ; first (move=>?; exact: fcont). 
+  by apply/continuousN/continuous_subspaceT => ? ?; apply: scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
   rewrite [_ *: _]mulrA mulrC mulrA mulVf.
     by rewrite mul1r addrCA subrr addr0.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
-exists c; first by rewrite in_itv /= ltW (itvP cab).
+exists c; first exact: cab. 
 have /fdrvbl dfc := cab; move/@derive_val: dgc0; rewrite deriveB //; last first.
   exact/derivable1_diffP.
 move/eqP; rewrite [X in _ - X]deriveE // derive_val diff_val scale1r subr_eq0.
 move/eqP->; rewrite -mulrA mulVf ?mulr1 //; apply: lt0r_neq0.
 by rewrite subr_gt0.
 Qed.
 
+(* Weakens MVT to work when the interval is a single point. *)
+Lemma MVT_segment (R : realType) (f df : R -> R) (a b : R) :
+  a <= b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) ->
+  {within `[a, b], continuous f} ->
+  exists2 c, c \in `[a, b]%R & f b - f a = df c * (b - a).
+Proof.
+move=> leab fdrvbl fcont; case: ltgtP leab => // [altb|aeb]; last first.
+  by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0].
+have [c cab D] := MVT altb fdrvbl fcont.
+by exists c => //; rewrite in_itv /= ltW (itvP cab).
+Qed.
+
 Lemma ler0_derive1_nincr (R : realType) (f : R -> R) (a b : R) :
-  (forall x, x \in `[a, b]%R -> derivable f x 1) ->
-  (forall x, x \in `[a, b]%R -> f^`() x <= 0) ->
+  (forall x, x \in `]a, b[%R -> derivable f x 1) ->
+  (forall x, x \in `]a, b[%R -> f^`() x <= 0) ->
+  {within `[a,b], continuous f} ->
   forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
 Proof.
-move=> fdrvbl dfle0 x y leax lexy leyb; rewrite -subr_ge0.
+move=> fdrvbl dfle0 ctsf x y leax lexy leyb; rewrite -subr_ge0.
+case: ltgtP lexy => // [xlty|xyb]; last first.
+  by rewrite xyb subrr.
 have itvW : {subset `[x, y]%R <= `[a, b]%R}.
   by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
+have itvWlt : {subset `]x, y[%R <= `]a, b[%R}.
+  by apply subitvP; rewrite /<=%O /= /<=%O /= leyb leax.
 have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`()z).
-  rewrite inE => /andP [/ltW lexz /ltW lezy].
+  rewrite inE => /andP [lexz lezy].
   apply: DeriveDef; last by rewrite derive1E.
   apply: fdrvbl; rewrite inE; apply/andP.
-  by split; [exact: le_trans lexz | exact: le_trans leyb].
-have [] := @MVT _ f (f^`()) x y lexy fdrv.
-  by move=> ? /itvW /fdrvbl /derivable1_diffP /differentiable_continuous.
-move=> t /itvW /dfle0 dft dftxy; rewrite -oppr_le0 opprB dftxy.
-by apply: mulr_le0_ge0 => //; rewrite subr_ge0.
+  split; [exact: le_trans lexz | apply: le_trans]; first exact: lezy.
+  by rewrite /Order.le; exact: leyb.
+have [] := @MVT _ f (f^`()) x y xlty fdrv. 
+  apply: (@continuous_subspaceW _ _ _ `[a,b]); first exact: itvW. 
+  by rewrite continuous_subspace_in.
+move=> t /itvWlt dft dftxy _; rewrite -oppr_le0 opprB dftxy. 
+apply: mulr_le0_ge0 => //; last by rewrite subr_ge0 ltW.
+exact: dfle0.
 Qed.
 
 Lemma le0r_derive1_ndecr (R : realType) (f : R -> R) (a b : R) :
-  (forall x, x \in `[a, b]%R -> derivable f x 1) ->
-  (forall x, x \in `[a, b]%R -> 0 <= f^`() x) ->
+  (forall x, x \in `]a, b[%R -> derivable f x 1) ->
+  (forall x, x \in `]a, b[%R -> 0 <= f^`() x) ->
+  {within `[a,b], continuous f} ->
   forall x y, a <= x -> x <= y -> y <= b -> f x <= f y.
 Proof.
-move=> fdrvbl dfge0 x y; rewrite -[f _ <= _]ler_opp2.
-apply: (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
-rewrite derive1E deriveN; last exact: fdrvbl.
-by rewrite oppr_le0 -derive1E; apply: dfge0.
+move=> fdrvbl dfge0 fcont x y; rewrite -[f _ <= _]ler_opp2.
+apply (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl.
+  rewrite derive1E deriveN; last exact: fdrvbl.
+  by rewrite oppr_le0 -derive1E; apply: dfge0.
+by apply: continuousN; exact: fcont.
 Qed.
 
 Lemma derive1_comp (R : realFieldType) (f g : R -> R) x :

theories/exp.v

@@ -443,8 +443,9 @@ Lemma expR_total_gt1 x :
 Proof.
 move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1.
 case: (@IVT _ (fun y => expR y - x) 0 x 0) => //.
-- by move=> x1 x1Ix; apply: continuousB => // y1;
-    [exact: continuous_expR|exact: cst_continuous].
+- move=> x1 x1Ix; apply: continuousB => // y1.
+  + by apply/continuous_subspaceT=> ? _; exact: continuous_expR.
+  + exact: cst_continuous.
 - rewrite expR0; case: (ltrgtP (1- x) (expR x - x)) => [_| |].
   + rewrite subr_le0 x_ge1 subr_ge0.
     by apply: le_trans (expR_ge1Dx _); rewrite ?ler_addr.

theories/normedtype.v

@@ -2784,20 +2784,20 @@ Qed.
 
 Lemma closed_le (y : R) : closed [set x : R | x <= y].
 Proof.
-rewrite (_ : mkset _ = ~` [set x | x > y]); first exact: closedC.
+rewrite (_ : mkset _ = ~` [set x | x > y]); first exact: open_closedC.
 by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
 Qed.
 
 Lemma closed_ge (y : R) : closed [set x : R | y <= x].
 Proof.
-rewrite (_ : mkset _ = ~` [set x | x < y]); first exact: closedC.
+rewrite (_ : mkset _ = ~` [set x | x < y]); first exact: open_closedC.
 by rewrite predeqE => x /=; rewrite leNgt; split => /negP.
 Qed.
 
 Lemma closed_eq (y : R) : closed [set x : R | x = y].
 Proof.
 rewrite [X in closed X](_ : (eq^~ _) = ~` (xpredC (eq_op^~ y))).
-  by apply: closedC; exact: open_neq.
+  by apply: open_closedC; exact: open_neq.
 by rewrite predeqE /setC => x /=; rewrite (rwP eqP); case: eqP; split.
 Qed.
 
@@ -3084,7 +3084,7 @@ split => [cE x y Ex Ey z /andP[xz zy]|].
   have [r zcA1] : {r:{posnum R}| ball z r%:num `<=` ~` closure (A true)}.
     have ? : ~ closure (A true) z.
       by move: sepA; rewrite /separated => -[] _ /disjoints_subset; apply.
-    have ? : open (~` closure (A true)) by exact/openC/closed_closure.
+    have ? : open (~` closure (A true)) by exact/closed_openC/closed_closure.
     exact/nbhsC_ball/open_nbhs_nbhs.
   pose z1 : R := z + r%:num / 2; exists z1.
   have z1y : z1 <= y.
@@ -3176,58 +3176,23 @@ rewrite {1}(splitr x) ger_addl pmulr_lle0 // => /(lt_le_trans x0);
 Qed.
 
 Lemma IVT (R : realType) (f : R -> R) (a b v : R) :
-  a <= b -> {in `[a, b], continuous f} ->
+  a <= b -> {within `[a, b], continuous f} ->
   minr (f a) (f b) <= v <= maxr (f a) (f b) ->
   exists2 c, c \in `[a, b] & f c = v.
 Proof.
 move=> leab fcont; gen have ivt : f v fcont / f a <= v <= f b ->
     exists2 c, c \in `[a, b] & f c = v; last first.
   case: (leP (f a) (f b)) => [] _ fabv; first exact: ivt.
   have [||c cab /oppr_inj] := ivt (- f) (- v); last by exists c.
-    by move=> x /fcont; apply: continuousN.
+    by move=> x; apply: continuousN; apply: fcont.
   by rewrite ler_oppr opprK ler_oppr opprK andbC.
-move=> /andP[]; rewrite le_eqVlt => /orP [/eqP<- _|ltfav].
-  by exists a => //; rewrite in_itv /= lexx leab.
-rewrite le_eqVlt => /orP [/eqP->|ltvfb].
-  by exists b => //; rewrite in_itv /= lexx leab.
-set A := [set c | (c <= b) && (f c <= v)].
-have An0 : nonempty A by exists a; apply/andP; split=> //; apply: ltW.
-have supA : has_sup A by split=> //; exists b; apply/ubP => ? /andP [].
-have supAab : sup A \in `[a, b].
-  rewrite inE; apply/andP; split; last first.
-    by apply: sup_le_ub => //; apply/ubP => ? /andP [].
-  by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leab andTb ltW.
-exists (sup A) => //; have lefsupv : f (sup A) <= v.
-  rewrite leNgt; apply/negP => ltvfsup.
-  have vltfsup : 0 < f (sup A) - v by rewrite subr_gt0.
-  have /fcont /(_ _ (nbhsx_ballx _ (PosNum vltfsup))) [_/posnumP[d] supdfe]
-    := supAab.
-  have [t At supd_t] := sup_adherent supA [gt0 of d%:num].
-  suff /supdfe : ball (sup A) d%:num t.
-    rewrite /= /ball /= ltr_norml => /andP [_].
-    by rewrite ltr_add2l ltr_oppr opprK ltNge; have /andP [_ ->] := At.
-  rewrite /= /ball /= ger0_norm.
-    by rewrite ltr_subl_addr -ltr_subl_addl.
-  by rewrite subr_ge0; move/ubP : (sup_upper_bound supA); exact.
-apply/eqP; rewrite eq_le; apply/andP; split=> //.
-rewrite -subr_le0; apply/ler0_addgt0P => _/posnumP[e].
-rewrite ler_subl_addr -ler_subl_addl ltW //.
-have /fcont /(_ _ (nbhsx_ballx _ e)) [_/posnumP[d] supdfe] := supAab.
-have atrF := at_right_proper_filter (sup A); near (at_right (sup A)) => x.
-have /supdfe /= : ball (sup A) d%:num x.
-  by near: x; rewrite /= nbhs_simpl; exists d%:num => //.
-rewrite /= => /ltr_distlC_subl; apply: le_lt_trans.
-rewrite ler_add2r ltW //; suff : forall t, t \in `](sup A), b] -> v < f t.
-  apply; rewrite inE; apply/andP; split; first by near: x; exists 1.
-  near: x; exists (b - sup A) => /=.
-    rewrite subr_gt0 lt_def (itvP supAab) andbT; apply/negP => /eqP besup.
-    by move: lefsupv; rewrite leNgt -besup ltvfb.
-  move=> t lttb ltsupt; move: lttb; rewrite /= distrC.
-  by rewrite gtr0_norm ?subr_gt0 // ltr_add2r; apply: ltW.
-move=> t; rewrite in_itv /=; case/andP => ltsupt letb.
-apply/contra_lt: ltsupt => leftv.
-by move/ubP : (sup_upper_bound supA); apply; rewrite /A/= leftv letb.
-Unshelve. all: by end_near. Qed.
+move=> favfb; suff: (is_interval (f @` `[a,b])).
+  apply; last by exact: favfb. 
+    by exists a => //=; rewrite inE /<=%O /=; apply/andP.
+  by exists b => //=; rewrite inE /<=%O /=; apply/andP.
+apply/connected_intervalP/connected_continuous_connected => //.
+exact: segment_connected.
+Qed.
 
 (** Local properties in [R] *)
 
@@ -3558,14 +3523,14 @@ Lemma closed_ereal_le_ereal y : closed [set x | y <= x].
 Proof.
 rewrite (_ : [set x | y <= x] = ~` [set x | y > x]); last first.
   by rewrite predeqE=> x; split=> [rx|/negP]; [apply/negP|]; rewrite -leNgt.
-exact/closedC/open_ereal_lt_ereal.
+exact/open_closedC/open_ereal_lt_ereal.
 Qed.
 
 Lemma closed_ereal_ge_ereal y : closed [set x | y >= x].
 Proof.
 rewrite (_ : [set x | y >= x] = ~` [set x | y < x]); last first.
   by rewrite predeqE=> x; split=> [rx|/negP]; [apply/negP|]; rewrite -leNgt.
-exact/closedC/open_ereal_gt_ereal.
+exact/open_closedC/open_ereal_gt_ereal.
 Qed.
 
 End open_closed_sets_ereal.