From 73466454e3b707ec732120ddf93ec08989b7fa9e Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 28 Oct 2024 23:50:23 -0400 Subject: [PATCH 1/4] able to separate the discrete stuff more cleanly --- CHANGELOG_UNRELEASED.md | 123 +++++++++++ _CoqProject | 1 + theories/Make | 1 + theories/cantor.v | 54 +++-- theories/separation_axioms.v | 15 +- theories/sequences.v | 4 +- theories/topology_theory/bool_topology.v | 25 +-- theories/topology_theory/discrete_topology.v | 197 ++++++++++++++++++ theories/topology_theory/nat_topology.v | 67 ++---- .../topology_theory/pseudometric_structure.v | 95 --------- theories/topology_theory/topology.v | 1 + theories/topology_theory/topology_structure.v | 40 +--- 12 files changed, 390 insertions(+), 233 deletions(-) create mode 100644 theories/topology_theory/discrete_topology.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1ed83e6d9..e319ca1fa 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,6 +14,105 @@ + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, `derivable_horner`, `derivE`, `continuous_horner` + instance `is_derive_poly` +- in file `separation_axioms.v`, + + new lemmas `compact_normal_local`, and `compact_normal`. + +- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals` + with files + + `xfinmap.v` + + `discrete.v` + + `realseq.v` + + `realsum.v` + + `distr.v` + +- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals` + with file + + `Rstruct.v` + +- package `coq-mathcomp-analysis-stdlib` depending on + `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files + + `Rstruct_topology.v` + + `showcase/uniform_bigO.v` + +- in file `separation_axioms.v`, + + new lemmas `compact_normal_local`, and `compact_normal`. + +- in file `topology_theory/one_point_compactification.v`, + + new definitions `one_point_compactification`, and `one_point_nbhs`. + + new lemmas `one_point_compactification_compact`, + `one_point_compactification_some_nbhs`, + `one_point_compactification_some_continuous`, + `one_point_compactification_open_some`, + `one_point_compactification_weak_topology`, and + `one_point_compactification_hausdorff`. + +- in file `normedtype.v`, + + new definition `type` (in module `completely_regular_uniformity`) + + new lemmas `normal_completely_regular`, + `one_point_compactification_completely_reg`, + `nbhs_one_point_compactification_weakE`, + `locally_compact_completely_regular`, and + `completely_regular_regular`. + + new lemmas `near_in_itvoy`, `near_in_itvNyo` + +- in file `mathcomp_extra.v`, + + 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 `sigT_hausdorff`. + +- in `measure.v`: + + lemma `countable_measurable` +- in `realfun.v`: + + lemma `cvgr_dnbhsP` + + new definitions `prodA`, and `prodAr`. + + new lemmas `prodAK`, `prodArK`, and `swapK`. +- in file `product_topology.v`, + + new lemmas `swap_continuous`, `prodA_continuous`, and + `prodAr_continuous`. + +- file `homotopy_theory/homotopy.v` +- file `homotopy_theory/wedge_sigT.v` +- in file `homotopy_theory/wedge_sigT.v` + + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. + + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, + `wedge_liftE`, `wedge_openP`, + `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, + `wedge_compact`, `wedge_connected`. + +- in `boolp.`: + + lemma `existT_inj` +- in file `order_topology.v` + + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and + `max_fun_continuous`. + +- in file `bool_topology.v`, + + new lemma `bool_compact`. + +### Changed + +- in file `normedtype.v`, + changed `completely_regular_space` to depend on uniform separators + which removes the dependency on `R`. The old formulation can be + recovered easily with `uniform_separatorP`. + +- moved from `Rstruct.v` to `Rstruct_topology.v` + + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, + `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` + and `nbhs_pt_comp` + +- moved from `real_interval.v` to `normedtype.v` + + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, + `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, + `disj_itv_Rhull` +- in `topology.v`: + + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, + `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned + into local `Let`'s - in `lebesgue_integral.v`: + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` @@ -43,6 +142,15 @@ - moved from `lebesgue_integral.v` to `measure.v` and generalized + lemmas `measurable_xsection`, `measurable_ysection` +- moved from `topology_structure.v` to `discrete_topology.v`: + `discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`. + +- moved from `pseudometric_structure.v` to `discrete_topology.v`: + `discrete_ent`, `discrete_ball`, and `discrete_topology`. + +- in file `cantor.v`, `cantor_space` now defined in terms of `bool`. +- in file `separation_axioms.v`, updated `discrete_hausdorff`, and + `discrete_zero_dimension` to take a `discreteTopologicalType`. ### Renamed @@ -76,6 +184,21 @@ - in `sequences.v`: + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) +- in `lebesgue_integral.v`: + + definition `cst_mfun` + + lemma `mfun_cst` + +- in `cardinality.v`: + + lemma `cst_fimfun_subproof` + +- in `lebesgue_integral.v`: + + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) + + lemma `cst_nnfun_subproof` (turned into a `Let`) + + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) +- in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`. +- in file `nat_topology.v`, removed `discrete_nat`. +- in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and + `discrete_space_discrete`. ### Infrastructure diff --git a/_CoqProject b/_CoqProject index a8b38635c..713f59627 100644 --- a/_CoqProject +++ b/_CoqProject @@ -60,6 +60,7 @@ theories/topology_theory/num_topology.v theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v theories/topology_theory/sigT_topology.v +theories/topology_theory/discrete_topology.v theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v diff --git a/theories/Make b/theories/Make index 35f6699fb..57fb3ba0a 100644 --- a/theories/Make +++ b/theories/Make @@ -28,6 +28,7 @@ topology_theory/num_topology.v topology_theory/quotient_topology.v topology_theory/one_point_compactification.v topology_theory/sigT_topology.v +topology_theory/discrete_topology.v homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v diff --git a/theories/cantor.v b/theories/cantor.v index b40e5631f..6160b1552 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -43,12 +43,13 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. -Definition cantor_space := - prod_topology (fun _ : nat => discrete_topology discrete_bool). +Definition cantor_space : Type := + prod_topology (fun _ : nat => bool). HB.instance Definition _ := Pointed.on cantor_space. HB.instance Definition _ := Nbhs.on cantor_space. HB.instance Definition _ := Topological.on cantor_space. +HB.instance Definition _ := Uniform.on cantor_space. Definition cantor_like (T : topologicalType) := [/\ perfect_set [set: T], @@ -58,20 +59,18 @@ Definition cantor_like (T : topologicalType) := Lemma cantor_space_compact : compact [set: cantor_space]. Proof. -have := @tychonoff _ (fun _ : nat => _) _ (fun=> discrete_bool_compact). +have := @tychonoff _ (fun _ : nat => _) _ (fun=> bool_compact). by congr (compact _); rewrite eqEsubset. Qed. Lemma cantor_space_hausdorff : hausdorff_space cantor_space. Proof. apply: hausdorff_product => ?; apply: discrete_hausdorff. -exact: discrete_space_discrete. Qed. Lemma cantor_zero_dimensional : zero_dimensional cantor_space. Proof. apply: zero_dimension_prod => _; apply: discrete_zero_dimension. -exact: discrete_space_discrete. Qed. Lemma cantor_perfect : perfect_set [set: cantor_space]. @@ -102,13 +101,12 @@ Qed. (* *) (******************************************************************************) Section topological_trees. -Context {K : nat -> ptopologicalType} {X : ptopologicalType} +Context {K : nat -> pdiscreteTopologicalType} {X : ptopologicalType} (refine_apx : forall n, set X -> K n -> set X) (tree_invariant : set X -> Prop). Hypothesis cmptX : compact [set: X]. Hypothesis hsdfX : hausdorff_space X. -Hypothesis discreteK : forall n, discrete_space (K n). Hypothesis refine_cover : forall n U, U = \bigcup_e @refine_apx n U e. Hypothesis refine_invar : forall n U e, tree_invariant U -> tree_invariant (@refine_apx n U e). @@ -122,7 +120,7 @@ Hypothesis refine_separates: forall x y : X, x != y -> Let refine_subset n U e : @refine_apx n U e `<=` U. Proof. by rewrite [X in _ `<=` X](refine_cover n); exact: bigcup_sup. Qed. -Let T := prod_topology K. +Let T := prod_topology (K : nat -> ptopologicalType). Local Fixpoint branch_apx (b : T) n := if n is m.+1 then refine_apx (branch_apx b m) (b m) else [set: X]. @@ -193,7 +191,6 @@ near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z). move=> [->]; near: z; exists (proj n @^-1` [set b n]). split => //; suff : @open T (proj n @^-1` [set b n]) by []. apply: open_comp; [move=> + _; exact: proj_continuous| apply: discrete_open]. -exact: discreteK. Unshelve. all: end_near. Qed. Let apx_prefix b c n : @@ -293,9 +290,7 @@ Local Lemma cantor_map : exists f : cantor_space -> T, set_surj [set: cantor_space] [set: T] f & set_inj [set: cantor_space] f ]. Proof. -have [] := @tree_map_props - (fun=> discrete_topology discrete_bool) T c_ind c_invar cmptT hsdfT. -- by move=> ?; exact: discrete_space_discrete. +have [] := @tree_map_props (fun=> bool) T c_ind c_invar cmptT hsdfT. - move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//]. have [?|?] := pselect (U_ n `&` V !=set0 /\ ~` U_ n `&` V !=set0). + have [Unt|Unt] := pselect (U_ n t). @@ -350,38 +345,40 @@ Qed. End TreeStructure. +Section cantor. +Context {R : realType}. + (**md**************************************************************************) (* ## Part 3: Finitely branching trees are Cantor-like *) (******************************************************************************) Section FinitelyBranchingTrees. Definition tree_of (T : nat -> pointedType) : Type := - prod_topology (fun n => discrete_topology_type (T n)). + prod_topology (fun n => discrete_topology (T n)). HB.instance Definition _ (T : nat -> pointedType) : Pointed (tree_of T):= Pointed.on (tree_of T). HB.instance Definition _ (T : nat -> pointedType) := Uniform.on (tree_of T). -HB.instance Definition _ {R : realType} (T : nat -> pointedType) : +HB.instance Definition _ (T : nat -> pointedType) : @PseudoMetric R _ := @PseudoMetric.on (tree_of T). Lemma cantor_like_finite_prod (T : nat -> ptopologicalType) : - (forall n, finite_set [set: discrete_topology_type (T n)]) -> + (forall n, finite_set [set: discrete_topology (T n)]) -> (forall n, (exists xy : T n * T n, xy.1 != xy.2)) -> cantor_like (tree_of T). Proof. move=> finiteT twoElems; split. -- exact/(@perfect_diagonal (discrete_topology_type \o T))/twoElems. +- exact/(@perfect_diagonal (discrete_topology \o T))/twoElems. - have := tychonoff (fun n => finite_compact (finiteT n)). set A := (X in compact X -> _). suff : A = [set: tree_of (fun x : nat => T x)] by move=> ->. by rewrite eqEsubset. -- apply: (@hausdorff_product _ (discrete_topology_type \o T)) => n. +- apply: (@hausdorff_product _ (discrete_topology \o T)) => n. by apply: discrete_hausdorff; exact: discrete_space_discrete. - apply: zero_dimension_prod => ?; apply: discrete_zero_dimension. - exact: discrete_space_discrete. Qed. End FinitelyBranchingTrees. @@ -390,7 +387,7 @@ End FinitelyBranchingTrees. (* ## Part 4: Building a finitely branching tree to cover `T` *) (******************************************************************************) Section alexandroff_hausdorff. -Context {R : realType} {T : pseudoPMetricType R}. +Context {T : pseudoPMetricType R}. Hypothesis cptT : compact [set: T]. Hypothesis hsdfT : hausdorff_space T. @@ -469,9 +466,14 @@ HB.instance Definition _ n := gen_eqMixin (K' n). HB.instance Definition _ n := gen_choiceMixin (K' n). HB.instance Definition _ n := isPointed.Build (K' n) (K'p n). -Let K n := K' n. +Let K n := discrete_topology (K' n). Let Tree := @tree_of K. +HB.instance Definition _ n := + DiscreteTopology.on (K n). +HB.instance Definition _ n := + Pointed.on (K n). + Let embed_refine n (U : set T) (k : K n) := (if pselect (projT1 k `&` U !=set0) then projT1 k @@ -486,17 +488,12 @@ case: e => W; have [//| _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))). exact. Qed. -Let discrete_subproof (P : choiceType) : - discrete_space (principal_filter_type P). -Proof. by []. Qed. - Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T, continuous f & set_surj [set: Tree] [set: T] f. Proof. pose entn n := projT2 (cid (ent_balls' (count_unif n))). -have [//| | |? []//| |? []// | |] := @tree_map_props - (discrete_topology_type \o K) T (embed_refine) (embed_invar) cptT hsdfT. -- by move=> n; exact: discrete_space_discrete. +have [ | |? []//| |? []// | |] := @tree_map_props + K T (embed_refine) (embed_invar) cptT hsdfT. - move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//]. have [//|_ _ _ + _] := entn n; rewrite -subTset. move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //. @@ -535,7 +532,7 @@ Local Lemma cantor_surj_pt2 : exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f. Proof. have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f. -apply: (@cantor_like_finite_prod (discrete_topology_type \o K)) => [n /=|n]. +apply: (@cantor_like_finite_prod (discrete_topology \o K)) => [n /=|n]. have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))). suff -> : [set: {classic K' n}] = (@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))). @@ -569,3 +566,4 @@ by exists f; rewrite -cstf; exact: cst_continuous. Qed. End alexandroff_hausdorff. +End cantor. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 023e28739..ff2dfd228 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -111,11 +111,6 @@ have [q [Aq clsAp_q]] := !! Aco _ _ pA; rewrite (hT p q) //. by apply: cvg_cluster clsAp_q; apply: cvg_within. Qed. -Lemma discrete_hausdorff {dsc : discrete_space T} : hausdorff_space. -Proof. -by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->. -Qed. - Lemma compact_cluster_set1 (x : T) F V : hausdorff_space -> compact V -> nbhs x V -> ProperFilter F -> F V -> cluster F = [set x] -> F --> x. @@ -211,6 +206,12 @@ move=> [[P Q]] /= [Px Qx] /= [/open_subspaceW oP /open_subspaceW oQ]. by move=> ?; exists (P, Q); split => //=; [exact: oP | exact: oQ]. Qed. +Lemma discrete_hausdorff {T : discreteTopologicalType} : hausdorff_space T. +Proof. +by move=> p q /(_ _ _ (discrete_set1 p) (discrete_set1 q)) [] // x [] -> ->. +Qed. + + Lemma order_hausdorff {d} {T : orderTopologicalType d} : hausdorff_space T. Proof. rewrite open_hausdorff=> p q; wlog : p q / (p < q)%O. @@ -567,9 +568,9 @@ Definition totally_disconnected {T} (A : set T) := Definition zero_dimensional T := (forall x y, x != y -> exists U : set T, [/\ clopen U, U x & ~ U y]). -Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T. +Lemma discrete_zero_dimension {T : discreteTopologicalType} : zero_dimensional T. Proof. -move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP. +move=> x y xny; exists [set x]; split => //; last exact/nesym/eqP. by split; [exact: discrete_open | exact: discrete_closed]. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index e520f2c9a..25152d5dc 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1316,9 +1316,9 @@ Lemma cvg_nseries_near (u : nat^nat) : cvgn (nseries u) -> \forall n \near \oo, u n = 0%N. Proof. move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l]. - by exists [set l]; split=> //; exists [set l] => //; rewrite bigcup_set1. + by rewrite nbhs_principalE. have /ul[b _ bul] : nbhs l [set l.-1; l]. - by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1. + by rewrite nbhs_principalE ; apply/principal_filterP => /=; right. exists (maxn a b) => // n /= abn. rewrite (_ : u = fun n => nseries u n.+1 - nseries u n)%N; last first. by rewrite funeqE => i; rewrite /nseries big_nat_recr//= addnC addnK. diff --git a/theories/topology_theory/bool_topology.v b/theories/topology_theory/bool_topology.v index ef2df6951..5950ac34e 100644 --- a/theories/topology_theory/bool_topology.v +++ b/theories/topology_theory/bool_topology.v @@ -3,6 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import signed reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology compact. +From mathcomp Require Import discrete_topology. (**md**************************************************************************) (* # Topology for boolean numbers *) @@ -15,25 +16,19 @@ Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -HB.instance Definition _ := Nbhs_isNbhsTopological.Build bool - principal_filter_proper discrete_sing discrete_nbhs. - -Lemma discrete_bool : discrete_space bool. -Proof. by []. Qed. +HB.instance Definition _ := hasNbhs.Build bool principal_filter. +HB.instance Definition _ := Discrete_ofNbhs.Build bool erefl. +HB.instance Definition _ := DiscreteUniform_ofNbhs.Build bool. Lemma bool_compact : compact [set: bool]. Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. -Section bool_ord_topology. -Local Open Scope classical_set_scope. -Local Open Scope order_scope. - Local Lemma bool_nbhs_itv (b : bool) : nbhs b = filter_from (fun i => itv_open_ends i /\ b \in i) (fun i => [set` i]). Proof. -rewrite discrete_bool eqEsubset; split=> U; first last. +rewrite nbhs_principalE eqEsubset; split=> U; first last. by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb. move/principal_filterP; case: b. move=> Ut; exists `]false, +oo[; first split => //; first by left. @@ -43,12 +38,6 @@ by move=> r /=; rewrite in_itv /=; case: r. Qed. HB.instance Definition _ := Order_isNbhs.Build _ bool bool_nbhs_itv. -End bool_ord_topology. - -Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool]. -Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. - -Definition pseudoMetric_bool {R : realType} : pseudoMetricType R := - discrete_topology discrete_bool. -#[global] Hint Resolve discrete_bool : core. +HB.instance Definition _ {R : numDomainType} := + @DiscretePseudoMetric_ofUniform.Build R bool. diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v new file mode 100644 index 000000000..94e837eb8 --- /dev/null +++ b/theories/topology_theory/discrete_topology.v @@ -0,0 +1,197 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals. +From mathcomp Require Import topology_structure uniform_structure. +From mathcomp Require Import order_topology pseudometric_structure compact. + +Import Order.TTheory GRing.Theory Num.Def Num.Theory. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + + +HB.mixin Record Discrete_ofNbhs T of Nbhs T := { + nbhs_principalE : (@nbhs T _) = principal_filter; +}. + +#[short(type="discreteNbhsType")] +HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}. + + +Definition discrete_ent {T} : set (set (T * T)) := + globally (range (fun x => (x, x))). + +(** Note: having the discrete topology does not guarantee the discrete + uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *) +HB.mixin Record Discrete_ofUniform T of Uniform T := { + uniform_discrete : @entourage T = discrete_ent +}. + +Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y. + +HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of + PseudoMetric R T := { + metric_discrete : @ball R T = @discrete_ball R T +}. + +#[short(type="discreteTopologicalType")] +HB.structure Definition DiscreteTopology := + { T of DiscreteNbhs T & Topological T}. + +#[short(type="discreteOrderTopologicalType")] +HB.structure Definition DiscreteOrderTopology d := + { T of Discrete_ofNbhs T & OrderTopological d T}. + +#[short(type="pdiscreteTopologicalType")] +HB.structure Definition PointedDiscreteTopology := + { T of DiscreteTopology T & Pointed T}. + +#[short(type="pdiscreteOrderTopologicalType")] +HB.structure Definition PointedDiscreteOrderTopology d := + { T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}. + +#[short(type="discreteUniformType")] +HB.structure Definition DiscreteUniform := + { T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}. + +#[short(type="discretePseudoMetricType")] +HB.structure Definition DiscretePseudoMetric {R : numDomainType} := + { T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}. + +HB.builders Context T of Discrete_ofNbhs T. + +Local Lemma principal_nbhs_filter (p : T) : ProperFilter (nbhs p). +Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed. + +Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p. +Proof. by rewrite nbhs_principalE => /principal_filterP. Qed. + +Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A). +Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed. + +HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T + principal_nbhs_filter principal_nbhs_singleton principal_nbhs_nbhs. + +HB.end. + +HB.factory Record DiscreteUniform_ofNbhs T of Discrete_ofNbhs T & Nbhs T := {}. +HB.builders Context T of DiscreteUniform_ofNbhs T. + +Local Open Scope relation_scope. + +Local Notation d := (@discrete_ent T). + +Local Lemma discrete_entourage_filter : Filter d. +Proof. exact: globally_filter. Qed. + +Local Lemma discrete_entourage_diagonal : forall A, d A -> diagonal `<=` A. +Proof. +by move=> ? + x x12; apply; exists x.1; rewrite // {2}x12 -surjective_pairing. +Qed. + +Local Lemma discrete_entourage_inv : forall A, d A -> d A^-1. +Proof. by move=> ? dA x [i _ <-]; apply: dA; exists i. Qed. + +Local Lemma discrete_entourage_split_ex : + forall A, d A -> exists2 B, d B & B \; B `<=` A. +Proof. +move=> ? dA; exists (range (fun x => (x, x))) => //. +by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i. +Qed. + +Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d. +Proof. +rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U. + move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. + by move=> z /= /set_mem; rewrite /diagonal /= => <-. +case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set. +exact: entW. +Qed. + +HB.instance Definition _ := @Nbhs_isUniform.Build T + discrete_ent + discrete_entourage_filter + discrete_entourage_diagonal + discrete_entourage_inv + discrete_entourage_split_ex + discrete_entourage_nbhsE. + +HB.instance Definition _ := @Discrete_ofUniform.Build T erefl. + +HB.end. + +HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of + DiscreteUniform T := {}. + +HB.builders Context R T of DiscretePseudoMetric_ofUniform R T. + +Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> + @discrete_ball R T x eps x. +Proof. by []. Qed. + +Local Lemma discrete_ball_sym (x y : T) (e : R) : + discrete_ball x e y -> discrete_ball y e x. +Proof. by move=>->. Qed. +Local Lemma discrete_ball_triangle (x y z:T) (e1 e2 : R) : + discrete_ball x e1 y -> discrete_ball y e2 z -> discrete_ball x (e1 + e2) z. +Proof. by move=> -> ->. Qed. + +Local Lemma discrete_entourageE : entourage = entourage_ (@discrete_ball R T). +Proof. +rewrite predeqE => P; rewrite uniform_discrete; split; last first. + by move=> dbP ? [?] _ <-; move: dbP; case => /= ? ?; apply. +move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //. +by rewrite {2}z12 -surjective_pairing. +Qed. + +HB.instance Definition _ := + @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) + discrete_ball_center discrete_ball_sym discrete_ball_triangle + discrete_entourageE. + +Local Lemma discrete_ballE : @ball R T = @discrete_ball R T. +Proof. by rewrite funeq2E => ? ?. Qed. + +HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE. + +HB.end. + +(** we introducing an alias attaching discrete structures for + topology, uniformity, and pseudometric *) +Definition discrete_topology (T : Type) : Type := T. +HB.instance Definition _ (T : choiceType) := + Choice.copy (discrete_topology T) T. +HB.instance Definition _ (T : pointedType) := + Pointed.on (discrete_topology T). +HB.instance Definition _ (T : choiceType) := + hasNbhs.Build (discrete_topology T) principal_filter. +HB.instance Definition _ (T : choiceType) := + Discrete_ofNbhs.Build (discrete_topology T) erefl. +HB.instance Definition _ (T : choiceType) := + DiscreteUniform_ofNbhs.Build (discrete_topology T). +HB.instance Definition _ {R : numDomainType} (T : choiceType) := + @DiscretePseudoMetric_ofUniform.Build R (discrete_topology T). + +Section discrete_topology. + +Context {X : discreteTopologicalType}. + +Lemma discrete_open (A : set X) : open A. +Proof. +rewrite openE => ? ?; rewrite /interior nbhs_principalE. +exact/principal_filterP. +Qed. + +Lemma discrete_set1 (x : X) : nbhs x [set x]. +Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed. + +Lemma discrete_closed (A : set X) : closed A. +Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed. + +Lemma discrete_cvg (F : set_system X) (x : X) : + Filter F -> F --> x <-> F [set x]. +Proof. +rewrite nbhs_principalE nbhs_simpl; split; first by exact. +by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->. +Qed. + +End discrete_topology. diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v index 4325ac634..0885f8c05 100644 --- a/theories/topology_theory/nat_topology.v +++ b/theories/topology_theory/nat_topology.v @@ -4,6 +4,7 @@ From mathcomp Require Import all_ssreflect all_algebra archimedean. From mathcomp Require Import all_classical. From mathcomp Require Import signed reals topology_structure uniform_structure. From mathcomp Require Import pseudometric_structure order_topology. +From mathcomp Require Import discrete_topology. (**md**************************************************************************) (* # Topology for natural numbers *) @@ -16,20 +17,29 @@ Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. -Section nat_topologicalType. +HB.instance Definition _ := hasNbhs.Build nat principal_filter. +HB.instance Definition _ := Discrete_ofNbhs.Build nat erefl. -Let D : set nat := setT. -Let b : nat -> set nat := fun i => [set i]. -Let bT : \bigcup_(i in D) b i = setT. -Proof. by rewrite predeqE => i; split => // _; exists i. Qed. - -Let bD : 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]. -Proof. by move=> i j t _ _ -> ->; exists j. Qed. - -HB.instance Definition _ := isBaseTopological.Build nat bT bD. +Local Lemma nat_nbhs_itv (n : nat) : + nbhs n = filter_from + (fun i => itv_open_ends i /\ n \in i) + (fun i => [set` i]). +Proof. +rewrite nbhs_principalE eqEsubset; split=> U; first last. + by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb. +move/principal_filterP; case: n. + move=> U0; exists `]-oo, 1[; first split => //; first by left. + by move=> r /=; rewrite in_itv /=; case: r. +move=> n USn; exists `]n, n.+2[; first split => //; first by right. + by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=. +move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->. +exact/esym/le_anti. +Qed. -End nat_topologicalType. +HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv. +HB.instance Definition _ := DiscreteUniform_ofNbhs.Build nat. +HB.instance Definition _ {R : numDomainType} := + @DiscretePseudoMetric_ofUniform.Build R nat. Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N. Proof. by exists N.+1. Qed. @@ -102,6 +112,7 @@ by near: m; apply: AF; near: B; apply: nbhs_infty_ge. Unshelve. all: end_near. Qed. Section map. + Context {I : Type} {F : set_system I} {FF : Filter F} (f : I -> nat). Lemma cvgnyPge : @@ -123,35 +134,3 @@ Proof. exact: (cvgnyP 0%N 4%N). Qed. End map. End infty_nat. - -Lemma discrete_nat : discrete_space nat. -Proof. -rewrite /discrete_space predeq2E => n U; split. - by case => /= V [_ Vn VU]; exact/principal_filterP/VU. -move/principal_filterP => Un; exists U; split => //=; exists U => //. -by rewrite eqEsubset; split => [z [i Ui ->//]|z Uz]; exists z. -Qed. - -Section nat_ord_topology. -Local Open Scope classical_set_scope. -Local Open Scope order_scope. - -Local Lemma nat_nbhs_itv (n : nat) : - nbhs n = filter_from - (fun i => itv_open_ends i /\ n \in i) - (fun i => [set` i]). -Proof. -rewrite discrete_nat eqEsubset; split=> U; first last. - by case => V [_ Vb] VU; apply/principal_filterP/VU; apply: Vb. -move/principal_filterP; case: n. - move=> U0; exists `]-oo, 1[; first split => //; first by left. - by move=> r /=; rewrite in_itv /=; case: r. -move=> n USn; exists `]n, n.+2[; first split => //; first by right. - by rewrite in_itv; apply/andP;split => //=; rewrite /Order.lt //=. -move=> r /=; rewrite in_itv /= => nr2; suff: r = n.+1 by move=> ->. -exact/esym/le_anti. -Qed. - -HB.instance Definition _ := Order_isNbhs.Build _ nat nat_nbhs_itv. - -End nat_ord_topology. diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index ec133325f..a88c1d2bd 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/theories/topology_theory/pseudometric_structure.v @@ -19,19 +19,11 @@ From mathcomp Require Import signed reals topology_structure uniform_structure. (* structure: a type equipped with balls *) (* The HB class is PseudoMetric. *) (* pseudoPMetricType == a pointed pseudoMetric space *) -(* discrete_topology dscT == the discrete topology on T, provided *) -(* dscT : discrete_space T *) (* ball x e == ball of center x and radius e *) (* nbhs_ball_ ball == nbhs defined using the given balls *) (* nbhs_ball == nbhs defined using balls in a *) (* pseudometric space *) -(* discrete_ent == entourages of the discrete uniformity *) -(* topology *) -(* discrete_ball == singleton balls for the discrete metric *) -(* discrete_topology_type == equip choice types with a discrete *) -(* topology *) (* ``` *) -(* `discrete_ent` is equipped with the `Uniform` structure. *) (* ### Factories *) (* ``` *) (* Nbhs_isPseudoMetric == factory to build a topological space *) @@ -89,37 +81,6 @@ HB.structure Definition PseudoMetric (R : numDomainType) := HB.structure Definition PseudoPointedMetric (R : numDomainType) := {T of Pointed T & Uniform T & Uniform_isPseudoMetric R T}. -Definition discrete_topology T (dsc : discrete_space T) : Type := T. - -Section discrete_uniform. -Context {T : nbhsType} {dsc: discrete_space T}. - -Definition discrete_ent : set (set (T * T)) := - globally (range (fun x => (x, x))). - -Program Definition discrete_uniform_structure := - @isUniform.Build (discrete_topology dsc) discrete_ent _ _ _ _. -Next Obligation. -by move=> ? + x x12; apply; exists x.1; rewrite // {2}x12 -surjective_pairing. -Qed. -Next Obligation. -by move=> ? dA x [i _ <-]; apply: dA; exists i. -Qed. -Next Obligation. -move=> ? dA; exists (range (fun x => (x, x))) => //. -by rewrite set_compose_diag => x [i _ <-]; apply: dA; exists i. -Qed. - -HB.instance Definition _ := Choice.on (discrete_topology dsc). -HB.instance Definition _ := discrete_uniform_structure. -End discrete_uniform. - -HB.instance Definition _ (P : pnbhsType) (dsc : discrete_space P) := - Pointed.on (discrete_topology dsc). - -HB.instance Definition _ {T : pnbhsType} {dsc: discrete_space T} := - Pointed.on (discrete_topology dsc). - (* was uniformityOfBallMixin *) HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := { ent : set_system (M * M); @@ -381,62 +342,6 @@ Qed. (** Specific pseudoMetric spaces *) -Section discrete_pseudoMetric. -Context {R : numDomainType} {T : nbhsType} {dsc : discrete_space T}. - -Definition discrete_ball (x : T) (eps : R) y : Prop := x = y. - -Lemma discrete_ball_center x (eps : R) : 0 < eps -> discrete_ball x eps x. -Proof. by []. Qed. - -Program Definition discrete_pseudometric_structure := - @Uniform_isPseudoMetric.Build R (discrete_topology dsc) discrete_ball - _ _ _ _. -Next Obligation. by done. Qed. -Next Obligation. by move=> ? ? ? ->. Qed. -Next Obligation. by move=> ? ? ? ? ? -> ->. Qed. -Next Obligation. -rewrite predeqE => P; split; last first. - by case=> e _ leP; move=> [a b] [i _] [-> ->]; apply: leP. -move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //. -by rewrite {2}z12 -surjective_pairing. -Qed. - -HB.instance Definition _ := discrete_pseudometric_structure. -End discrete_pseudoMetric. - -(** we use `discrete_topology` to equip choice types with a discrete topology *) -Section discrete_topology. - -Let discrete_subproof (P : choiceType) : - discrete_space (principal_filter_type P). -Proof. by []. Qed. - -Definition discrete_topology_type (P : Type) : Type := P. - -HB.instance Definition _ (P : choiceType) := Choice.copy - (discrete_topology_type P) (discrete_topology (discrete_subproof P)). -HB.instance Definition _ (P : choiceType) := Filtered.copy - (discrete_topology_type P) (discrete_topology (discrete_subproof P)). -HB.instance Definition _ (P : choiceType) := Uniform.copy - (discrete_topology_type P) (discrete_topology (discrete_subproof P)). -HB.instance Definition _ (P : pointedType) := Pointed.copy - (discrete_topology_type P) (discrete_topology (discrete_subproof P)). -HB.instance Definition _ R (P : choiceType) : @PseudoMetric R _ := - PseudoMetric.copy - (discrete_topology_type P) (discrete_topology (discrete_subproof P)). - -End discrete_topology. - -Lemma discrete_space_discrete (P : choiceType) : - discrete_space (discrete_topology_type P). -Proof. -apply/funext => /= x; apply/funext => A; apply/propext; split. -- by move=> [E hE EA] _ ->; apply/EA/xsectionP/hE; exists x. -- move=> h; exists diagonal; first by move=> -[a b] [t _] [<- <-]. - by move=> y /xsectionP/= xy; exact: h. -Qed. - HB.instance Definition _ (R : zmodType) := isPointed.Build R 0. Definition ball_ diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 604b4af8a..08196df68 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -17,3 +17,4 @@ From mathcomp Require Export uniform_structure. From mathcomp Require Export weak_topology. From mathcomp Require Export one_point_compactification. From mathcomp Require Export sigT_topology. +From mathcomp Require Export discrete_topology. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 8eaf56dbb..0127775e7 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -39,15 +39,13 @@ From mathcomp Require Export filter. (* x^' == set of neighbourhoods of x where x is *) (* excluded (a "deleted neighborhood") *) (* limit_point E == the set of limit points of E *) -(* discrete_space T == every nbhs is a principal filter *) -(* discrete_space dscT == the discrete topology on T, provided *) -(* a (dscT : discrete_space T) *) (* dense S == the set (S : set T) is dense in T, with T of *) (* type topologicalType *) (* continuousType == type of continuous functions *) (* The HB structures is Continuous. *) (* mkcts f_cts == object of type continuousType corresponding to *) (* the function f (f_cts : continuous f) *) +(* *) (* ``` *) (* ### Factories *) (* ``` *) @@ -908,42 +906,6 @@ Proof. by rewrite -interiorC interiorEbigcup. Qed. #[deprecated(since="mathcomp-analysis 1.7.0", note="use `interiorC` and `interiorEbigcup` instead")] Notation closureC := closureC_deprecated (only parsing). -Section DiscreteTopology. -Section DiscreteMixin. -Context {X : Type}. - -Lemma discrete_sing (p : X) (A : set X) : principal_filter p A -> A p. -Proof. by move=> /principal_filterP. Qed. - -Lemma discrete_nbhs (p : X) (A : set X) : - principal_filter p A -> principal_filter p (principal_filter^~ A). -Proof. by move=> ?; exact/principal_filterP. Qed. - -End DiscreteMixin. - -Definition discrete_space (X : nbhsType) := @nbhs X _ = @principal_filter X. - -Context {X : topologicalType} {dsc : discrete_space X}. - -Lemma discrete_open (A : set X) : open A. -Proof. -by rewrite openE => ? ?; rewrite /interior dsc; exact/principal_filterP. -Qed. - -Lemma discrete_set1 (x : X) : nbhs x [set x]. -Proof. by apply: open_nbhs_nbhs; split => //; exact: discrete_open. Qed. - -Lemma discrete_closed (A : set X) : closed A. -Proof. by rewrite -[A]setCK closedC; exact: discrete_open. Qed. - -Lemma discrete_cvg (F : set_system X) (x : X) : - Filter F -> F --> x <-> F [set x]. -Proof. -rewrite dsc nbhs_simpl; split; first by exact. -by move=> Fx U /principal_filterP ?; apply: filterS Fx => ? ->. -Qed. - -End DiscreteTopology. Definition dense (T : topologicalType) (S : set T) := forall (O : set T), O !=set0 -> open O -> O `&` S !=set0. From 2e448c5dbb49efdd7ab6066084f9c1d75c74b5c6 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 10 Jan 2025 22:57:04 +0900 Subject: [PATCH 2/4] doc, trailing spaces --- CHANGELOG_UNRELEASED.md | 114 +------------------ theories/topology_theory/discrete_topology.v | 68 +++++++---- 2 files changed, 47 insertions(+), 135 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index e319ca1fa..115de956b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,105 +14,6 @@ + lemmas `horner0_ext`, `hornerD_ext`, `horner_scale_ext`, `hornerC_ext`, `derivable_horner`, `derivE`, `continuous_horner` + instance `is_derive_poly` -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals` - with files - + `xfinmap.v` - + `discrete.v` - + `realseq.v` - + `realsum.v` - + `distr.v` - -- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals` - with file - + `Rstruct.v` - -- package `coq-mathcomp-analysis-stdlib` depending on - `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files - + `Rstruct_topology.v` - + `showcase/uniform_bigO.v` - -- in file `separation_axioms.v`, - + new lemmas `compact_normal_local`, and `compact_normal`. - -- in file `topology_theory/one_point_compactification.v`, - + new definitions `one_point_compactification`, and `one_point_nbhs`. - + new lemmas `one_point_compactification_compact`, - `one_point_compactification_some_nbhs`, - `one_point_compactification_some_continuous`, - `one_point_compactification_open_some`, - `one_point_compactification_weak_topology`, and - `one_point_compactification_hausdorff`. - -- in file `normedtype.v`, - + new definition `type` (in module `completely_regular_uniformity`) - + new lemmas `normal_completely_regular`, - `one_point_compactification_completely_reg`, - `nbhs_one_point_compactification_weakE`, - `locally_compact_completely_regular`, and - `completely_regular_regular`. - + new lemmas `near_in_itvoy`, `near_in_itvNyo` - -- in file `mathcomp_extra.v`, - + 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 `sigT_hausdorff`. - -- in `measure.v`: - + lemma `countable_measurable` -- in `realfun.v`: - + lemma `cvgr_dnbhsP` - + new definitions `prodA`, and `prodAr`. - + new lemmas `prodAK`, `prodArK`, and `swapK`. -- in file `product_topology.v`, - + new lemmas `swap_continuous`, `prodA_continuous`, and - `prodAr_continuous`. - -- file `homotopy_theory/homotopy.v` -- file `homotopy_theory/wedge_sigT.v` -- in file `homotopy_theory/wedge_sigT.v` - + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. - + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, - `wedge_liftE`, `wedge_openP`, - `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, - `wedge_compact`, `wedge_connected`. - -- in `boolp.`: - + lemma `existT_inj` -- in file `order_topology.v` - + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and - `max_fun_continuous`. - -- in file `bool_topology.v`, - + new lemma `bool_compact`. - -### Changed - -- in file `normedtype.v`, - changed `completely_regular_space` to depend on uniform separators - which removes the dependency on `R`. The old formulation can be - recovered easily with `uniform_separatorP`. - -- moved from `Rstruct.v` to `Rstruct_topology.v` - + lemmas `continuity_pt_nbhs`, `continuity_pt_cvg`, - `continuity_ptE`, `continuity_pt_cvg'`, `continuity_pt_dnbhs` - and `nbhs_pt_comp` - -- moved from `real_interval.v` to `normedtype.v` - + lemmas `set_itvK`, `RhullT`, `RhullK`, `set_itv_setT`, - `Rhull_smallest`, `le_Rhull`, `neitv_Rhull`, `Rhull_involutive`, - `disj_itv_Rhull` -- in `topology.v`: - + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`, - `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned - into local `Let`'s - in `lebesgue_integral.v`: + lemmas `integral_fin_num_abs`, `Rintegral_cst`, `le_Rintegral` @@ -129,6 +30,9 @@ - in `classical_sets.v`: + lemmas `xsectionE`, `ysectionE` +- in file `bool_topology.v`, + + new lemma `bool_compact`. + ### Changed - in `lebesgue_integrale.v` @@ -142,12 +46,12 @@ - moved from `lebesgue_integral.v` to `measure.v` and generalized + lemmas `measurable_xsection`, `measurable_ysection` + - moved from `topology_structure.v` to `discrete_topology.v`: `discrete_open`, `discrete_set1`, `discrete_closed`, and `discrete_cvg`. - moved from `pseudometric_structure.v` to `discrete_topology.v`: `discrete_ent`, `discrete_ball`, and `discrete_topology`. - - in file `cantor.v`, `cantor_space` now defined in terms of `bool`. - in file `separation_axioms.v`, updated `discrete_hausdorff`, and `discrete_zero_dimension` to take a `discreteTopologicalType`. @@ -184,17 +88,7 @@ - in `sequences.v`: + notations `nneseries_pred0`, `eq_nneseries`, `nneseries0`, `ereal_cvgPpinfty`, `ereal_cvgPninfty` (were deprecated since 0.6.0) -- in `lebesgue_integral.v`: - + definition `cst_mfun` - + lemma `mfun_cst` - -- in `cardinality.v`: - + lemma `cst_fimfun_subproof` -- in `lebesgue_integral.v`: - + lemma `cst_mfun_subproof` (use lemma `measurable_cst` instead) - + lemma `cst_nnfun_subproof` (turned into a `Let`) - + lemma `indic_mfun_subproof` (use lemma `measurable_fun_indic` instead) - in file `topology_structure.v`, removed `discrete_sing`, `discrete_nbhs`, and `discrete_space`. - in file `nat_topology.v`, removed `discrete_nat`. - in file `pseudometric_structure.v`, removed `discrete_ball_center`, `discrete_topology_type`, and diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 94e837eb8..0a4838b12 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -3,12 +3,30 @@ From mathcomp Require Import all_ssreflect all_algebra all_classical all_reals. From mathcomp Require Import topology_structure uniform_structure. From mathcomp Require Import order_topology pseudometric_structure compact. +(**md**************************************************************************) +(* # Discrete Topology *) +(* ``` *) +(* discreteNbhsType == neighborhoods are principal filters *) +(* discrete_ent == entourages of the discrete uniformity *) +(* topology, equipped with the Uniform *) +(* structure *) +(* discrete_ball == singleton balls for the discrete metric, *) +(* equipped with the Uniform structure *) +(* discreteTopologicalType == types with a discrete topology *) +(* discreteOrderTopologicalType == *) +(* pdiscreteTopologicalType == *) +(* pdiscreteOrderTopologicalType == *) +(* discreteUniformType == *) +(* discretePseudoMetricType == *) +(* discrete_topology T == alias attaching discrete structures for *) +(* topology, uniformity, and pseudometric *) +(* ``` *) +(******************************************************************************) Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope classical_set_scope. Local Open Scope ring_scope. - HB.mixin Record Discrete_ofNbhs T of Nbhs T := { nbhs_principalE : (@nbhs T _) = principal_filter; }. @@ -16,45 +34,45 @@ HB.mixin Record Discrete_ofNbhs T of Nbhs T := { #[short(type="discreteNbhsType")] HB.structure Definition DiscreteNbhs := {T of Nbhs T & Discrete_ofNbhs T}. - Definition discrete_ent {T} : set (set (T * T)) := globally (range (fun x => (x, x))). -(** Note: having the discrete topology does not guarantee the discrete +(** Note: having the discrete topology does not guarantee the discrete uniformity. Likewise for the discrete metric. Consider [set 1/n | n in R] *) HB.mixin Record Discrete_ofUniform T of Uniform T := { uniform_discrete : @entourage T = discrete_ent }. -Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := x = y. +Definition discrete_ball {R : numDomainType} {T} (x : T) (eps : R) y : Prop := + x = y. -HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of +HB.mixin Record Discrete_ofPseudometric {R : numDomainType} T of PseudoMetric R T := { metric_discrete : @ball R T = @discrete_ball R T }. #[short(type="discreteTopologicalType")] -HB.structure Definition DiscreteTopology := +HB.structure Definition DiscreteTopology := { T of DiscreteNbhs T & Topological T}. #[short(type="discreteOrderTopologicalType")] -HB.structure Definition DiscreteOrderTopology d := +HB.structure Definition DiscreteOrderTopology d := { T of Discrete_ofNbhs T & OrderTopological d T}. #[short(type="pdiscreteTopologicalType")] -HB.structure Definition PointedDiscreteTopology := +HB.structure Definition PointedDiscreteTopology := { T of DiscreteTopology T & Pointed T}. #[short(type="pdiscreteOrderTopologicalType")] -HB.structure Definition PointedDiscreteOrderTopology d := +HB.structure Definition PointedDiscreteOrderTopology d := { T of Discrete_ofNbhs T & OrderTopological d T & Pointed T}. #[short(type="discreteUniformType")] -HB.structure Definition DiscreteUniform := +HB.structure Definition DiscreteUniform := { T of Discrete_ofUniform T & Uniform T & Discrete_ofNbhs T}. #[short(type="discretePseudoMetricType")] -HB.structure Definition DiscretePseudoMetric {R : numDomainType} := +HB.structure Definition DiscretePseudoMetric {R : numDomainType} := { T of Discrete_ofPseudometric R T & PseudoMetric R T & DiscreteUniform T}. HB.builders Context T of Discrete_ofNbhs T. @@ -65,7 +83,8 @@ Proof. rewrite nbhs_principalE; exact: principal_filter_proper. Qed. Local Lemma principal_nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p. Proof. by rewrite nbhs_principalE => /principal_filterP. Qed. -Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : nbhs p A -> nbhs p (nbhs^~ A). +Local Lemma principal_nbhs_nbhs (p : T) (A : set T) : + nbhs p A -> nbhs p (nbhs^~ A). Proof. by move=> ?; rewrite {1}nbhs_principalE; apply/principal_filterP. Qed. HB.instance Definition _ := @Nbhs_isNbhsTopological.Build T @@ -101,16 +120,16 @@ Qed. Local Lemma discrete_entourage_nbhsE : (@nbhs T _) = nbhs_ d. Proof. rewrite funeqE => x; rewrite nbhs_principalE eqEsubset; split => U. - move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. + move/principal_filterP => ?; exists diagonal; first by move=> ? [w _ <-]. by move=> z /= /set_mem; rewrite /diagonal /= => <-. case => w entW wU; apply/principal_filterP; apply: wU; apply/mem_set. exact: entW. Qed. HB.instance Definition _ := @Nbhs_isUniform.Build T - discrete_ent - discrete_entourage_filter - discrete_entourage_diagonal + discrete_ent + discrete_entourage_filter + discrete_entourage_diagonal discrete_entourage_inv discrete_entourage_split_ex discrete_entourage_nbhsE. @@ -119,12 +138,12 @@ HB.instance Definition _ := @Discrete_ofUniform.Build T erefl. HB.end. -HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of +HB.factory Record DiscretePseudoMetric_ofUniform (R : numDomainType) T of DiscreteUniform T := {}. HB.builders Context R T of DiscretePseudoMetric_ofUniform R T. -Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> +Local Lemma discrete_ball_center x (eps : R) : 0 < eps -> @discrete_ball R T x eps x. Proof. by []. Qed. @@ -143,9 +162,9 @@ move=> entP; exists 1 => //= z z12; apply: entP; exists z.1 => //. by rewrite {2}z12 -surjective_pairing. Qed. -HB.instance Definition _ := - @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) - discrete_ball_center discrete_ball_sym discrete_ball_triangle +HB.instance Definition _ := + @Uniform_isPseudoMetric.Build R T (@discrete_ball R T) + discrete_ball_center discrete_ball_sym discrete_ball_triangle discrete_entourageE. Local Lemma discrete_ballE : @ball R T = @discrete_ball R T. @@ -155,9 +174,8 @@ HB.instance Definition _ := @Discrete_ofPseudometric.Build R T discrete_ballE. HB.end. -(** we introducing an alias attaching discrete structures for - topology, uniformity, and pseudometric *) Definition discrete_topology (T : Type) : Type := T. + HB.instance Definition _ (T : choiceType) := Choice.copy (discrete_topology T) T. HB.instance Definition _ (T : pointedType) := @@ -166,9 +184,9 @@ HB.instance Definition _ (T : choiceType) := hasNbhs.Build (discrete_topology T) principal_filter. HB.instance Definition _ (T : choiceType) := Discrete_ofNbhs.Build (discrete_topology T) erefl. -HB.instance Definition _ (T : choiceType) := +HB.instance Definition _ (T : choiceType) := DiscreteUniform_ofNbhs.Build (discrete_topology T). -HB.instance Definition _ {R : numDomainType} (T : choiceType) := +HB.instance Definition _ {R : numDomainType} (T : choiceType) := @DiscretePseudoMetric_ofUniform.Build R (discrete_topology T). Section discrete_topology. From a8f6198cc805753e236e20cedabee95a1c1d6239 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 10 Jan 2025 23:20:59 +0900 Subject: [PATCH 3/4] bool_compact is not a new lemma --- CHANGELOG_UNRELEASED.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 115de956b..279916694 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -30,9 +30,6 @@ - in `classical_sets.v`: + lemmas `xsectionE`, `ysectionE` -- in file `bool_topology.v`, - + new lemma `bool_compact`. - ### Changed - in `lebesgue_integrale.v` From 559b1c172708fc4e46fc0704cb78841a487508f4 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 10 Jan 2025 16:41:31 -0500 Subject: [PATCH 4/4] adding docs --- theories/topology_theory/discrete_topology.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/theories/topology_theory/discrete_topology.v b/theories/topology_theory/discrete_topology.v index 0a4838b12..9884875d0 100644 --- a/theories/topology_theory/discrete_topology.v +++ b/theories/topology_theory/discrete_topology.v @@ -13,11 +13,13 @@ From mathcomp Require Import order_topology pseudometric_structure compact. (* discrete_ball == singleton balls for the discrete metric, *) (* equipped with the Uniform structure *) (* discreteTopologicalType == types with a discrete topology *) -(* discreteOrderTopologicalType == *) -(* pdiscreteTopologicalType == *) -(* pdiscreteOrderTopologicalType == *) -(* discreteUniformType == *) -(* discretePseudoMetricType == *) +(* discreteOrderTopologicalType == an order type with the discrete topology *) +(* pdiscreteTopologicalType == pointed type with the discrete topology *) +(* pdiscreteOrderTopologicalType == pointed, ordered, and discrete *) +(* discreteUniformType == a uniform space where the diagonal is an *) +(* entourage *) +(* discretePseudoMetricType == a pseudometric space where the only balls *) +(* are singletons *) (* discrete_topology T == alias attaching discrete structures for *) (* topology, uniformity, and pseudometric *) (* ``` *)