fix #1863

CHANGELOG_UNRELEASED.md

@@ -196,6 +196,10 @@
 
 - in `subspace_topology.v`:
   + lemmas `open_subspaceP` and `closed_subspaceP` (use `exists2` instead of `exists`)
+- moved from `filter.v` to `classical_sets.v`:
+  + definition `set_system`
+- moved from `measurable_structure.v` to `classical_sets.v`:
+  + definitions `setI_closed`, `setU_closed`
 
 ### Renamed
 

classical/classical_sets.v

@@ -103,6 +103,17 @@ From mathcomp Require Import mathcomp_extra boolp wochoice.
 (*           \bigcap_(i < n) F := \bigcap_(i in `I_n) F                       *)
 (*          \bigcap_(i >= n) F := \bigcap_(i in [set i | i >= n]) F           *)
 (*                 \bigcap_i F == same as before with T left implicit         *)
+(* ```                                                                        *)
+(*                                                                            *)
+(* ### About sets of sets                                                     *)
+(* ```                                                                        *)
+(*       set_system T := set (set T)                                          *)
+(*      setI_closed G == the set of sets G is closed under finite             *)
+(*                       intersection                                         *)
+(*      setU_closed G == the set of sets G is closed under finite union       *)
+(* ```                                                                        *)
+(*                                                                            *)
+(* ```                                                                        *)
 (*                smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A  *)
 (*                   A `<=` B <-> A is included in B                          *)
 (*                     A `<` B := A `<=` B /\ ~ (B `<=` A)                    *)
@@ -1625,6 +1636,18 @@ by rewrite eqEsubset; split => [x [b [a Aa] <- <-]|x [a Aa] <-];
   [apply/imageP |apply/imageP/imageP].
 Qed.
 
+Definition set_system U := set (set U).
+Identity Coercion set_system_to_set : set_system >-> set.
+
+Section set_systems.
+Context {T} (G : set_system T).
+
+Definition setI_closed := forall A B, G A -> G B -> G (A `&` B).
+
+Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
+
+End set_systems.
+
 Lemma subKimage {T T'} {P : set (set T')} (f : T -> T') (g : T' -> T) :
   cancel f g -> [set A | P (f @` A)] `<=` [set g @` A | A in P].
 Proof. by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.

classical/filter.v

@@ -214,9 +214,6 @@ Reserved Notation "E `@[ x --> F ]"
   (at level 60, x name, format "E  `@[ x  -->  F ]").
 Reserved Notation "f `@ F" (at level 60, format "f  `@  F").
 
-Definition set_system U := set (set U).
-Identity Coercion set_system_to_set : set_system >-> set.
-
 HB.mixin Record isFiltered U T := {
   nbhs : T -> set_system U
 }.
@@ -431,7 +428,7 @@ Qed.
 
 Class Filter {T : Type} (F : set_system T) := {
   filterT : F setT ;
-  filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ;
+  filterI : setI_closed F ;
   filterS : forall P Q : set T, P `<=` Q -> F P -> F Q
 }.
 Global Hint Mode Filter - ! : typeclass_instances.
@@ -1179,7 +1176,7 @@ Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
 - by apply: filterE.
-- by move=> P Q; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ].
+- by move=> P Q/=; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ].
 - by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ.
 Qed.
 
@@ -1203,7 +1200,7 @@ Global Instance subset_filter_filter T F (D : set T) :
 Proof.
 move=> FF; constructor; rewrite /subset_filter/=.
 - exact: filterE.
-- by move=> P Q; apply: filterS2=> x PD QD Dx; split.
+- by move=> P Q/=; exact: filterS2.
 - by move=> P Q subPQ; apply: filterS => R PD Dx; apply: subPQ.
 Qed.
 #[global] Typeclasses Opaque subset_filter.

theories/measure_theory/measurable_structure.v

@@ -62,9 +62,6 @@ From mathcomp Require Import ereal topology normedtype sequences.
 (*                                                                            *)
 (* ## About sets of sets                                                      *)
 (* ```                                                                        *)
-(*      setI_closed G == the set of sets G is closed under finite             *)
-(*                       intersection                                         *)
-(*      setU_closed G == the set of sets G is closed under finite union       *)
 (*      setC_closed G == the set of sets G is closed under complement         *)
 (*     setSD_closed G == the set of sets G is closed under proper             *)
 (*                       difference                                           *)
@@ -153,8 +150,6 @@ Section set_systems.
 Context {T} (C : set (set T) -> Prop) (D : set T) (G : set (set T)).
 
 Definition setC_closed := forall A, G A -> G (~` A).
-Definition setI_closed := forall A B, G A -> G B -> G (A `&` B).
-Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
 Definition setSD_closed := forall A B, B `<=` A -> G A -> G B -> G (A `\` B).
 Definition setD_closed := forall A B, G A -> G B -> G (A `\` B).
 Definition setY_closed := forall A B, G A -> G B -> G (A `+` B).
@@ -196,7 +191,7 @@ Definition fin_trivIset_closed :=
   forall I (D : set I) (F : I -> set T), finite_set D -> trivIset D F ->
    (forall i, D i -> G (F i)) -> G (\bigcup_(k in D) F k).
 
-Definition setring := [/\ G set0, setU_closed & setD_closed].
+Definition setring := [/\ G set0, setU_closed G & setD_closed].
 
 Definition sigma_ring := [/\ G set0, setD_closed &
    (forall A : (set T)^nat, (forall n, G (A n)) -> G (\bigcup_k A k))].

theories/topology_theory/compact.v

@@ -1,6 +1,7 @@
-(* 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 all_ssreflect_compat all_algebra finmap all_classical.
+From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_classical.
 From mathcomp Require Import interval_inference reals topology_structure.
 From mathcomp Require Import uniform_structure pseudometric_structure.
 
@@ -234,9 +235,9 @@ Qed.
 Section Precompact.
 Context {X : topologicalType}.
 
-Lemma compactU (A B : set X) : compact A -> compact B -> compact (A `|` B).
+Lemma compactU : setU_closed (@compact X).
 Proof.
-rewrite compact_ultra => cptA cptB F UF FAB; rewrite setIUl.
+move=> A B; rewrite compact_ultra => cptA cptB F UF FAB; rewrite setIUl.
 have [/cptA[x AFx]|] := in_ultra_setVsetC A UF; first by exists x; left.
 move=> /(filterI FAB); rewrite setIUl setICr set0U => FBA.
 have /cptB[x BFx] : F B by apply: filterS FBA; exact: subIsetr.

theories/topology_theory/initial_topology.v

@@ -49,9 +49,9 @@ Definition wopen := [set f @^-1` A | A in open].
 Local Lemma wopT : wopen [set: W].
 Proof. by exists setT => //; apply: openT. Qed.
 
-Local Lemma wopI (A B : set W) : wopen A -> wopen B -> wopen (A `&` B).
+Local Lemma wopI : setI_closed wopen.
 Proof.
-by move=> [C Cop <-] [D Dop <-]; exists (C `&` D) => //; apply: openI.
+by move=> ? ? [C Cop <-] [D Dop <-]; exists (C `&` D) => //; exact: openI.
 Qed.
 
 Local Lemma wop_bigU (I : Type) (g : I -> set W) :

theories/topology_theory/topology_structure.v

@@ -1,6 +1,7 @@
-(* mathcomp analysis (c) 2025 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 all_ssreflect_compat all_algebra finmap all_classical.
+From mathcomp Require Import all_ssreflect_compat all_algebra finmap.
+From mathcomp Require Import all_classical.
 From mathcomp Require Export filter.
 
 (**md**************************************************************************)
@@ -169,9 +170,9 @@ Proof. by rewrite openE. Qed.
 Lemma openT : open (setT : set T).
 Proof. by rewrite openE => ??; apply: filterT. Qed.
 
-Lemma openI (A B : set T) : open A -> open B -> open (A `&` B).
+Lemma openI : setI_closed (@open T).
 Proof.
-rewrite openE => Aop Bop p [Ap Bp].
+move=> A B; rewrite openE => Aop Bop p [Ap Bp].
 by apply: filterI; [apply: Aop|apply: Bop].
 Qed.
 
@@ -182,9 +183,9 @@ rewrite openE => fop p [i Di].
 by have /fop fiop := Di; move/fiop; apply: filterS => ??; exists i.
 Qed.
 
-Lemma openU (A B : set T) : open A -> open B -> open (A `|` B).
+Lemma openU : setU_closed (@open T).
 Proof.
-by rewrite openE => Aop Bop p [/Aop|/Bop]; apply: filterS => ??; [left|right].
+by move=> A B /[!openE] AA BB p [/AA|/BB]; apply: filterS => ? ?; [left|right].
 Qed.
 
 Lemma open_subsetE (A B : set T) : open A -> (A `<=` B) = (A `<=` B°).
@@ -210,9 +211,8 @@ Qed.
 Lemma open_nbhsT (p : T) : open_nbhs p setT.
 Proof. by split=> //; apply: openT. Qed.
 
-Lemma open_nbhsI (p : T) (A B : set T) :
-  open_nbhs p A -> open_nbhs p B -> open_nbhs p (A `&` B).
-Proof. by move=> [Aop Ap] [Bop Bp]; split; [apply: openI|split]. Qed.
+Lemma open_nbhsI (p : T) : setI_closed (open_nbhs p).
+Proof. by move=> A B [Aop Ap] [Bop Bp]; split => //; exact: openI. Qed.
 
 Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A.
 Proof. by rewrite nbhsE => p_A; exists A. Qed.
@@ -455,7 +455,7 @@ Definition nbhs_of_open (T : Type) (op : set_system T) (p : T) (A : set T) :=
 HB.factory Record isOpenTopological T & Choice T := {
   op : set_system T ;
   opT : op setT ;
-  opI : forall (A B : set T), op A -> op B -> op (A `&` B) ;
+  opI : setI_closed op ;
   op_bigU : forall (I : Type) (f : I -> set T), (forall i, op (f i)) ->
     op (\bigcup_i f i)
 }.
@@ -739,9 +739,9 @@ move=> fcl t clft i Di; have /fcl := Di; apply.
 by move=> A /clft [s [/(_ i Di)]]; exists s.
 Qed.
 
-Lemma closedI (D E : set T) : closed D -> closed E -> closed (D `&` E).
+Lemma closedI : setI_closed closed.
 Proof.
-by move=> Dcl Ecl p clDEp; split; [apply: Dcl|apply: Ecl];
+by move=> D E Dcl Ecl p clDEp; split; [apply: Dcl|apply: Ecl];
   move=> A /clDEp [q [[]]]; exists q.
 Qed.
 
@@ -815,9 +815,8 @@ rewrite continuousP; split=> ctsf ? ?.
 by rewrite -closedC preimage_setC; apply: ctsf; rewrite closedC.
 Qed.
 
-Lemma closedU (T : topologicalType) (D E : set T) :
-  closed D -> closed E -> closed (D `|` E).
-Proof. by rewrite -?openC setCU; exact: openI. 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)
     (F : I -> set T) : (forall x, x \in s -> closed (F x)) ->
@@ -1003,11 +1002,11 @@ Implicit Type T : topologicalType.
 
 Definition clopen {T} (A : set T) := open A /\ closed A.
 
-Lemma clopenI {T} (A B : set T) : clopen A -> clopen B -> clopen (A `&` B).
-Proof. by case=> ? ? [] ? ?; split; [exact: openI | exact: closedI]. Qed.
+Lemma clopenI {T} : setI_closed (@clopen T).
+Proof. by move=> ? ? [] ? ? [] ? ?; split; [exact: openI|exact: closedI]. Qed.
 
-Lemma clopenU {T} (A B : set T) : clopen A -> clopen B -> clopen (A `|` B).
-Proof. by case=> ? ? [] ? ?; split; [exact: openU | exact: closedU]. Qed.
+Lemma clopenU {T} : setU_closed (@clopen T).
+Proof. by move=> ? ? [] ? ? [] ? ?; split; [exact: openU|exact: closedU]. Qed.
 
 Lemma clopenC {T} (A B : set T) : clopen A -> clopen (~`A).
 Proof. by case=> ? ?; split;[exact: closed_openC | exact: open_closedC ]. Qed.