fixes #1968 (finI_from)

CHANGELOG_UNRELEASED.md

@@ -459,6 +459,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.
 
@@ -1520,41 +1520,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.
@@ -1573,21 +1574,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

@@ -525,9 +525,6 @@ Qed.
 
 End DLetDLet.
 
-#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
-Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).
-
 (* -------------------------------------------------------------------- *)
 Section DLetAlg.
 Context {T U : choiceType} (mu mu1 mu2 : {distr T / R}).
@@ -744,6 +741,8 @@ End Std.
 Notation __deprecated__dmargin_dlet := dmargin_dlet (only parsing).
 #[deprecated(since="1.17.0", note="use `dlet_dmargin` instead")]
 Notation __deprecated__dlet_dmargin := dlet_dmargin (only parsing).
+#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
+Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).
 
 Notation dfst mu := (dmargin fst mu).
 Notation dsnd mu := (dmargin snd mu).
@@ -966,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

@@ -1285,7 +1285,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/measure_theory/measurable_structure.v

@@ -1319,6 +1319,9 @@ HB.instance Definition _ := @isMeasurable.Build (sigma_display G)
 
 End g_salgebra_instance.
 
+HB.instance Definition _ {T : pointedType} (G : set_system T) :=
+  Pointed.on (g_sigma_algebraType G).
+
 Notation "G .-sigma" := (sigma_display G) : measure_display_scope.
 Notation "G .-sigma.-measurable" :=
   (measurable : set_system (g_sigma_algebraType G)) : classical_set_scope.
@@ -1592,7 +1595,7 @@ Definition measure_prod_display :
 Proof. exact. Qed.
 
 Section product_salgebra_instance.
-Context d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2).
+Context {d1} {d2} {T1 : semiRingOfSetsType d1} {T2 : semiRingOfSetsType d2}.
 Let f1 := @fst T1 T2.
 Let f2 := @snd T1 T2.
 
@@ -1621,7 +1624,12 @@ Notation "p .-prod.-measurable" :=
   ((p.-prod).-measurable : set_system (_ * _)) :
     classical_set_scope.
 
-Lemma measurableX d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2)
+HB.instance Definition _
+    d d' (X : pmeasurableType d) (Y : pmeasurableType d') :=
+  Measurable.on (X * Y)%type.
+
+Lemma measurableX
+    d1 d2 (T1 : semiRingOfSetsType d1) (T2 : semiRingOfSetsType d2)
     (A : set T1) (B : set T2) :
   measurable A -> measurable B -> measurable (A `*` B).
 Proof.

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.