fixes #1968 (#2056)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -481,6 +481,18 @@
 - in `functions.v`
   + lemma `scalrfctE` -> `scalerfctE` (deprecating `scalrfctE`)
 
+- in `filter.v`:
+  + definition `finI_from` -> `open_finI_from`
+  + lemma `finI_from_cover` -> `open_finI_from_cover`
+  + lemma `finI_from1` -> `open_finI_from1`
+  + lemma `finI_from_countable` -> `open_finI_from_countable`
+  + lemma `finI_fromI` -> `open_finI_fromI`
+
+- in `topology_structure.v`:
+  + definition `open_from` -> `openU_from`
+  + lemma `closed_bigsetU` -> `bigsetU_closed`
+  + lemma `closed_bigcup` -> `bigcup_closed`
+
 ### Generalized
 
 - in `measurable_structure.v`:

classical/filter.v

@@ -38,7 +38,7 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*                                The HB class is SubNbhs.                    *)
 (*            filterI_iter F n == nth stage of recursively building the       *)
 (*                                filter of finite intersections of F         *)
-(*               finI_from D f == set of \bigcap_(i in E) f i where E is a    *)
+(*          open_finI_from D f == set of \bigcap_(i in E) f i where E is a    *)
 (*                                a finite subset of D                        *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -185,7 +185,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 (* Making sure that [Program] does not automatically introduce *)
-Obligation Tactic := idtac.
+#[global,export] Obligation Tactic := idtac.
 
 Import Order.TTheory GRing.Theory Num.Theory.
 
@@ -1560,41 +1560,42 @@ move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB.
 by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)].
 Qed.
 
-Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) :=
+Definition open_finI_from (I : choiceType) T (D : set I) (f : I -> set T) :=
   [set \bigcap_(i in [set` D']) f i |
     D' in [set A : {fset I} | {subset A <= D}]].
 
-Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) :
-  \bigcup_(A in finI_from D f) A = setT.
+Lemma open_finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) :
+  \bigcup_(A in open_finI_from D f) A = setT.
 Proof.
 rewrite predeqE => t; split=> // _; exists setT => //.
 by exists fset0 => //; rewrite set_fset0 bigcap_set0.
 Qed.
 
-Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i :
-  D i -> finI_from D f (f i).
+Lemma open_finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i :
+  D i -> open_finI_from D f (f i).
 Proof.
 move=> Di; exists [fset i]%fset; first by move=> ?; rewrite !inE => /eqP ->.
 by rewrite bigcap_fset big_seq_fset1.
 Qed.
 
-Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) :
-  countable D -> countable (finI_from D f).
+Lemma open_finI_from_countable (I : pointedType) T (D : set I)
+    (f : I -> set T) :
+  countable D -> countable (open_finI_from D f).
 Proof.
 move=> ?; apply: (card_le_trans (card_image_le _ _)).
 exact: fset_subset_countable.
 Qed.
 
-Lemma finI_fromI {I : choiceType} T D (f : I -> set T) A B :
-  finI_from D f A -> finI_from D f B -> finI_from D f (A `&` B) .
+Lemma open_finI_fromI {I : choiceType} {T} D (f : I -> set T) :
+  setI_closed (open_finI_from D f).
 Proof.
-case=> N ND <- [M MD <-]; exists (N `|` M)%fset.
+move=> A B; case=> N ND <- [M MD <-]; exists (N `|` M)%fset.
   by move=> ?; rewrite inE => /orP[/ND | /MD].
 by rewrite -bigcap_setU set_fsetU.
 Qed.
 
 Lemma filterI_iter_finI {I : choiceType} T D (f : I -> set T) :
-  finI_from D f = \bigcup_n (filterI_iter (f @` D) n).
+  open_finI_from D f = \bigcup_n (filterI_iter (f @` D) n).
 Proof.
 rewrite eqEsubset; split.
   move=> A [N /= + <-]; have /finite_setP[n] := finite_fset N; elim: n N.
@@ -1613,21 +1614,31 @@ move=> A [n _]; elim: n A.
   - by rewrite set_fset0 bigcap_set0.
   - by move=> ?; rewrite !inE => /eqP ->.
   - by rewrite set_fset1 bigcap_set1.
-by move=> n IH A /= [B snB [C snC <-]]; apply: finI_fromI; apply: IH.
+by move=> n IH A /= [B snB [C snC <-]]; apply: open_finI_fromI; exact: IH.
 Qed.
 
 Lemma smallest_filter_finI {I T : choiceType} (D : set I) (f : I -> set T) :
-  filter_from (finI_from D f) id = smallest (@Filter T) (f @` D).
+  filter_from (open_finI_from D f) id = smallest (@Filter T) (f @` D).
 Proof. by rewrite filterI_iter_finI filterI_iterE. Qed.
 
 End filter_supremums.
+#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from)]
+Notation finI_from := open_finI_from (only parsing).
+#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from_cover)]
+Notation finI_from_cover := open_finI_from_cover (only parsing).
+#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from1)]
+Notation finI_from1 := open_finI_from1 (only parsing).
+#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_from_countable)]
+Notation finI_from_countable := open_finI_from_countable (only parsing).
+#[deprecated(since="mathcomp-analysis 1.17.0", use=open_finI_fromI)]
+Notation finI_fromI := open_finI_fromI (only parsing).
 
 Definition finI (I : choiceType) T (D : set I) (f : I -> set T) :=
   forall D' : {fset I}, {subset D' <= D} ->
   \bigcap_(i in [set i | i \in D']) f i !=set0.
 
 Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) :
-  finI D f -> ProperFilter (filter_from (finI_from D f) id).
+  finI D f -> ProperFilter (filter_from (open_finI_from D f) id).
 Proof.
 move=> finIf; apply: (filter_from_proper (filter_from_filter _ _)).
 - by exists setT; exists fset0 => //; rewrite predeqE.

experimental_reals/distr.v

@@ -965,7 +965,7 @@ rewrite interchange_psum /=; last first.
   by apply/eq_psum=> x /=; rewrite mulrCA.
 + have := summable_pr E (dlet f mu); apply/eq_summable.
   by move=> x; rewrite /= dletE psumZ ?ler0n.
-+ by move=> y; apply/summable_condl/summable_mlet.
++ by move=> t; exact/summable_condl/summable_mlet.
 Qed.
 
 Lemma pr_dmargin E f (mu : {distr U / R}) :

theories/lebesgue_measure.v

@@ -1284,7 +1284,7 @@ have [N F5e] : exists N, \sum_(N <= n <oo) \esum_(i in F n) mu (closure (B i)) <
   - by rewrite nneseries_esum// set_mem_set.
 pose K := \bigcup_(i in `I_N) \bigcup_(j in F i) closure (B j).
 have closedK : closed K.
-  apply: closed_bigcup => //= i iN; apply: closed_bigcup => //.
+  apply: bigcup_closed => //= i iN; apply: bigcup_closed => //.
   by move=> j Fij; exact: closed_closure.
 have ZNF5 : Z r%:num `<=`
     \bigcup_(i in ~` `I_N) \bigcup_(j in F i) closure (5%:R *` B j).

theories/topology_theory/compact.v

@@ -324,7 +324,7 @@ Definition closed_fam_of (A : set T) I (D : set I) (f : I -> set T) :=
 End Covers.
 
 Section PCovers.
-Variable T : ptopologicalType.
+Context {T : ptopologicalType}.
 
 Lemma compact_In0 :
   compact = [set A | forall (I : choiceType) (D : set I) (f : I -> set T),
@@ -334,14 +334,15 @@ rewrite predeqE => A; split=> [Aco I D f [g gcl feAg] finIf|Aco F FF FA].
   case: (pselect (exists i, D i)) => [[i Di] | /asboolP]; last first.
     by rewrite asbool_neg => /forallp_asboolPn D0; exists point => ? /D0.
   have [|p [Ap clfinIfp]] := Aco _ (finI_filter finIf).
-    by exists (f i); [apply: finI_from1|rewrite feAg // => ? []].
+    by exists (f i); [exact: open_finI_from1|rewrite feAg // => ? []].
   exists p => j Dj; rewrite feAg //; split=> //; apply: gcl => // B.
-  by apply: clfinIfp; exists (f j); [apply: finI_from1|rewrite feAg // => ? []].
+  apply: clfinIfp.
+  by exists (f j); [exact: open_finI_from1|rewrite feAg // => ? []].
 have finIAclF : finI F (fun B => A `&` closure B).
   apply: (@filter_finI _ F) => B FB.
   by apply: filterI => //; apply: filterS FB; apply: subset_closure.
 have [|p AclFIp] := Aco _ _ _ _ finIAclF.
-  by exists closure=> //; move=> ??; apply: closed_closure.
+  by exists closure=> //; move=> ? ?; exact: closed_closure.
 exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA.
 by have /AclFIp [_] := FB; move=> /(_ _ p_C).
 Qed.

theories/topology_theory/separation_axioms.v

@@ -190,7 +190,7 @@ Lemma accessible_finite_set_closed :
 Proof.
 split => [TT1 A fA|h x y xy].
   rewrite -(fsbig_setU_set1 fA) fsbig_finite//=.
-  by apply: closed_bigsetU => x xA; exact: accessible_closed_set1.
+  by apply: bigsetU_closed => x xA; exact: accessible_closed_set1.
 by exists (~` [set y]); rewrite !inE/=; split;
   [rewrite openC; exact: h|exact/eqP|].
 Qed.

theories/topology_theory/supremum_topology.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order algebra finmap all_classical.
 From mathcomp Require Import topology_structure uniform_structure.
@@ -62,7 +62,7 @@ HB.instance Definition _ (I : Type) (T : pointedType) (f : I -> Topological T) :
 
 Section sup_uniform.
 Local Open Scope relation_scope.
-Variable (T : choiceType) (Ii : Type) (Tc : Ii -> Uniform T).
+Context {T : choiceType} {Ii : Type} (Tc : Ii -> Uniform T).
 
 Let I : choiceType := {classic Ii}.
 Let TS := fun i => Uniform.Pack (Tc i).
@@ -75,7 +75,7 @@ Local Lemma IEnt_pointT (i : I) : ent_of (i, setT).
 Proof. by apply/asboolP; exact: entourageT. Qed.
 
 Definition sup_ent : set_system (T * T) :=
-  filter_from (finI_from [set: IEnt] (fun p => (projT1 p).2)) id.
+  filter_from (open_finI_from [set: IEnt] (fun p => (projT1 p).2)) id.
 
 Ltac IEntP := move=> [[ /= + + /[dup] /asboolP]].
 
@@ -185,8 +185,9 @@ have [I0 | /set0P [i0 _]] := eqVneq [set: I] set0.
   move=> P [w [A _]] <- subP; exists setT => //.
   apply: subset_trans subP; apply: sub_bigcap => i _ ? _.
   by suff : [set: I] (projT1 i).1 by rewrite I0.
-exists (finI_from (\bigcup_n g n) id); split.
-- by apply/finI_from_countable/bigcup_countable => //i _; case: (projT2 (f i)).
+exists (open_finI_from (\bigcup_n g n) id); split.
+- apply/open_finI_from_countable/bigcup_countable => // i _.
+  by case: (projT2 (f i)).
 - move=> E [A AsubGn AE]; exists E => //.
   have h (w : set (T * T)) : { p : IEnt | w \in A -> w = (projT1 p).2 }.
     apply: cid; have [|] := boolP (w \in A); last first.

theories/topology_theory/topology_structure.v

@@ -500,46 +500,48 @@ HB.end.
 (** Topology defined by a base of open sets *)
 
 HB.factory Record isBaseTopological T & Choice T := {
-  I : pointedType;
-  D : set I;
-  b : I -> (set T);
-  b_cover : \bigcup_(i in D) b i = setT;
+  I : pointedType ;
+  D : set I ;
+  b : I -> set T ;
+  b_cover : \bigcup_(i in D) b i = setT ;
   b_join : forall i j t, D i -> D j -> b i t -> b j t ->
-    exists k, [/\ D k, b k t & b k `<=` b i `&` b j];
+    exists k, [/\ D k, b k t & b k `<=` b i `&` b j]
 }.
 
+Definition openU_from T I (D : set I) (b : I -> set T) :=
+  [set \bigcup_(i in D') b i | D' in subset^~ D].
+
 HB.builders Context T & isBaseTopological T.
 
-Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
+Local Notation openU_from := (openU_from D b).
 
-Let open_fromT : open_from setT.
+Let openU_fromT : openU_from setT.
 Proof. exists D => //; exact: b_cover. Qed.
 
-Let open_fromI (A B : set T) : open_from A -> open_from B ->
-  open_from (A `&` B).
+Let openU_fromI : setI_closed openU_from.
 Proof.
-move=> [DA sDAD AeUbA] [DB sDBD BeUbB].
-have ABU : forall t, (A `&` B) t ->
-  exists it, D it /\ b it t /\ b it `<=` A `&` B.
-  move=> t [At Bt].
-  have [iA [DiA [biAt sbiA]]] : exists i, D i /\ b i t /\ b i `<=` A.
+move=> A B [DA sDAD AeUbA] [DB sDBD BeUbB].
+have ABU t : (A `&` B) t ->
+  exists it, [/\ D it, b it t & b it `<=` A `&` B].
+  move=> [At Bt].
+  have [iA [DiA biAt sbiA]] : exists i, [/\ D i, b i t & b i `<=` A].
     move: At; rewrite -AeUbA => - [i DAi bit]; exists i.
-    by split; [apply: sDAD|split=> // ?; exists i].
-  have [iB [DiB [biBt sbiB]]] : exists i, D i /\ b i t /\ b i `<=` B.
+    by split => //; [exact: sDAD|exact: bigcup_sup].
+  have [iB [DiB biBt sbiB]] : exists i, [/\ D i, b i t & b i `<=` B].
     move: Bt; rewrite -BeUbB => - [i DBi bit]; exists i.
-    by split; [apply: sDBD|split=> // ?; exists i].
+    by split=> //; [exact: sDBD|exact: bigcup_sup].
   have [i [Di bit sbiAB]] := b_join DiA DiB biAt biBt.
-  by exists i; split=> //; split=> // s /sbiAB [/sbiA ? /sbiB].
-set Dt := fun t => [set it | D it /\ b it t /\ b it `<=` A `&` B].
+  by exists i; split=> // s /sbiAB [/sbiA ? /sbiB].
+set Dt := fun t => [set it | [/\ D it, b it t & b it `<=` A `&` B]].
 exists [set get (Dt t) | t in A `&` B].
   by move=> _ [t ABt <-]; have /ABU/getPex [] := ABt.
 rewrite predeqE => t; split=> [[_ [s ABs <-] bDtst]|ABt].
-  by have /ABU/getPex [_ [_]] := ABs; apply.
-by exists (get (Dt t)); [exists t| have /ABU/getPex [? []]:= ABt].
+  by have /ABU/getPex [_ _] := ABs; exact.
+by exists (get (Dt t)); [exists t| have /ABU/getPex [?]:= ABt].
 Qed.
 
-Let open_from_bigU (I0 : Type) (f : I0 -> set T) :
-  (forall i, open_from (f i)) -> open_from (\bigcup_i f i).
+Let openU_from_bigU (I0 : Type) (f : I0 -> set T) :
+  (forall i, openU_from (f i)) -> openU_from (\bigcup_i f i).
 Proof.
 set fop := fun j => [set Dj | Dj `<=` D /\ f j = \bigcup_(i in Dj) b i].
 exists (\bigcup_j get (fop j)).
@@ -554,19 +556,22 @@ by move=> [i]; exists i => //; exists j.
 Qed.
 
 HB.instance Definition _ := isOpenTopological.Build T
-  open_fromT open_fromI open_from_bigU.
+  openU_fromT openU_fromI openU_from_bigU.
 
 HB.end.
 
+#[deprecated(since="mathcomp-analysis 1.17.0", use=openU_from)]
+Notation open_from := openU_from (only parsing).
+
 HB.factory Record isSubBaseTopological T & Choice T := {
-  I : pointedType;
-  D : set I;
-  b : I -> (set T);
+  I : pointedType ;
+  D : set I ;
+  b : I -> set T
 }.
 
 HB.builders Context T & isSubBaseTopological T.
 
-Local Notation finI_from := (finI_from D b).
+Local Notation finI_from := (open_finI_from D b).
 
 Let finI_from_cover : \bigcup_(A in finI_from) A = setT.
 Proof.
@@ -829,25 +834,29 @@ Qed.
 Lemma closedU (T : topologicalType) : setU_closed (@closed T).
 Proof. by move=> E D; rewrite -?openC setCU; exact: openI. Qed.
 
-Lemma closed_bigsetU (T : topologicalType) (I : eqType) (s : seq I)
+Lemma bigsetU_closed {T : topologicalType} {I : eqType} (s : seq I)
     (F : I -> set T) : (forall x, x \in s -> closed (F x)) ->
   closed (\big[setU/set0]_(x <- s) F x).
 Proof.
 move=> scF; rewrite big_seq.
 by elim/big_ind : _ => //; [exact: closed0|exact: closedU].
 Qed.
+#[deprecated(since="mathcomp-analysis 1.17.0", use=bigsetU_closed)]
+Notation closed_bigsetU := bigsetU_closed (only parsing).
 
-Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I)
+Lemma bigcup_closed {T : topologicalType} {I : choiceType} (A : set I)
     (F : I -> set T) :
     finite_set A -> (forall i, A i -> closed (F i)) ->
   closed (\bigcup_(i in A) F i).
 Proof.
-move=> finA cF; rewrite -bigsetU_fset_set//; apply: closed_bigsetU => i.
+move=> finA cF; rewrite -bigsetU_fset_set//; apply: bigsetU_closed => i.
 by rewrite in_fset_set// inE; exact: cF.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.17.0", use=bigcup_closed)]
+Notation closed_bigcup := bigcup_closed (only parsing).
 
 Section closure_lemmas.
-Variable T : topologicalType.
+Context {T : topologicalType}.
 Implicit Types E A B U : set T.
 
 Lemma closureS A B : A `<=` B -> closure A `<=` closure B.