Heine cantor

CHANGELOG_UNRELEASED.md

@@ -103,6 +103,22 @@
 
 - in `lebesgue_integrable.v`:
   + lemma `integrable_set0`
+- in `functions.v`:
+  + lemma `injectiveT_ltn`
+
+- in `sequences.v`:
+  + lemma `finite_range_cst`
+  + lemma `finite_range_cvg`
+  + theorem `bolzano_weierstrass`
+
+- in `subspace_topology.v`:
+  + lemmas `unif_continuous_set0`, `unif_continuous_set1`
+
+- in `normed_module.v`:
+  + lemma `itv_bounded_fun`
+
+- in `realfun.v`:
+  + lemma `within_continuous_unif`
 
 ### Changed
 

classical/cardinality.v

@@ -412,6 +412,22 @@ apply/idP/idP=> [/card_leP[f]|?];
 by have /leq_card := in2TT 'inj_(IIord \o f \o IIord^-1); rewrite !card_ord.
 Qed.
 
+Lemma injectiveT_ltn (A : set nat) (f : {injfun [set: nat] >-> A}) (n : nat) :
+  exists m, (n < f m)%N.
+Proof.
+elim: n => [|n [m ih]].
+  apply/not_existsP => f_le0.
+  have /(_ 0 1 (in_setT _) (in_setT _)) : set_inj setT f by [].
+  have /negP := f_le0 0; rewrite -leqNgt leqn0 => /eqP ->.
+  have /negP := f_le0 1; rewrite -leqNgt leqn0 => /eqP ->.
+  by move=> /(_ erefl)/esym; exact/eqP/oner_neq0.
+apply/not_existsP => f_leS.
+have {}f_leS x : (f x <= n.+1)%N by rewrite leqNgt; exact/negP/f_leS.
+have /subset_card_le : f @` `I_n.+3 `<=` `I_n.+2.
+  by move=> /= _ [y] yn3 <-; rewrite ltnS f_leS.
+by rewrite (card_ge_image f)// card_le_II ltnn.
+Qed.
+
 Lemma ocard_eqP {T U} {A : set T} {B : set U} :
   reflect $|{bij A >-> some @` B}| (A #= B).
 Proof.

classical/functions.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.

classical/unstable.v

@@ -35,6 +35,12 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
+Lemma split3r (F : numFieldType) (x : F) : x = x / 3 + x / 3 + x / 3.
+Proof.
+rewrite -!mulrDl -[in RHS](mulr1 x) -!mulrDr [in X in X / _](_ : 1 = 1%:R)//.
+by rewrite !natr1 -mulrA divff ?mulr1// pnatr_eq0.
+Qed.
+
 Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I)
     (l : seq I) :
   all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] ->

theories/normedtype_theory/normed_module.v

@@ -1558,6 +1558,50 @@ Qed.
 
 End Rhull.
 
+Lemma itv_bounded_fun {R : realFieldType} (u_ : nat -> R) b0 b1 x y :
+  (forall n, u_ n \in Interval (BSide b0 x) (BSide b1 y)) ->
+  bounded_fun u_.
+Proof.
+have [yx|] := ltP x y; last first.
+  rewrite le_eqVlt => /predU1P[->{y} yx|yx]; last first.
+    move/(_ 0); rewrite in_itv/=.
+    move: b0 b1 => [] [] /= /andP[xu uy].
+    - by have := le_lt_trans xu uy; rewrite ltNge (ltW yx).
+    - by have := le_trans xu uy; rewrite leNgt yx.
+    - by have := lt_trans xu uy; rewrite ltNge (ltW yx).
+    - by have := lt_le_trans xu uy; rewrite ltNge (ltW yx).
+    move: b0 b1 yx => [] [] /= yx.
+    - have := yx 0; rewrite in_itv/= => /andP[/le_lt_trans/[apply]].
+      by rewrite ltxx.
+    - have {yx}-> : u_ = cst x.
+        apply/funext => n.
+        have := yx n.
+        by rewrite in_itv/= -eq_le => /eqP.
+      exact: bounded_cst.
+    - have := yx 0; rewrite in_itv/= => /andP[/lt_trans/[apply]].
+      by rewrite ltxx.
+    - have := yx 0; rewrite in_itv/= => /andP[/lt_le_trans/[apply]].
+      by rewrite ltxx.
+move=> uab.
+rewrite /bounded_fun /bounded_near.
+near=> M => n _ /=.
+rewrite (@le_trans _ _ (Num.max `|x| `|y|))//.
+move: uab => /(_ n); rewrite in_itv/= => /andP[xu uy].
+rewrite le_max.
+have /orP[x0|x0] := le_total 0 (u_ n).
+- rewrite (ger0_norm x0); apply/orP; right.
+  case: b1 in uy *.
+  + by rewrite (le_trans (ltW uy))// ler_norm.
+  + by rewrite (le_trans uy)// ler_norm.
+- rewrite (ler0_norm x0); apply/orP; left.
+  have a0 : x <= 0.
+  + case: b0 in xu *.
+    * by rewrite (le_trans xu).
+    * by rewrite (le_trans (ltW xu)).
+  + rewrite ler0_norm// lerN2.
+  by case: b0 xu => //= /ltW.
+Unshelve. all: by end_near. Qed.
+
 (**md properties of segments in $\bar{R}$ *)
 Section segment.
 Context {R : realType}.

theories/realfun.v

@@ -268,6 +268,168 @@ Unshelve. all: end_near. Qed.
 
 End cvgr_fun_cvg_seq.
 
+Section heine_cantorR.
+Context {R : realType}.
+
+Let within_continuous_unif_contra a b (f : R -> R) : a < b ->
+  {within `[a, b], continuous f} ->
+  ~ @unif_continuous (subspace `[a, b]) R f ->
+  exists2 e : R, e > 0 &
+    forall d : R, d > 0 -> exists x : R * R, [/\ x.1 \in `]a, b[,
+      x.2 \in `]a, b[, `|x.1 - x.2| < d & `|f x.1 - f x.2| >= e].
+Proof.
+move=> ab /continuous_within_itvP => /(_ ab)[cf fa fb].
+move/unif_continuousP => /= /existsNP[e /not_implyP[e0 /forall2NP ucf]].
+exists (e / 3); [by rewrite divr_gt0|move=> d d0].
+have [//|{ucf}] := ucf d.
+move/existsNP => -[[x y] /= /not_implyP][xdy efxfy].
+wlog xy : x y xdy efxfy / x < y.
+  move=> wlg; have [xy|xy|xy]:= ltgtP x y.
+  - exact: (wlg x y).
+  - by apply: (wlg y x) => //; [exact/ball_sym|move/ball_sym].
+  - by move: efxfy; rewrite -xy /ball/= subrr normr0 e0.
+have [|xab] := boolP (x \in `[a, b]%classic); last first.
+  move: xdy; rewrite /ball/= /subspace_ball (negPf xab) /= => yx.
+  by move: efxfy; rewrite yx /ball/= subrr normr0 e0.
+rewrite inE/= in_itv/= => /andP[ax xb].
+have [|yab] := boolP (y \in `[a, b]%classic); last first.
+  move: xdy; rewrite /ball/= /subspace_ball mem_setE in_itv/= ax xb/=.
+  by move: yab; rewrite mem_setE/= => /negbTE -> [].
+rewrite inE/= in_itv/= => /andP[ay yb].
+move: ax; rewrite le_eqVlt => /predU1P[xa|xa].
+- move: xy xdy efxfy; rewrite -{}xa => {}ay ady efafy {xb x}.
+  have [r [s [ar rs sy ers]]] : exists r, exists s,
+      [/\ a < r, r < s, s < y & e / 3 <= `|f r - f s| ].
+    near a^'+ => a0; exists a0.
+    near y^'- => y0; exists y0; split => //.
+    move/negP: efafy; rewrite -leNgt [in X in X -> _](split3r e) -addrA.
+    rewrite -lerBrDr => /le_trans; apply; rewrite lerBlDl.
+    rewrite -(subrKA (f a0)) (le_trans (ler_normD _ _))// -addrA lerD//.
+      near: a0.
+      by move/cvgrPdist_le : fa => /(_ (e / 3) ltac:(by rewrite divr_gt0)).
+    rewrite distrC -(subrKA (f y0)) (le_trans (ler_normD _ _))// lerD//.
+      near: y0.
+      move: yb; rewrite le_eqVlt => /predU1P[->|yb].
+        by move/cvgrPdist_le : fb => /(_ (e / 3) ltac:(by rewrite divr_gt0)).
+      have : f x @[x --> (y : R)] --> f y by apply: cf; rewrite in_itv/= ay.
+      move/left_right_continuousP => -[fy _].
+      by move/cvgrPdist_le : fy => /(_ (e / 3) ltac:(by rewrite divr_gt0)).
+    by rewrite distrC.
+  exists (r, s); split => //=.
+  + by rewrite in_itv/= ar/= (lt_trans rs)// (lt_le_trans sy).
+  + by rewrite !in_itv/= (lt_trans ar)// (lt_le_trans sy).
+  + move: ady; rewrite /ball/= /subspace_ball/= mem_setE in_itv/=.
+    rewrite lexx (ltW ab)/= => -[_]; apply: le_lt_trans.
+    do 2 rewrite ltr0_norm ?subr_lt0// opprB.
+    by rewrite (lerB (ltW sy))// ltW.
+- have {}ay : a < y by rewrite (lt_trans xa).
+  have {}xb : x < b by rewrite (lt_le_trans xy).
+  move: yb; rewrite le_eqVlt => /predU1P[{}yb|{}yb].
+  + move: xdy efxfy xy; rewrite {}yb => xdb efxfb {}xb {y ay}.
+    have {}yab : x \in `]a, b[ by rewrite in_itv/= xa xb.
+    near b^'- => b0.
+    exists (x, b0); split => //=.
+    * by rewrite in_itv/=; apply/andP; split.
+    * move: xdb.
+      rewrite /ball/= /subspace_ball/= mem_setE in_itv/= (ltW xa) (ltW xb)/=.
+      move=> -[_]; apply: le_lt_trans.
+      do 2 rewrite ltr0_norm ?subr_lt0//.
+      by rewrite lerN2 lerD2l lerN2.
+    * move: efxfb => /negP; rewrite -leNgt.
+      rewrite [in X in X -> _](split3r e) -addrA -lerBrDr => /le_trans; apply.
+      rewrite lerBlDl -{1}(subrKA (f b0)) (le_trans (ler_normD _ _))//.
+      rewrite addrC lerD2r -mulr2n -mulr_natl distrC.
+      near: b0.
+      move/cvgrPdist_le : fb => /(_ (2 * (e / 3)) ltac:(rewrite !mulr_gt0)).
+      exact.
+  + exists (x, y); split => /=.
+    * by rewrite in_itv/= xa xb.
+    * by rewrite in_itv/= ay yb.
+    * move: xdy; rewrite /ball/= /subspace_ball/=.
+      by rewrite mem_setE/= in_itv/= (ltW xa) (ltW xb)/= => -[].
+    * move: efxfy => /negP; rewrite -leNgt; apply: le_trans.
+      by rewrite ler_piMr ?invf_le1 ?ler1n// ltW.
+Unshelve. all: by end_near. Qed.
+
+Lemma within_continuous_unif a b (f : R -> R) :
+  {within `[a, b], continuous f} -> @unif_continuous (subspace `[a, b]) R f.
+Proof.
+have [ab|] := ltP a b; last first.
+  rewrite le_eqVlt => /predU1P[-> _|ba _].
+    by rewrite set_itv1; exact: unif_continuous_set1.
+  by rewrite set_itv_ge ?bnd_simp -?ltNge//; exact: unif_continuous_set0.
+move=> cf; apply: contrapT => ucf.
+have [e e0 de] := within_continuous_unif_contra ab cf ucf.
+move: cf => /continuous_within_itvP => /(_ ab)[cf fa fb].
+rewrite {ucf}.
+have n0 n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0.
+pose u_ n := (sval (cid (de _ (n0 n)))).1.
+pose v_ n := (sval (cid (de _ (n0 n)))).2.
+have u_ab n : u_ n \in `]a, b[ by have [] := svalP (cid (de n.+1%:R^-1 (n0 n))).
+have v_ab n : v_ n \in `]a, b[ by have [] := svalP (cid (de n.+1%:R^-1 (n0 n))).
+have u_v n : `|u_ n - v_ n| < n.+1%:R^-1.
+  by have [] := svalP (cid (de n.+1%:R^-1 (n0 n))).
+have /bolzano_weierstrass[g incrg /cvg_ex[/= l u_gl]] : bounded_fun u_.
+  apply: (@itv_bounded_fun _ _ false true a b) => n.
+  by rewrite /u_/=; case: cid => // -[x y] /= [].
+have lab : `[a, b]%classic l.
+  apply: (closed_cvg _ _ _ _ u_gl); first exact: itv_closed.
+  by apply/nearW => n /=; apply: subset_itv_oo_cc; exact: u_ab.
+have v_gl : v_ \o g @ \oo --> l.
+  apply/cvgrPdist_le => /= r r0.
+  have r20 : 0 < r / 2 by rewrite divr_gt0.
+  have {}invrg n : (n <= (g n).+1)%N.
+    elim: n => // n ih; rewrite (leq_ltn_trans ih)// ltnS.
+    by move/increasing_seqP : incrg; exact.
+  near=> n.
+  rewrite -(subrKA (u_ (g n))) (splitr r) (le_trans (ler_normD _ _))// lerD//.
+    by near: n; move/cvgrPdist_le : u_gl; exact.
+  rewrite ltW// (@lt_trans _ _ (g n).+1%:R^-1)// invf_plt ?posrE//.
+  rewrite (@lt_le_trans _ _ n%:R) ?ler_nat//.
+  by near: n; exact: nbhs_infty_gtr.
+have e20 : 0 < e / 2 by rewrite divr_gt0.
+have efufv n : e <= `|f (u_ n) - f (v_ n)|.
+  by have [] := svalP (cid (de n.+1%:R^-1 (n0 n))).
+have [la {lab} | lb {lab} | {}lab] : [\/ l = a, l = b | `]a, b[%classic l].
+  move: lab; rewrite -(@setU1itv _ _ _ a) ?bnd_simp; last exact/ltW.
+  by rewrite -(@setUitv1 _ _ _ b) ?bnd_simp// /setU/= (orC _ (l = b)) or3E.
+- rewrite {}la {l} in u_gl v_gl *.
+  have /cvgrPdist_lt /(_ _ e20) fu_a : (f \o u_ \o g) @ \oo --> f a.
+    move/cvg_at_rightP : fa; apply; split => // n.
+    by move/itvP : (u_ab (g n)) => ->.
+  have /cvgrPdist_lt /(_ _ e20) fv_a : (f \o v_ \o g) @ \oo --> f a.
+    move/cvg_at_rightP : fa; apply; split => // n.
+    by move/itvP : (v_ab (g n)) => ->.
+  near \oo => n.
+  have := efufv (g n); rewrite leNgt => /negP; apply.
+  rewrite (splitr e) -(subrKA (f a)) (le_lt_trans (ler_normD _ _))// ltrD//.
+    by rewrite distrC; near: n.
+  by near: n.
+- rewrite {}lb {l} in u_gl v_gl *.
+  have /cvgrPdist_lt /(_ _ e20) fu_b : (f \o u_ \o g) @ \oo --> f b.
+    move/cvg_at_leftP : fb; apply; split => // n.
+    by move/itvP : (u_ab (g n)) => ->.
+  have /cvgrPdist_lt /(_ _ e20) fv_b : (f \o v_ \o g) @ \oo --> f b.
+    move/cvg_at_leftP : fb; apply; split => // n.
+    by move/itvP: (v_ab (g n)) => ->.
+  near \oo => n.
+  have := efufv (g n); rewrite leNgt => /negP; apply.
+  rewrite (splitr e) -(subrKA (f b)) (le_lt_trans (ler_normD _ _))// ltrD//.
+    by rewrite distrC; near: n.
+  by near: n.
+- have /cvgrPdist_lt /(_ _ e20) fu_l : (f \o u_ \o g) @ \oo --> f l.
+    exact: (continuous_cvg _ (cf _ _)).
+  have /cvgrPdist_lt /(_ _ e20) fv_l : (f \o v_ \o g) @ \oo --> f l.
+    exact: (continuous_cvg _ (cf _ _)).
+  near \oo => n.
+  have := efufv (g n); rewrite leNgt => /negP; apply.
+  rewrite -(subrKA (f l)) (splitr e) (le_lt_trans (ler_normD _ _))// ltrD//.
+    by rewrite distrC; near: n.
+ by near: n.
+Unshelve. all: by end_near. Qed.
+
+End heine_cantorR.
+
 Section cvge_fun_cvg_seq.
 Context {R : realType}.
 

theories/sequences.v

@@ -2972,6 +2972,81 @@ Qed.
 
 End adjacent_cut.
 
+Section finite_range_sequence_constant.
+Context {R : realFieldType}.
+
+Lemma finite_range_cst (u_ : R^nat) : finite_set (range u_) ->
+  exists N, exists2 A, infinite_set A & (forall k, A k <-> u_ k = u_ N).
+Proof.
+case=> n; elim: n => [|n ih] in u_ *.
+  by rewrite card_eq_sym => /card_set_bijP[/= f [_ _ /(_ _ (imageT u_ 0))[]]].
+move/eq_cardSP => -[r [N _ uNr]] urn.
+apply: assume_not => /forallNP/(_ N) uN.
+have {uN}[B finB BuN] : exists2 B, finite_set B &
+    (forall k, B k <-> u_ k = u_ N).
+  exists (u_ @^-1` [set u_ N]); last by move=> k; split.
+  by apply: contrapT => u_N; apply: uN; eexists; [exact: u_N|by []].
+have [M BM] : exists M, ~ B M.
+  apply/existsNP => allB.
+  move: finB; rewrite (_ : B = setT); first exact/infinite_nat.
+  by rewrite -subTset => x _; exact: allB.
+have uMuN : u_ M != u_ N by apply: contra_not_neq BM; exact: (BuN _).2.
+pose v_ k := if k \in B then u_ M else u_ k.
+have /ih[k [A infA Ak]] : (range v_ #= `I_n)%card.
+  suff : range v_ = (range u_) `\ u_ N by move=> ->; rewrite uNr.
+  apply/seteqP; split=> [_ [y] _ <-|_ [[y _ <-]] uyuN]; rewrite /v_.
+  - case: ifPn => [yB|]; first by split; [exists M|exact/eqP].
+    by rewrite notin_setE => /BuN.
+  - by exists y => //; case: ifPn => // /set_mem /BuN.
+have [Bk|Bk] := pselect (B k).
+- exists M, (A `\` B); [exact: infinite_setD|move=> m; split=> [[+ Bm]|]].
+  + by move/(Ak _).1; rewrite /v_ memNset// mem_set.
+  + apply: contraPP; rewrite -[~ _]/((~` (_ `\` _)) m) setCD => -[|/BuN ->].
+    * have /iff_not2[+ _] := Ak m.
+      by move/[apply]; rewrite /v_; case: ifPn => mB; rewrite mem_set// eqxx.
+    * exact/nesym/eqP.
+- exists k, (A `\` B); [exact: infinite_setD|move=> m].
+  split=> [[+ Bm]|]; first by move/(Ak _).1; rewrite /v_ memNset// memNset.
+  apply: contraPP; rewrite -[~ _]/((~` (_ `\` _)) m) setCD => -[|Bm].
+  + have /iff_not2[+ _] := Ak m.
+    move=> /[apply]; rewrite /v_; case: ifPn => mB; rewrite memNset//.
+    by move: mB Bk => /set_mem /BuN -> /BuN /nesym.
+  + have /iff_not2[+ _] := BuN k.
+    by move=> /(_ Bk); apply: contra_not; rewrite ((BuN m).1 Bm).
+Qed.
+
+Lemma finite_range_cvg (x_ : R ^nat) : finite_set (range x_) ->
+  exists2 f : nat -> nat, increasing_seq f & cvgn (x_ \o f).
+Proof.
+move=> /finite_range_cst[k [A /infiniteP/pcard_leP/unsquash f Ak]].
+have : forall n, {y | (n < y)%N /\ A y}.
+  move=> n; apply/cid.
+  have [m xfm] : exists m, (n < f m)%N by exact: injectiveT_ltn.
+  by exists (f m); split => //; exact: funS.
+move/dependent_choice => /(_ 0)[g [g00 gincr]].
+exists g; first by apply/increasing_seqP => n; exact: (gincr _).1.
+apply/cvg_ex; exists (x_ k); apply/cvgrPdist_le => /= e e0.
+near=> n.
+have := (gincr n.-1).2; rewrite prednK; last by near: n; by exists 1%N.
+by move/(Ak (g n)).1 => ->; rewrite subrr normr0 ltW.
+Unshelve. all: end_near. Qed.
+
+End finite_range_sequence_constant.
+
+Theorem bolzano_weierstrass {R : realType} (u_ : R^nat):
+  bounded_fun u_ -> exists2 f : nat -> nat, increasing_seq f & cvgn (u_ \o f).
+Proof.
+move=> bnd_u; set U := range u_.
+have bndU : bounded_set U.
+  case: bnd_u => N [Nreal Nu_].
+  by exists N; split => // x /Nu_ {}Nu_ /= y [x0 _ <-]; exact: Nu_.
+have [/finite_range_cvg//|infU] := pselect (finite_set U).
+have [/= l Ul] := infinite_bounded_limit_point_nonempty infU bndU.
+have x_l := limit_point_cluster_eventually Ul.
+have [+ _] := cluster_eventually_cvg u_ l.
+by move=> /(_ x_l)[f fi fl]; exists f => //; apply/cvg_ex; exists l.
+Qed.
+
 Section banach_contraction.
 
 Context {R : realType} {X : completeNormedModType R} (U : set X).

theories/topology_theory/subspace_topology.v

@@ -564,6 +564,22 @@ Proof. by []. Qed.
 
 End SubspacePseudoMetric.
 
+Lemma unif_continuous_set0 R (U V : pseudoMetricType R) (f : U -> V) :
+  @unif_continuous (subspace set0) _ f.
+Proof.
+apply/unif_continuousP => /= e e0; exists 1 => // -[x y]/=.
+by rewrite [X in X -> _]/ball/= /subspace_ball/= in_set0 => ->; exact: ballxx.
+Qed.
+
+Lemma unif_continuous_set1 R (U V : pseudoMetricType R) a (f : U -> V) :
+  @unif_continuous (subspace [set a]) _ f.
+Proof.
+apply/unif_continuousP => /= e e0; exists 1 => // -[x y]/=.
+rewrite [X in X -> _]/ball/= /subspace_ball/=; case: ifPn => [|_ ->].
+  by rewrite inE => -> [->] _; exact: ballxx.
+exact: ballxx.
+Qed.
+
 Section SubspaceWeak.
 Context {T : topologicalType} {U : choiceType}.
 Variables (f : U -> T).