From 2c646b8462f09b6802be8aaef56d9cbd0d57e5ba Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 15 Dec 2025 09:22:58 +0900 Subject: [PATCH 1/5] bolzano-weierstrass --- CHANGELOG_UNRELEASED.md | 7 ++++ classical/cardinality.v | 16 +++++++++ classical/functions.v | 2 +- theories/sequences.v | 75 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 99 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e5df5f1a1..c1962d138 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -103,6 +103,13 @@ - 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 `lebesgue_integrable.v`: + lemma `integrable_norm` diff --git a/classical/cardinality.v b/classical/cardinality.v index 7afaef4ee..fbc6d9ef8 100644 --- a/classical/cardinality.v +++ b/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. diff --git a/classical/functions.v b/classical/functions.v index 9f5b894c3..e76c09907 100644 --- a/classical/functions.v +++ b/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. diff --git a/theories/sequences.v b/theories/sequences.v index 43619f4f6..683ba93ed 100644 --- a/theories/sequences.v +++ b/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). From 849d3040a713232a1368f9948d94f75c2b77a87b Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 26 Dec 2025 14:14:31 +0100 Subject: [PATCH 2/5] splitting in more elementary pieces + proof simplifications --- classical/cardinality.v | 8 ++++ classical/classical_sets.v | 9 ++++ theories/sequences.v | 92 ++++++++++++++++---------------------- 3 files changed, 55 insertions(+), 54 deletions(-) diff --git a/classical/cardinality.v b/classical/cardinality.v index fbc6d9ef8..1940672b6 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -531,6 +531,9 @@ 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 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. @@ -565,6 +568,7 @@ Qed. Lemma finite_set_countable T (A : set T) : finite_set A -> countable A. Proof. by move=> /finite_setP[n /eq_countable->]. Qed. + Lemma infiniteP T (A : set T) : infinite_set A <-> [set: nat] #<= A. Proof. elim/Ppointed: T => T in A *. @@ -1041,6 +1045,10 @@ have : finite_set ((A `&` ~` B) `|` B) by rewrite finite_setU. by rewrite setUIl setUCl setIT finite_setU => -[]. Qed. +Lemma infinite_setI {T} (A B : set T) : + infinite_set A -> finite_set (~` B) -> infinite_set (A `&` B). +Proof. by move=> /infinite_setD/[apply]; rewrite setDE setCK. Qed. + Lemma infinite_set_fset {T : choiceType} (A : set T) n : infinite_set A -> exists2 B : {fset T}, [set` B] `<=` A & (#|` B| >= n)%N. diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 920e838c2..bb1f91d6d 100644 --- a/classical/classical_sets.v +++ b/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]. diff --git a/theories/sequences.v b/theories/sequences.v index 683ba93ed..b29fe7a53 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2973,63 +2973,47 @@ 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_) -> +Lemma finite_range_cst {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, [/\ 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, [/\ increasing_seq f, forall n : nat, (x0 < f n)%O & forall n, A (f n)]. +Proof. +move=> Dfin Aoo; apply: infinite_increasing_seq => x; apply: infinite_setI => //. +by apply: sub_finite_set (Dfin x) => y /=; case: leP. +Qed. + +Lemma finite_range_cvg {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[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. +move=> /finite_range_cst[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. From 0e5a5c100253f54b24a366ff0be09a5d2d4a6741 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 26 Dec 2025 19:47:32 +0100 Subject: [PATCH 3/5] split and rename injectiveT_ltn --- classical/cardinality.v | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/classical/cardinality.v b/classical/cardinality.v index 1940672b6..858b2169c 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -412,21 +412,6 @@ 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). @@ -568,7 +553,6 @@ Qed. Lemma finite_set_countable T (A : set T) : finite_set A -> countable A. Proof. by move=> /finite_setP[n /eq_countable->]. Qed. - Lemma infiniteP T (A : set T) : infinite_set A <-> [set: nat] #<= A. Proof. elim/Ppointed: T => T in A *. @@ -875,6 +859,10 @@ have Gy : y \in G k by rewrite in_fset_set ?inE//; apply: Ffin. by exists (Tagged G [` Gy]%fset). Qed. +Lemma infinite_setC {T} (A : set T) : infinite_set [set: T] -> + finite_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)| = @@ -1143,6 +1131,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: infinite_setC; 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]. From 1168ef4d21300bc26375c1a76c132f409788c372 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 26 Dec 2025 20:07:36 +0100 Subject: [PATCH 4/5] small clean up using cofinite sets --- classical/cardinality.v | 42 ++++++++++++++++++++++++++++++++++++----- theories/sequences.v | 2 +- 2 files changed, 38 insertions(+), 6 deletions(-) diff --git a/classical/cardinality.v b/classical/cardinality.v index 858b2169c..b41639db6 100644 --- a/classical/cardinality.v +++ b/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. @@ -516,6 +518,10 @@ 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. @@ -606,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 A. +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. @@ -661,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. @@ -669,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. @@ -859,8 +887,8 @@ have Gy : y \in G k by rewrite in_fset_set ?inE//; apply: Ffin. by exists (Tagged G [` Gy]%fset). Qed. -Lemma infinite_setC {T} (A : set T) : infinite_set [set: T] -> - finite_set (~` A) -> infinite_set A. +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 : @@ -1033,10 +1061,14 @@ have : finite_set ((A `&` ~` B) `|` B) by rewrite finite_setU. by rewrite setUIl setUCl setIT finite_setU => -[]. Qed. -Lemma infinite_setI {T} (A B : set T) : - infinite_set A -> finite_set (~` B) -> infinite_set (A `&` B). +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. @@ -1134,7 +1166,7 @@ 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: infinite_setC; first exact: infinite_nat. +apply: infinite_setN0; apply: cofinite_set_infinite; first exact: infinite_nat. by rewrite setCK; apply: finite_preimage; first by move=> ? ? ? ?; apply: fI. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index b29fe7a53..466a53cef 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -3000,7 +3000,7 @@ 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, [/\ increasing_seq f, forall n : nat, (x0 < f n)%O & forall n, A (f n)]. Proof. -move=> Dfin Aoo; apply: infinite_increasing_seq => x; apply: infinite_setI => //. +move=> Dfin Aoo; apply: infinite_increasing_seq => x; apply: infinite_setIl => //. by apply: sub_finite_set (Dfin x) => y /=; case: leP. Qed. From 4488e2355b46d17b4528075287881fc4f1e0fd0a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 31 Dec 2025 19:50:55 +0900 Subject: [PATCH 5/5] changelog, fix sub_cofinite_set, renamings --- CHANGELOG_UNRELEASED.md | 18 ++++++++++++++---- classical/cardinality.v | 2 +- theories/sequences.v | 17 ++++++++++------- 3 files changed, 25 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c1962d138..cdcfd65cd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -103,12 +103,22 @@ - in `lebesgue_integrable.v`: + lemma `integrable_set0` -- in `functions.v`: - + lemma `injectiveT_ltn` + +- 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` - + lemma `finite_range_cvg` + + 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`: diff --git a/classical/cardinality.v b/classical/cardinality.v index b41639db6..078276a22 100644 --- a/classical/cardinality.v +++ b/classical/cardinality.v @@ -613,7 +613,7 @@ Lemma sub_finite_set T (A B : set T) : A `<=` B -> 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 A. + 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 -> diff --git a/theories/sequences.v b/theories/sequences.v index 466a53cef..703056d04 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2974,7 +2974,7 @@ End adjacent_cut. Section finite_range_sequence_constant. -Lemma finite_range_cst {T} (u_ : T^nat) : finite_set (range u_) -> +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]. @@ -2987,7 +2987,8 @@ 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, [/\ increasing_seq f, forall n : nat, (x0 < f n)%O & forall n, A (f n)]. + 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. @@ -2998,17 +2999,19 @@ 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, [/\ increasing_seq f, forall n : nat, (x0 < f n)%O & forall n, A (f n)]. + 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 => //. +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 {T : ptopologicalType} (x_ : T ^nat) : +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[x [A Aoo Ax_]]. +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. @@ -3024,7 +3027,7 @@ 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 [/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.