Bolzano weierstrass (#1787)

* bolzano-weierstrass

---------

Co-authored-by: Cyril Cohen <cohen@crans.org>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -104,6 +104,23 @@
 - in `lebesgue_integrable.v`:
   + lemma `integrable_set0`
 
+- in `classical_sets.v`:
+  + lemmas `setUDl`, `setUDr`
+
+- in `cardinality.v`:
+  + notation `cofinite_set`
+  + lemmas `cofinite_setT`, `infinite_setN0`, `sub_cofinite_set`,
+    `sub_infinite_set`, `cofinite_setUl`, `cofinite_setUr`, `cofinite_setU`,
+    `cofinite_setI`, `cofinite_set_infinite`, `infinite_setIl`,
+    `infinite_setIr`
+  + lemma `injective_gtn`
+
+- in `sequences.v`:
+  + lemma `finite_range_cst_subsequence`
+  + lemmas `infinite_increasing_seq`, `infinite_increasing_seq_wf`
+  + lemma `finite_range_cvg_subsequence`
+  + theorem `bolzano_weierstrass`
+
 - in `lebesgue_integrable.v`:
   + lemma `integrable_norm`
 - in `order_topology.v`:

classical/cardinality.v

@@ -26,6 +26,7 @@ From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 (*                   <-> exists X : {fset T}, A = [set` X]                    *)
 (*                   <-> ~ ([set: nat] #<= A)                                 *)
 (*    infinite_set A := ~ finite_set A                                        *)
+(*    cofinite_set A := finite_set (~` A)                                     *)
 (*       countable A <-> A is countable                                       *)
 (*                   := A #<= [set: nat]                                      *)
 (*        fset_set A == the finite set corresponding if A : set T is finite,  *)
@@ -68,6 +69,7 @@ Notation "A '#!=' B" := (~~ (card_eq A B)) : card_scope.
 
 Definition finite_set {T} (A : set T) := exists n, A #= `I_n.
 Notation infinite_set A := (~ finite_set A).
+Notation cofinite_set A := (finite_set (~` A)).
 
 Lemma injPex {T U} {A : set T} :
    $|{inj A >-> U}| <-> exists f : T -> U, set_inj A f.
@@ -412,6 +414,7 @@ apply/idP/idP=> [/card_leP[f]|?];
 by have /leq_card := in2TT 'inj_(IIord \o f \o IIord^-1); rewrite !card_ord.
 Qed.
 
+
 Lemma ocard_eqP {T U} {A : set T} {B : set U} :
   reflect $|{bij A >-> some @` B}| (A #= B).
 Proof.
@@ -515,6 +518,13 @@ Lemma finite_set0 T : finite_set (set0 : set T).
 Proof. by apply/finite_setP; exists 0%N; rewrite II0. Qed.
 #[global] Hint Resolve finite_set0 : core.
 
+Lemma cofinite_setT T : cofinite_set [set: T].
+Proof. by rewrite setCT. Qed.
+#[global] Hint Resolve cofinite_setT : core.
+
+Lemma infinite_setN0 {T} (A : set T) : infinite_set A -> A !=set0.
+Proof. by rewrite -set0P; apply: contra_not_neq => ->. Qed.
+
 Lemma finite_seqP {T : eqType} A :
    finite_set A <-> exists s : seq T, A = [set` s].
 Proof.
@@ -602,6 +612,14 @@ Lemma sub_finite_set T (A B : set T) : A `<=` B ->
   finite_set B -> finite_set A.
 Proof. by move=> ?; apply/card_le_finite/subset_card_le. Qed.
 
+Lemma sub_cofinite_set T (A B : set T) : A `<=` B ->
+  cofinite_set A -> cofinite_set B.
+Proof. by move=> /subsetC/sub_finite_set. Qed.
+
+Lemma sub_infinite_set T (A B : set T) : A `<=` B ->
+  infinite_set A -> infinite_set B.
+Proof. by move=> AB; apply/contra_not/sub_finite_set. Qed.
+
 Lemma finite_set_leP T (A : set T) : finite_set A <-> exists n, A #<= `I_n.
 Proof.
 split=> [[n /card_eqPle[]]|[n leAn]]; first by exists n.
@@ -657,6 +675,16 @@ Qed.
 Lemma finite_setD T (A B : set T) : finite_set A -> finite_set (A `\` B).
 Proof. exact/card_le_finite/card_le_setD. Qed.
 
+Lemma cofinite_setUl T (A B : set T) : cofinite_set A -> cofinite_set (A `|` B).
+Proof. by rewrite setCU -setDE; apply: finite_setD. Qed.
+
+Lemma cofinite_setUr T (A B : set T) : cofinite_set B -> cofinite_set (A `|` B).
+Proof. by rewrite setUC; apply: cofinite_setUl. Qed.
+
+Lemma cofinite_setU T (A B : set T) :
+  cofinite_set A \/ cofinite_set B -> cofinite_set (A `|` B).
+Proof. by move=> [/cofinite_setUl|/cofinite_setUr]. Qed.
+
 Lemma finite_setU T (A B : set T) :
   finite_set (A `|` B) = (finite_set A /\ finite_set B).
 Proof.
@@ -665,6 +693,10 @@ pose fP := @finite_fsetP {classic T}; rewrite propeqE; split.
 by case=> /fP[X->]/fP[Y->]; apply/fP; exists (X `|` Y)%fset; rewrite set_fsetU.
 Qed.
 
+Lemma cofinite_setI T (A B : set T) :
+  cofinite_set (A `&` B) = (cofinite_set A /\ cofinite_set B).
+Proof. by rewrite setCI finite_setU. Qed.
+
 Lemma finite_set2 T (x y : T) : finite_set [set x; y].
 Proof. by rewrite !finite_setU; split; apply: finite_set1. Qed.
 #[global] Hint Resolve finite_set2 : core.
@@ -855,6 +887,10 @@ have Gy : y \in G k by rewrite in_fset_set ?inE//; apply: Ffin.
 by exists (Tagged G [` Gy]%fset).
 Qed.
 
+Lemma cofinite_set_infinite {T} (A : set T) : infinite_set [set: T] ->
+  cofinite_set A -> infinite_set A.
+Proof. by move=> + ACfin Afin; apply; rewrite -(setvU A) finite_setU. Qed.
+
 Lemma trivIset_sum_card (T : choiceType) (F : nat -> set T) n :
   (forall n, finite_set (F n)) -> trivIset [set: nat] F ->
   (\sum_(i < n) #|` fset_set (F i)| =
@@ -1025,6 +1061,14 @@ have : finite_set ((A `&` ~` B) `|` B) by rewrite finite_setU.
 by rewrite setUIl setUCl setIT finite_setU => -[].
 Qed.
 
+Lemma infinite_setIl {T} (A B : set T) :
+  infinite_set A -> cofinite_set B -> infinite_set (A `&` B).
+Proof. by move=> /infinite_setD/[apply]; rewrite setDE setCK. Qed.
+
+Lemma infinite_setIr {T} (A B : set T) :
+  cofinite_set A -> infinite_set B -> infinite_set (A `&` B).
+Proof. by rewrite setIC => *; apply: infinite_setIl. Qed.
+
 Lemma infinite_set_fset {T : choiceType} (A : set T) n :
   infinite_set A ->
     exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N.
@@ -1119,6 +1163,13 @@ Proof. by rewrite -setXTT; apply: infinite_setX; exact: infinite_nat. Qed.
 Lemma card_nat2 : [set: nat * nat] #= [set: nat].
 Proof. exact/eq_card_nat/infinite_prod_nat/countableP. Qed.
 
+Lemma injective_gtn (f : nat -> nat) : injective f -> forall (n : nat), exists m, (n < f m)%N.
+Proof.
+move=> fI n; suff [m /negP] : ~` (f @^-1` `I_n.+1) !=set0 by rewrite -ltnNge; exists m.
+apply: infinite_setN0; apply: cofinite_set_infinite; first exact: infinite_nat.
+by rewrite setCK; apply: finite_preimage; first by move=> ? ? ? ?; apply: fI.
+Qed.
+
 HB.instance Definition _ := isPointed.Build rat 0.
 
 Lemma infinite_rat : infinite_set [set: rat].

classical/classical_sets.v

@@ -710,6 +710,15 @@ Qed.
 
 Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.
 
+Lemma setUDl A B C : (A `\` B) `|` C = (A `|` C) `\` (B `\` C).
+Proof.
+apply/seteqP; split => x /=; first tauto.
+by move=> [[a|c]]; rewrite not_andE notE; tauto.
+Qed.
+
+Lemma setUDr A B C : A `|` (B `\` C) = (A `|` B) `\` (C `\` A).
+Proof. by rewrite setUC setUDl setUC. Qed.
+
 Lemma setDUK A B : A `<=` B -> A `|` (B `\` A) = B.
 Proof.
 move=> AB; apply/seteqP; split=> [x [/AB//|[//]]|x Bx].

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.

theories/sequences.v

@@ -2972,6 +2972,68 @@ Qed.
 
 End adjacent_cut.
 
+Section finite_range_sequence_constant.
+
+Lemma finite_range_cst_subsequence {T} (u_ : T^nat) : finite_set (range u_) ->
+  exists x, exists2 A, infinite_set A & (forall k, A k <-> u_ k = x).
+Proof.
+move=> range_u_finite; pose A x := u_ @^-1` [set x].
+suff [x Aoo] : exists x, infinite_set (A x) by exists x, (A x) => // k.
+apply/existsNP => Afin.
+have: finite_set (\bigcup_(x in range u_) A x) by exact: bigcup_finite.
+rewrite -preimage_bigcup bigcup_imset1 image_id preimage_range.
+exact: infinite_nat.
+Qed.
+
+Lemma infinite_increasing_seq {d} {T : porderType d} (A : set T) :
+  (forall x, infinite_set [set y | A y /\ (x < y)%O]) ->
+  forall x0 : T, exists f : nat -> T,
+    [/\ increasing_seq f, forall n : nat, (x0 < f n)%O & forall n, A (f n)].
+Proof.
+pose R (x y : T) := A y /\ (x < y)%O => Roo x0.
+have [x|f [f0 /all_and2[fA fS]]] := @dependent_choice T R _ x0.
+  by have /infinite_setN0/cid := Roo x.
+exists (f \o S); split => //=; first by apply/increasing_seqP => n; apply: fS.
+by elim=> /= [|n IHn]; rewrite (le_lt_trans _ (fS _)) ?f0//= ltW.
+Qed.
+
+Lemma infinite_increasing_seq_wf {d} {T : orderType d} (A : set T) :
+  (forall x : T, finite_set [set y | (y <= x)%O]) -> infinite_set A ->
+  forall x0 : T, exists f : nat -> T,
+  [/\ increasing_seq f, forall n, (x0 < f n)%O & forall n, A (f n)].
+Proof.
+move=> Dfin Aoo; apply: infinite_increasing_seq => x.
+apply: infinite_setIl => //.
+by apply: sub_finite_set (Dfin x) => y /=; case: leP.
+Qed.
+
+Lemma finite_range_cvg_subsequence {T : ptopologicalType} (x_ : T ^nat) :
+  finite_set (range x_) ->
+  exists2 f : nat -> nat, increasing_seq f & cvgn (x_ \o f).
+Proof.
+move=> /finite_range_cst_subsequence[x [A Aoo Ax_]].
+have /= [|f [fincr _ Af]] := infinite_increasing_seq_wf _ Aoo 0.
+  by move=> n; apply: sub_finite_set (finite_II n.+1) => m /=.
+exists f => //=; suff -> : x_ \o f = fun=> x by apply: is_cvg_cst.
+by apply/funext => k /=; rewrite (Ax_ _).1.
+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_subsequence//|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).