diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 549045ba2a..d0396d241f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 7ab2a157c7..4aeb97958d 100644 --- a/classical/classical_sets.v +++ b/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. diff --git a/classical/filter.v b/classical/filter.v index 62cbb550bb..1d658e36f4 100644 --- a/classical/filter.v +++ b/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. diff --git a/theories/measure_theory/measurable_structure.v b/theories/measure_theory/measurable_structure.v index 5fcf197942..327a7caf4a 100644 --- a/theories/measure_theory/measurable_structure.v +++ b/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))]. diff --git a/theories/topology_theory/compact.v b/theories/topology_theory/compact.v index 58d898e93d..4dec3f2488 100644 --- a/theories/topology_theory/compact.v +++ b/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. diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index c1c1077aa5..b800fda4fe 100644 --- a/theories/topology_theory/initial_topology.v +++ b/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) : diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index a8d31bc866..beba6022db 100644 --- a/theories/topology_theory/topology_structure.v +++ b/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.