diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 284b09b888..654f9d7303 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -100,6 +100,12 @@ - in `measure.v`: + lemma `sigma_finiteP` generalized to an equivalence and changed to use `[/\ ..., .. & ....]` +- moved from `cantor.v` to `topology.v`: + + lemma `discrete_bool_compact` + + definition `pointed_principal_filter` + + definition `pointed_discrete_topology` + + lemma `discrete_pointed` + ### Renamed - in `constructive_ereal.v`: diff --git a/theories/cantor.v b/theories/cantor.v index 21e0b1b104..017e0fb39a 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -14,8 +14,6 @@ From HB Require Import structures. (* homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff. *) (* *) (* ``` *) -(* pointed_principal_filter == alias for pointed types with principal *) -(* filters *) (* cantor_space == the Cantor space, with its canonical metric *) (* cantor_like T == perfect + compact + hausdroff + zero dimensional *) (* tree_of T == builds a topological tree with levels (T n) *) @@ -45,42 +43,6 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. -(* we start by introducing an alias for pointed types with - principal filters *) -Definition pointed_principal_filter (P : pointedType) : Type := P. -HB.instance Definition _ (P : pointedType) := - Pointed.on (pointed_principal_filter P). -HB.instance Definition _ (P : pointedType) := - hasNbhs.Build (pointed_principal_filter P) principal_filter. - -(* we use `discrete_topology` to equip pointed types - with a discrete topology *) -Section discrete_topology_for_pointed_types. - -Let discrete_pointed_subproof (P : pointedType) : - discrete_space (pointed_principal_filter P). -Proof. by []. Qed. - -Definition pointed_discrete_topology (P : pointedType) : Type := - discrete_topology (discrete_pointed_subproof P). - -End discrete_topology_for_pointed_types. -(* note that in topology.v, we already have: -HB.instance Definition _ := discrete_uniform_mixin. -and -HB.instance Definition _ := discrete_pseudometric_mixin. *) - -(* we need the following proof when using - `discrete_hausdorff` or `discrete_zero_dimension` *) -Lemma discrete_pointed (T : pointedType) : - discrete_space (pointed_discrete_topology T). -Proof. -apply/funext => /= x; apply/funext => A; apply/propext; split. -- by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x. -- move=> h; exists [set x | x.1 = x.2]; first by move=> -[a b] [t _] [<- <-]. - by move=> y /= xy; exact: h. -Qed. - Definition cantor_space := prod_topology (fun _ : nat => discrete_topology discrete_bool). @@ -94,10 +56,6 @@ Definition cantor_like (T : topologicalType) := hausdorff_space T & zero_dimensional T]. -(* TODO: move to topology.v? *) -Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool]. -Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. - Lemma cantor_space_compact : compact [set: cantor_space]. Proof. have := @tychonoff _ (fun _ : nat => _) _ (fun=> discrete_bool_compact). diff --git a/theories/topology.v b/theories/topology.v index 691d1089b2..357fc89f62 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -120,6 +120,8 @@ Require Import reals signed. (* within D F == restriction of the filter F to the *) (* domain D *) (* principal_filter x == filter containing every superset of x *) +(* pointed_principal_filter == alias for pointed types with *) +(* principal filters *) (* subset_filter F D == similar to within D F, but with *) (* dependent types *) (* powerset_filter_from F == the filter of downward closed subsets *) @@ -324,6 +326,8 @@ Require Import reals signed. (* pseudometric space *) (* discrete_ball == singleton balls for the discrete *) (* topology *) +(* pointed_discrete_topology == equip pointed types with a discrete *) +(* topology *) (* ``` *) (* *) (* We endow several standard types with the structure of pseudometric space, *) @@ -1626,6 +1630,13 @@ Section PrincipalFilters. Definition principal_filter {X : Type} (x : X) : set_system X := globally [set x]. +(** we introducing an alias for pointed types with principal filters *) +Definition pointed_principal_filter (P : pointedType) : Type := P. +HB.instance Definition _ (P : pointedType) := + Pointed.on (pointed_principal_filter P). +HB.instance Definition _ (P : pointedType) := + hasNbhs.Build (pointed_principal_filter P) principal_filter. + Lemma principal_filterP {X} (x : X) (W : set X) : principal_filter x W <-> W x. Proof. by split=> [|? ? ->]; [exact|]. Qed. @@ -3841,6 +3852,7 @@ Qed. End connected_sets. Arguments connected {T}. Arguments connected_component {T}. + Section DiscreteTopology. Section DiscreteMixin. Context {X : Type}. @@ -4697,6 +4709,9 @@ HB.instance Definition _ := discrete_uniform_mixin. End discrete_uniform. +Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool]. +Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. + (* was uniformityOfBallMixin *) HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := { ent : set_system (M * M); @@ -5149,6 +5164,33 @@ End discrete_pseudoMetric. Definition pseudoMetric_bool {R : realType} := [the pseudoMetricType R of discrete_topology discrete_bool : Type]. +(** we use `discrete_topology` to equip pointed types with a discrete topology *) +Section discrete_topology_for_pointed_types. + +Let discrete_pointed_subproof (P : pointedType) : + discrete_space (pointed_principal_filter P). +Proof. by []. Qed. + +Definition pointed_discrete_topology (P : pointedType) : Type := + discrete_topology (discrete_pointed_subproof P). + +End discrete_topology_for_pointed_types. +(* note that in topology.v, we already have: +HB.instance Definition _ := discrete_uniform_mixin. +and +HB.instance Definition _ := discrete_pseudometric_mixin. *) + +(** we need the following proof when using + `discrete_hausdorff` or `discrete_zero_dimension` in `cantor.v` *) +Lemma discrete_pointed (T : pointedType) : + discrete_space (pointed_discrete_topology T). +Proof. +apply/funext => /= x; apply/funext => A; apply/propext; split. +- by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x. +- move=> h; exists [set x | x.1 = x.2]; first by move=> -[a b] [t _] [<- <-]. + by move=> y /= xy; exact: h. +Qed. + (** Complete uniform spaces *) Definition cauchy {T : uniformType} (F : set_system T) := (F, F) --> entourage.