From 23961b2260038d5d527cb44e2270891545d7be8e Mon Sep 17 00:00:00 2001 From: zstone Date: Sun, 27 Oct 2024 20:06:16 -0400 Subject: [PATCH 1/4] adding the sum topology --- CHANGELOG_UNRELEASED.md | 11 +++ _CoqProject | 1 + classical/mathcomp_extra.v | 8 ++- theories/Make | 2 + theories/separation_axioms.v | 23 ++++++ theories/topology_theory/sum_topology.v | 93 +++++++++++++++++++++++++ theories/topology_theory/topology.v | 1 + 7 files changed, 138 insertions(+), 1 deletion(-) create mode 100644 theories/topology_theory/sum_topology.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03c90f7b0..b7662e6de 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -57,6 +57,17 @@ `locally_compact_completely_regular`, and `completely_regular_regular`. +- in file `mathcomp_extra.v`, + + new definition `sum_fun`. +- in file `sum_topology.v`, + + new definition `sum_nbhs`. + + new lemmas `sum_nbhsE`, `existT_continuous`, `existT_open_map`, + `existT_nbhs`, `sum_openP`, `sum_continuous`, `sum_setUE`, and + `sum_compact`. +- in file `separation_axioms.v`, + + new lemma `sum_hausdorff`. + + ### Changed - in file `normedtype.v`, diff --git a/_CoqProject b/_CoqProject index 0c3ff3b81..0e755b047 100644 --- a/_CoqProject +++ b/_CoqProject @@ -58,6 +58,7 @@ theories/topology_theory/weak_topology.v theories/topology_theory/num_topology.v theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v +theories/topology_theory/sum_topology.v theories/separation_axioms.v theories/function_spaces.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2bb8f9f86..281c5f4b0 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -13,9 +13,11 @@ From mathcomp Require Import finset interval. (* dfwith f x == fun j => x if j = i, and f j otherwise *) (* given x : T i *) (* swap x := (x.2, x.1) *) -(* map_pair f x := (f x.1, f x.2) *) +(* map_pair f x := (f x.1, f x.2) *) (* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) (* {in A &, {mono f : x y /~ x <= y}} *) +(* sum_fun f := lifts a family of functions f into a function on *) +(* the dependent sum *) (* ``` *) (* *) (******************************************************************************) @@ -509,3 +511,7 @@ Proof. move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab). by rewrite in_itv/= !fge ?(itvP xab). Qed. + +Definition sum_fun {I : Type} {X : I -> Type} {T : Type} + (f : forall i, X i -> T) (x : {i & X i}) : T := + (f (projT1 x) (projT2 x)). \ No newline at end of file diff --git a/theories/Make b/theories/Make index 95312be86..2107e6e57 100644 --- a/theories/Make +++ b/theories/Make @@ -26,6 +26,8 @@ topology_theory/weak_topology.v topology_theory/num_topology.v topology_theory/quotient_topology.v topology_theory/one_point_compactification.v +topology_theory/sum_topology.v + separation_axioms.v function_spaces.v cantor.v diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 4f54e83e1..71e9b2ba6 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1125,3 +1125,26 @@ by move=> y [] ? [->] -> /eqP. Qed. End perfect_sets. + +Section sum_separations. +Context {I : choiceType} {X : I -> topologicalType}. + +Lemma sum_hausdorff : + (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}. +Proof. +move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= ?sum_nbhsE /= => cl. +have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]). +- by apply: existT_nbhs; exact: filterT. +- by apply: existT_nbhs; exact: filterT. +(* TODO: get rid of dependent destruct *) +move=> p [/= [? _] <- [ ? _]] [] E; destruct E => _. +congr( _ _); apply: hX => U V Ux Vy. +have [] := cl (existT X j @` U) (existT X j @` V). +- exact: existT_nbhs. +- exact: existT_nbhs. +move=> z [/= [l] ?] <- [r] Vr lr; exists l; split => //. +move: Vr; have -> // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr. +by move=> a b; case: (pselect (a = b)) => ?; [left | right]. +Qed. + +End sum_separations. \ No newline at end of file diff --git a/theories/topology_theory/sum_topology.v b/theories/topology_theory/sum_topology.v new file mode 100644 index 000000000..986b7e78f --- /dev/null +++ b/theories/topology_theory/sum_topology.v @@ -0,0 +1,93 @@ +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import topology_structure compact subspace_topology. + +(**md**************************************************************************) +(* # Sum topology *) +(* This file equips the dependent sum {i & X i} with its standard topology *) +(* *) +(* ``` *) +(* sum_nbhs x == the neighborhoods of the standard topology on the *) +(* dependent sum type {i & X i} *) +(* ``` *) +(******************************************************************************) + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Section sum_topology. +Context {I : choiceType} {X : I -> topologicalType}. + +Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := + (existT _ _) @ (nbhs (projT2 x)). + +Lemma sum_nbhsE (i : I) (x : X i) : + sum_nbhs (existT _ i x) = (existT _ _) @ (nbhs x). +Proof. by done. Qed. + +HB.instance Definition _ := hasNbhs.Build {i & X i} sum_nbhs. + +Local Lemma sum_nbhs_proper x : ProperFilter (sum_nbhs x). +Proof. by case: x => i xi; exact: fmap_proper_filter. Qed. + +Local Lemma sum_nbhs_singleton x A : sum_nbhs x A -> A x. +Proof. by case: x => ? ? /=; apply: nbhs_singleton. Qed. + +Local Lemma sum_nbhs_nbhs x A: sum_nbhs x A -> sum_nbhs x (sum_nbhs^~ A). +Proof. +case: x => i zi /=. + rewrite sum_nbhsE /= nbhsE /=; case => W [oW Wz WlA]. + exists W; first by split. + move=> x /= ?; move/filterS: WlA; apply. + by apply: open_nbhs_nbhs. +Qed. + +HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i} + sum_nbhs_proper sum_nbhs_singleton sum_nbhs_nbhs. + +Lemma existT_continuous (i : I) : continuous (existT X i). +Proof. by move=> ? ?. Qed. + +Lemma existT_open_map (i : I) (A : set (X i)): open A -> open (existT X i @` A). +Proof. +move=> oA; rewrite openE /interior /= => ?. +case=> x Ax <-; rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. +move: oA; rewrite openE => /(_ _ Ax); apply: filterS. +by move=> z => Az; exists z. +Qed. + +Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : + nbhs x U -> nbhs (existT _ i x) (existT _ i @` U). +Proof. by move/filterS; apply; exact: preimage_image. Qed. + +Lemma sum_openP (U : set {i & X i}) : + open U <-> (forall i, open (existT _ i@^-1` U)). +Proof. +split => ?. + by move=> i; apply: open_comp=> //; move=> y _; exact: existT_continuous. +rewrite openE /interior; case=> i x Uxi. +rewrite /nbhs /= sum_nbhsE; apply: open_nbhs_nbhs; split => //. +Qed. + +Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : + (forall i, continuous (f i)) -> continuous (sum_fun f). +Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed. + +Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: (X i)]). +Proof. +by rewrite eqEsubset; split; case=> i x //=; first by move=> _; exists i. +Qed. + +Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> + compact [set: {i&X i}]. +Proof. +move=> fsetI cptX. +rewrite sum_setUE -fsbig_setU //; apply: big_ind. +- exact: compact0. +- by move=> ? ? ? ?; exact: compactU. +move=> i _; apply: continuous_compact; last exact: cptX. +by apply: continuous_subspaceT; exact: existT_continuous. +Qed. + +End sum_topology. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 357618420..49cd835b4 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -15,3 +15,4 @@ From mathcomp Require Export topology_structure. From mathcomp Require Export uniform_structure. From mathcomp Require Export weak_topology. From mathcomp Require Export one_point_compactification. +From mathcomp Require Export sum_topology. From 8a344e8c3ecfb22d83876ed5f374da7b67157956 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 28 Oct 2024 10:08:03 +0900 Subject: [PATCH 2/4] wo destruct --- theories/separation_axioms.v | 31 +++++------ theories/topology_theory/sum_topology.v | 68 +++++++++++-------------- 2 files changed, 45 insertions(+), 54 deletions(-) diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 71e9b2ba6..281532c4b 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1129,22 +1129,19 @@ End perfect_sets. Section sum_separations. Context {I : choiceType} {X : I -> topologicalType}. -Lemma sum_hausdorff : +Lemma sum_hausdorff : (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}. Proof. -move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= ?sum_nbhsE /= => cl. -have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]). -- by apply: existT_nbhs; exact: filterT. -- by apply: existT_nbhs; exact: filterT. -(* TODO: get rid of dependent destruct *) -move=> p [/= [? _] <- [ ? _]] [] E; destruct E => _. -congr( _ _); apply: hX => U V Ux Vy. -have [] := cl (existT X j @` U) (existT X j @` V). -- exact: existT_nbhs. -- exact: existT_nbhs. -move=> z [/= [l] ?] <- [r] Vr lr; exists l; split => //. -move: Vr; have -> // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr. -by move=> a b; case: (pselect (a = b)) => ?; [left | right]. -Qed. - -End sum_separations. \ No newline at end of file +move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sum_nbhsE /= => cl. +have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]); + [by apply: existT_nbhs; exact: filterT..|]. +move=> p [/= [_ _ <-] [_ _ [ji]]] _. +rewrite {}ji {j} in x y cl *. +congr existT; apply: hX => U V Ux Vy. +have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. +move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. +rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr. +by move=> a b; exact: pselect. +Qed. + +End sum_separations. diff --git a/theories/topology_theory/sum_topology.v b/theories/topology_theory/sum_topology.v index 986b7e78f..d7faf31cf 100644 --- a/theories/topology_theory/sum_topology.v +++ b/theories/topology_theory/sum_topology.v @@ -19,10 +19,10 @@ Local Open Scope ring_scope. Section sum_topology. Context {I : choiceType} {X : I -> topologicalType}. -Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := - (existT _ _) @ (nbhs (projT2 x)). +Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := + existT _ _ @ nbhs (projT2 x). -Lemma sum_nbhsE (i : I) (x : X i) : +Lemma sum_nbhsE (i : I) (x : X i) : sum_nbhs (existT _ i x) = (existT _ _) @ (nbhs x). Proof. by done. Qed. @@ -32,62 +32,56 @@ Local Lemma sum_nbhs_proper x : ProperFilter (sum_nbhs x). Proof. by case: x => i xi; exact: fmap_proper_filter. Qed. Local Lemma sum_nbhs_singleton x A : sum_nbhs x A -> A x. -Proof. by case: x => ? ? /=; apply: nbhs_singleton. Qed. +Proof. by case: x => ? ? /=; exact: nbhs_singleton. Qed. Local Lemma sum_nbhs_nbhs x A: sum_nbhs x A -> sum_nbhs x (sum_nbhs^~ A). -Proof. -case: x => i zi /=. - rewrite sum_nbhsE /= nbhsE /=; case => W [oW Wz WlA]. - exists W; first by split. - move=> x /= ?; move/filterS: WlA; apply. - by apply: open_nbhs_nbhs. +Proof. +case: x => i Xi /=. +rewrite sum_nbhsE /= nbhsE /= => -[W [oW Wz WlA]]. +by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs. Qed. HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i} sum_nbhs_proper sum_nbhs_singleton sum_nbhs_nbhs. -Lemma existT_continuous (i : I) : continuous (existT X i). +Lemma existT_continuous (i : I) : continuous (existT X i). Proof. by move=> ? ?. Qed. -Lemma existT_open_map (i : I) (A : set (X i)): open A -> open (existT X i @` A). -Proof. -move=> oA; rewrite openE /interior /= => ?. -case=> x Ax <-; rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. +Lemma existT_open_map (i : I) (A : set (X i)) : open A -> open (existT X i @` A). +Proof. +move=> oA; rewrite openE /interior /= => iXi [x Ax <-]. +rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. move: oA; rewrite openE => /(_ _ Ax); apply: filterS. -by move=> z => Az; exists z. +by move=> z Az; exists z. Qed. -Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : +Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : nbhs x U -> nbhs (existT _ i x) (existT _ i @` U). -Proof. by move/filterS; apply; exact: preimage_image. Qed. +Proof. exact/filterS/preimage_image. Qed. -Lemma sum_openP (U : set {i & X i}) : - open U <-> (forall i, open (existT _ i@^-1` U)). +Lemma sum_openP (U : set {i & X i}) : + open U <-> forall i, open (existT _ i @^-1` U). Proof. -split => ?. - by move=> i; apply: open_comp=> //; move=> y _; exact: existT_continuous. -rewrite openE /interior; case=> i x Uxi. -rewrite /nbhs /= sum_nbhsE; apply: open_nbhs_nbhs; split => //. +split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous. +rewrite openE => -[i x Uxi]. +by rewrite /interior /nbhs/= sum_nbhsE; exact: open_nbhs_nbhs. Qed. -Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : +Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : (forall i, continuous (f i)) -> continuous (sum_fun f). Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed. -Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: (X i)]). -Proof. -by rewrite eqEsubset; split; case=> i x //=; first by move=> _; exists i. -Qed. +Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]). +Proof. by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed. -Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> - compact [set: {i&X i}]. +Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> + compact [set: {i & X i}]. Proof. -move=> fsetI cptX. -rewrite sum_setUE -fsbig_setU //; apply: big_ind. -- exact: compact0. -- by move=> ? ? ? ?; exact: compactU. -move=> i _; apply: continuous_compact; last exact: cptX. -by apply: continuous_subspaceT; exact: existT_continuous. +move=> fsetI cptX; rewrite sum_setUE -fsbig_setU//. +apply: big_rec; first exact: compact0. +move=> i ? _ cptx; apply: compactU => //. +apply: continuous_compact; last exact: cptX. +exact/continuous_subspaceT/existT_continuous. Qed. End sum_topology. From 0f2320c713b8e3fc6e32152426a4089a5f97c6a0 Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 29 Oct 2024 00:23:02 -0400 Subject: [PATCH 3/4] renaming sum to sigT --- CHANGELOG_UNRELEASED.md | 12 ++--- _CoqProject | 2 +- classical/mathcomp_extra.v | 6 +-- theories/Make | 2 +- theories/separation_axioms.v | 8 ++-- .../{sum_topology.v => sigT_topology.v} | 46 +++++++++---------- theories/topology_theory/topology.v | 2 +- 7 files changed, 39 insertions(+), 39 deletions(-) rename theories/topology_theory/{sum_topology.v => sigT_topology.v} (61%) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index b7662e6de..20afc4adc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,12 +58,12 @@ `completely_regular_regular`. - in file `mathcomp_extra.v`, - + new definition `sum_fun`. -- in file `sum_topology.v`, - + new definition `sum_nbhs`. - + new lemmas `sum_nbhsE`, `existT_continuous`, `existT_open_map`, - `existT_nbhs`, `sum_openP`, `sum_continuous`, `sum_setUE`, and - `sum_compact`. + + new definition `sigT_fun`. +- in file `sigT_topology.v`, + + new definition `sigT_nbhs`. + + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`, + `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and + `sigT_compact`. - in file `separation_axioms.v`, + new lemma `sum_hausdorff`. diff --git a/_CoqProject b/_CoqProject index 0e755b047..4a9bd2415 100644 --- a/_CoqProject +++ b/_CoqProject @@ -58,7 +58,7 @@ theories/topology_theory/weak_topology.v theories/topology_theory/num_topology.v theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v -theories/topology_theory/sum_topology.v +theories/topology_theory/sigT_topology.v theories/separation_axioms.v theories/function_spaces.v diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 281c5f4b0..4e1150553 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -16,7 +16,7 @@ From mathcomp Require Import finset interval. (* map_pair f x := (f x.1, f x.2) *) (* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) (* {in A &, {mono f : x y /~ x <= y}} *) -(* sum_fun f := lifts a family of functions f into a function on *) +(* sigT_fun f := lifts a family of functions f into a function on *) (* the dependent sum *) (* ``` *) (* *) @@ -512,6 +512,6 @@ move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab). by rewrite in_itv/= !fge ?(itvP xab). Qed. -Definition sum_fun {I : Type} {X : I -> Type} {T : Type} +Definition sigT_fun {I : Type} {X : I -> Type} {T : Type} (f : forall i, X i -> T) (x : {i & X i}) : T := - (f (projT1 x) (projT2 x)). \ No newline at end of file + (f (projT1 x) (projT2 x)). diff --git a/theories/Make b/theories/Make index 2107e6e57..cf786d30d 100644 --- a/theories/Make +++ b/theories/Make @@ -26,7 +26,7 @@ topology_theory/weak_topology.v topology_theory/num_topology.v topology_theory/quotient_topology.v topology_theory/one_point_compactification.v -topology_theory/sum_topology.v +topology_theory/sigT_topology.v separation_axioms.v function_spaces.v diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 281532c4b..ff6f7702c 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1126,13 +1126,13 @@ Qed. End perfect_sets. -Section sum_separations. +Section sigT_separations. Context {I : choiceType} {X : I -> topologicalType}. -Lemma sum_hausdorff : +Lemma sigT_hausdorff : (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}. Proof. -move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sum_nbhsE /= => cl. +move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sigT_nbhsE /= => cl. have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]); [by apply: existT_nbhs; exact: filterT..|]. move=> p [/= [_ _ <-] [_ _ [ji]]] _. @@ -1144,4 +1144,4 @@ rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr. by move=> a b; exact: pselect. Qed. -End sum_separations. +End sigT_separations. diff --git a/theories/topology_theory/sum_topology.v b/theories/topology_theory/sigT_topology.v similarity index 61% rename from theories/topology_theory/sum_topology.v rename to theories/topology_theory/sigT_topology.v index d7faf31cf..c0b779117 100644 --- a/theories/topology_theory/sum_topology.v +++ b/theories/topology_theory/sigT_topology.v @@ -4,45 +4,45 @@ From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import topology_structure compact subspace_topology. (**md**************************************************************************) -(* # Sum topology *) -(* This file equips the dependent sum {i & X i} with its standard topology *) +(* # sigT topology *) +(* This file equips the type {i & X i} with its standard topology *) (* *) (* ``` *) -(* sum_nbhs x == the neighborhoods of the standard topology on the *) -(* dependent sum type {i & X i} *) +(* sigT_nbhs x == the neighborhoods of the standard topology on the *) +(* type {i & X i} *) (* ``` *) (******************************************************************************) Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Section sum_topology. +Section sigT_topology. Context {I : choiceType} {X : I -> topologicalType}. -Definition sum_nbhs (x : {i & X i}) : set_system {i & X i} := +Definition sigT_nbhs (x : {i & X i}) : set_system {i & X i} := existT _ _ @ nbhs (projT2 x). -Lemma sum_nbhsE (i : I) (x : X i) : - sum_nbhs (existT _ i x) = (existT _ _) @ (nbhs x). +Lemma sigT_nbhsE (i : I) (x : X i) : + sigT_nbhs (existT _ i x) = (existT _ _) @ (nbhs x). Proof. by done. Qed. -HB.instance Definition _ := hasNbhs.Build {i & X i} sum_nbhs. +HB.instance Definition _ := hasNbhs.Build {i & X i} sigT_nbhs. -Local Lemma sum_nbhs_proper x : ProperFilter (sum_nbhs x). +Local Lemma sigT_nbhs_proper x : ProperFilter (sigT_nbhs x). Proof. by case: x => i xi; exact: fmap_proper_filter. Qed. -Local Lemma sum_nbhs_singleton x A : sum_nbhs x A -> A x. +Local Lemma sigT_nbhs_singleton x A : sigT_nbhs x A -> A x. Proof. by case: x => ? ? /=; exact: nbhs_singleton. Qed. -Local Lemma sum_nbhs_nbhs x A: sum_nbhs x A -> sum_nbhs x (sum_nbhs^~ A). +Local Lemma sigT_nbhs_nbhs x A: sigT_nbhs x A -> sigT_nbhs x (sigT_nbhs^~ A). Proof. case: x => i Xi /=. -rewrite sum_nbhsE /= nbhsE /= => -[W [oW Wz WlA]]. +rewrite sigT_nbhsE /= nbhsE /= => -[W [oW Wz WlA]]. by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs. Qed. HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i} - sum_nbhs_proper sum_nbhs_singleton sum_nbhs_nbhs. + sigT_nbhs_proper sigT_nbhs_singleton sigT_nbhs_nbhs. Lemma existT_continuous (i : I) : continuous (existT X i). Proof. by move=> ? ?. Qed. @@ -50,7 +50,7 @@ Proof. by move=> ? ?. Qed. Lemma existT_open_map (i : I) (A : set (X i)) : open A -> open (existT X i @` A). Proof. move=> oA; rewrite openE /interior /= => iXi [x Ax <-]. -rewrite /nbhs /= sum_nbhsE /= nbhs_simpl /=. +rewrite /nbhs /= sigT_nbhsE /= nbhs_simpl /=. move: oA; rewrite openE => /(_ _ Ax); apply: filterS. by move=> z Az; exists z. Qed. @@ -59,29 +59,29 @@ Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) : nbhs x U -> nbhs (existT _ i x) (existT _ i @` U). Proof. exact/filterS/preimage_image. Qed. -Lemma sum_openP (U : set {i & X i}) : +Lemma sigT_openP (U : set {i & X i}) : open U <-> forall i, open (existT _ i @^-1` U). Proof. split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous. rewrite openE => -[i x Uxi]. -by rewrite /interior /nbhs/= sum_nbhsE; exact: open_nbhs_nbhs. +by rewrite /interior /nbhs/= sigT_nbhsE; exact: open_nbhs_nbhs. Qed. -Lemma sum_continuous {Z : topologicalType} (f : forall i, X i -> Z) : - (forall i, continuous (f i)) -> continuous (sum_fun f). +Lemma sigT_continuous {Z : topologicalType} (f : forall i, X i -> Z) : + (forall i, continuous (f i)) -> continuous (sigT_fun f). Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed. -Lemma sum_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]). +Lemma sigT_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]). Proof. by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed. -Lemma sum_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> +Lemma sigT_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> compact [set: {i & X i}]. Proof. -move=> fsetI cptX; rewrite sum_setUE -fsbig_setU//. +move=> fsetI cptX; rewrite sigT_setUE -fsbig_setU//. apply: big_rec; first exact: compact0. move=> i ? _ cptx; apply: compactU => //. apply: continuous_compact; last exact: cptX. exact/continuous_subspaceT/existT_continuous. Qed. -End sum_topology. +End sigT_topology. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 49cd835b4..25460c770 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -15,4 +15,4 @@ From mathcomp Require Export topology_structure. From mathcomp Require Export uniform_structure. From mathcomp Require Export weak_topology. From mathcomp Require Export one_point_compactification. -From mathcomp Require Export sum_topology. +From mathcomp Require Export sigT_topology. From 5349d8bc0cbe43cd5f8815240ba67dbf624c7601 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Tue, 29 Oct 2024 08:03:38 -0400 Subject: [PATCH 4/4] Update CHANGELOG_UNRELEASED.md Co-authored-by: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 20afc4adc..31ab6ca7b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -65,7 +65,7 @@ `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and `sigT_compact`. - in file `separation_axioms.v`, - + new lemma `sum_hausdorff`. + + new lemma `sigT_hausdorff`. ### Changed