diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 5d586a362..e40c77f37 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -136,12 +136,7 @@ From mathcomp Require Import mathcomp_extra boolp. (* ``` *) (* pointedType == interface type for types equipped with a *) (* canonical inhabitant *) -(* PointedType T m == packs the term m : T to build a *) -(* pointedType; T must have a choiceType *) -(* structure *) -(* [pointedType of T for cT] == T-clone of the pointedType structure cT *) -(* [pointedType of T] == clone of a canonical pointedType structure *) -(* on T *) +(* The HB class is Pointed. *) (* point == canonical inhabitant of a pointedType *) (* get P == point x in P if it exists, point otherwise *) (* P must be a set on a pointedType. *) diff --git a/theories/normedtype.v b/theories/normedtype.v index b3e4686da..462bf0a3e 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -25,11 +25,7 @@ Require Import ereal reals signed topology prodnormedzmodule. (* ``` *) (* pseudoMetricNormedZmodType R == interface type for a normed topological *) (* Abelian group equipped with a norm *) -(* PseudoMetricNormedZmodule.Mixin nb == builds the mixin for a normed *) -(* topological Abelian group from the *) -(* compatibility between the norm and *) -(* balls; the carrier type must have a *) -(* normed Zmodule over a numDomainType. *) +(* The HB class is PseudoMetricNormedZmod. *) (* ``` *) (* *) (* lower_semicontinuous f == the extented real-valued function f is *) @@ -40,31 +36,20 @@ Require Import ereal reals signed topology prodnormedzmodule. (* ## Normed modules *) (* ``` *) (* normedModType K == interface type for a normed module *) -(* structure over the numDomainType K. *) -(* NormedModMixin normZ == builds the mixin for a normed module *) -(* from the property of the linearity of *) -(* the norm; the carrier type must have a *) -(* pseudoMetricNormedZmodType structure *) -(* NormedModType K T m == packs the mixin m to build a *) -(* normedModType K; T must have canonical *) -(* pseudoMetricNormedZmodType K and *) -(* pseudoMetricType structures. *) -(* [normedModType K of T for cT] == T-clone of the normedModType K structure *) -(* cT. *) -(* [normedModType K of T] == clone of a canonical normedModType K *) -(* structure on T. *) -(* `|x| == the norm of x (notation from ssrnum). *) +(* structure over the numDomainType K *) +(* The HB class is NormedModule. *) +(* `|x| == the norm of x (notation from ssrnum) *) (* ball_norm == balls defined by the norm. *) (* edist == the extended distance function for a *) -(* pseudometric X, from X*X -> \bar R *) +(* pseudometric X, from X * X -> \bar R *) (* edist_inf A == the infimum of distances to the set A *) (* Urysohn A B == a continuous function T -> [0,1] which *) (* separates A and B when *) (* `uniform_separator A B` *) -(* uniform_separator A B == There is a suitable uniform space and *) +(* uniform_separator A B == there is a suitable uniform space and *) (* entourage separating A and B *) -(* nbhs_norm == neighborhoods defined by the norm. *) -(* closed_ball == closure of a ball. *) +(* nbhs_norm == neighborhoods defined by the norm *) +(* closed_ball == closure of a ball *) (* f @`[ a , b ], f @`] a , b [ == notations for images of intervals, *) (* intended for continuous, monotonous *) (* functions, defined in ring_scope and *) @@ -83,10 +68,10 @@ Require Import ereal reals signed topology prodnormedzmodule. (* bounded_near f F == f is bounded near F *) (* [bounded f x | x in A] == f is bounded on A, ie F := globally A *) (* [locally [bounded f x | x in A] == f is locally bounded on A *) -(* bounded_set == set of bounded sets. *) +(* bounded_set == set of bounded sets *) (* := [set A | [bounded x | x in A]] *) (* bounded_fun == set of functions bounded on their *) -(* whole domain. *) +(* whole domain *) (* := [set f | [bounded f x | x in setT]] *) (* lipschitz_on f F == f is lipschitz near F *) (* [lipschitz f x | x in A] == f is lipschitz on A *) @@ -110,14 +95,13 @@ Require Import ereal reals signed topology prodnormedzmodule. (* ``` *) (* completeNormedModType K == interface type for a complete normed *) (* module structure over a realFieldType *) -(* K. *) -(* [completeNormedModType K of T] == clone of a canonical complete normed *) -(* module structure over K on T. *) +(* K *) +(* The HB class is CompleteNormedModule. *) (* ``` *) (* *) (* ## Filters *) (* ``` *) -(* at_left x, at_right x == filters on real numbers for predicates *) +(* x^'-, x^'+ == filters on real numbers for predicates *) (* s.t. nbhs holds on the left/right of x *) (* ``` *) (* *) @@ -2154,7 +2138,7 @@ Proof. by move=> cf /cvg_eq->// e; rewrite subrr normr0. Qed. note="simply use the fact that `(x --> l) -> (x = l)`")] Notation continuous_cvg_dist := __deprecated__continuous_cvg_dist (only parsing). -(** Matrices: *) +(** Matrices *) Section mx_norm. Variables (K : numDomainType) (m n : nat). Implicit Types x y : 'M[K]_(m, n). @@ -2270,7 +2254,7 @@ HB.instance Definition _ := End matrix_NormedModule. -(** Pairs: *) +(** Pairs *) Section prod_PseudoMetricNormedZmodule. Context {K : numDomainType} {U V : pseudoMetricNormedZmodType K}. @@ -2307,10 +2291,10 @@ Variables (K : numDomainType). Example matrix_triangke m n (M N : 'M[K]_(m.+1, n.+1)) : `|M + N| <= `|M| + `|N|. -Proof. apply ler_normD. Qed. +Proof. exact: ler_normD. Qed. Example pair_triangle (x y : K * K) : `|x + y| <= `|x| + `|y|. -Proof. apply ler_normD. Qed. +Proof. exact: ler_normD. Qed. End example_of_sharing. @@ -3910,7 +3894,7 @@ Unshelve. all: by end_near. Qed. End closure_left_right_open. -(** ** Complete Normed Modules *) +(** Complete Normed Modules *) #[short(type="completeNormedModType")] HB.structure Definition CompleteNormedModule (K : numFieldType) := diff --git a/theories/reals.v b/theories/reals.v index 79e403811..e58b47883 100644 --- a/theories/reals.v +++ b/theories/reals.v @@ -14,6 +14,7 @@ (* *) (* ``` *) (* realType == type of real numbers *) +(* The HB class is Real. *) (* sup A == where A : set R with R : realType, the supremum of A when *) (* it exists, 0 otherwise *) (* inf A := - sup (- A) *) diff --git a/theories/topology.v b/theories/topology.v index 4dd1ea122..03a6ed3ec 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -50,42 +50,26 @@ Require Import reals signed. (* elements represent sets of sets on U. *) (* These sets are intended to be filters *) (* on U but this is not enforced yet. *) -(* FilteredType U T m == packs the function m: T -> set (set U) *) -(* to build a filtered type of type *) -(* filteredType U *) -(* T must have a pointedType structure. *) -(* [filteredType U of T for cT] == T-clone of the filteredType U *) -(* structure cT *) -(* [filteredType U of T] == clone of a canonical structure of *) -(* filteredType U on T *) -(* Filtered.source Y Z == structure that records types X such *) -(* that there is a function mapping *) -(* functions of type X -> Y to filters on *) -(* Z *) -(* Allows to infer the canonical filter *) -(* associated to a function by looking *) -(* looking at its source type. *) -(* Filtered.Source F == if F : (X -> Y) -> set (set Z), packs *) -(* X with F in a Filtered.source Y Z *) -(* structure *) +(* The HB class is called Filtered. *) +(* It extends Pointed. *) +(* nbhs p == set of sets associated to p (in a *) +(* filtered type) *) +(* hasNbhs == factory for filteredType *) (* ``` *) (* *) (* We endow several standard types with the structure of filter, e.g.: *) -(* - products: filtered_prod *) -(* - matrices: matrix_filtered *) -(* - natural numbers: nat_filteredType *) +(* - products `(X1 * X2)%type` *) +(* - matrices `'M[X]_(m, n)` *) +(* - natural numbers `nat` *) (* *) (* ## Theory of filters *) (* ``` *) -(* nbhs p == set of sets associated to p (in a *) -(* filtered type) *) (* filter_from D B == set of the supersets of the elements *) (* of the family of sets B whose indices *) (* are in the domain D *) (* This is a filter if (B_i)_(i in D) *) (* forms a filter base. *) (* filter_prod F G == product of the filters F and G *) -(* [filter of x] == canonical filter associated to x *) (* F `=>` G <-> G is included in F *) (* F and G are sets of sets. *) (* F --> G <-> the canonical filter associated to G *) @@ -210,20 +194,8 @@ Require Import reals signed. (* ### Topology *) (* ``` *) (* topologicalType == interface type for topological space *) -(* structure. *) -(* TopologicalType T m == packs the mixin m to build a *) -(* topologicalType *) -(* T must have a canonical structure of *) -(* filteredType T. *) -(* TopologicalMixin nbhs_filt nbhsE == builds the mixin for a topological *) -(* space from the proofs that nbhs *) -(* outputs proper filters and defines the *) -(* same notion of neighbourhood as the *) -(* open sets. *) -(* [topologicalType of T for cT] == T-clone of the topologicalType *) -(* structure cT *) -(* [topologicalType of T] == clone of a canonical structure of *) -(* topologicalType on T *) +(* structure *) +(* the HB class is Topological. *) (* open == set of open sets *) (* open_nbhs p == set of open neighbourhoods of p *) (* basis B == a family of open sets that converges *) @@ -232,50 +204,49 @@ Require Import reals signed. (* continuous f <-> f is continuous w.r.t the topology *) (* [locally P] := forall a, A a -> G (within A (nbhs x)) *) (* if P is convertible to G (globally A) *) -(* topologyOfFilterMixin nbhs_filt nbhs_sing nbhs_nbhs == topology defined by *) -(* a filter *) +(* Nbhs_isNbhsTopological == factory for a topology defined by a *) +(* filter *) (* It builds the mixin for a topological *) (* space from the properties of nbhs and *) (* hence assumes that the carrier is a *) (* filterType. *) -(* topologyOfOpenMixin opT opI op_bigU == topology defined by open sets *) +(* Pointed_isOpenTopological == factory for a topology defined by open *) +(* sets *) (* It builds the mixin for a topological *) (* space from the properties of open *) (* sets, assuming the carrier is a *) (* pointed type. nbhs_of_open must be *) (* used to declare a filterType. *) -(* topologyOfBaseMixin b_cover b_join == topology defined by a base of open *) -(* sets *) +(* Pointed_isBaseTopological == factory for a topology defined by a *) +(* base of open sets *) (* It builds the mixin for a topological *) (* space from the properties of a base of *) (* open sets; the type of indices must be *) (* a pointedType, as well as the carrier. *) -(* nbhs_of_open \o open_from must be *) -(* used to declare a filterType. *) (* filterI_iter F n == nth stage of recursively building the *) (* filter of finite intersections of F *) (* finI_from D f == set of \bigcap_(i in E) f i where E is *) (* a finite subset of D *) -(* topologyOfSubbaseMixin D b == topology defined by a subbase of open *) -(* sets *) +(* Pointed_isSubBaseTopological == factory for a topology defined by a *) +(* subbase of open sets *) (* It builds the mixin for a topological *) (* space from a subbase of open sets b *) (* indexed on domain D; the type of *) (* indices must be a pointedType. *) (* *) (* We endow several standard types with the structure of topology, e.g.: *) -(* - products: prod_topologicalType *) -(* - matrices: matrix_topologicalType *) -(* - natural numbers: nat_topologicalType *) +(* - products `(T * U)%type` *) +(* - matrices `'M[T]_(m, n)` *) +(* - natural numbers `nat` *) (* *) -(* weak_topologicalType f == weak topology by a function f : S -> T *) +(* weak_topology f == weak topology by a function f : S -> T *) (* on S *) (* S must be a pointedType and T a *) (* topologicalType. *) -(* sup_topologicalType Tc == supremum topology of the family of *) +(* sup_topology Tc == supremum topology of the family of *) (* topologicalType structures Tc on T *) (* T must be a pointedType. *) -(* product_topologicalType T == product topology of the family of *) +(* prod_topology T == product topology of the family of *) (* topologicalTypes T. *) (* quotient_topology Q == the quotient topology corresponding to *) (* quotient Q : quotType T. where T has *) @@ -330,19 +301,10 @@ Require Import reals signed. (* nbhs_ ent == neighbourhoods defined using entourages *) (* uniformType == interface type for uniform spaces: a *) (* type equipped with entourages *) -(* UniformMixin efilter erefl einv esplit nbhse == builds the mixin for a *) -(* uniform space from the properties of *) -(* entourages and the compatibility between *) -(* entourages and nbhs *) -(* UniformType T m == packs the uniform space mixin into a *) -(* uniformType. T must have a canonical *) -(* structure of topologicalType *) -(* [uniformType of T for cT] == T-clone of the uniformType structure cT *) -(* [uniformType of T] == clone of a canonical structure of *) -(* uniformType on T *) -(* topologyOfEntourageMixin umixin == builds the mixin for a topological *) -(* space from a mixin for a uniform space *) +(* The HB class is Uniform. *) (* entourage == set of entourages in a uniform space *) +(* Nbhs_isUniform == factory to build a topological space *) +(* from a mixin for a uniform space *) (* split_ent E == when E is an entourage, split_ent E is *) (* an entourage E' such that E' \o E' is *) (* included in E when seen as a relation *) @@ -351,36 +313,23 @@ Require Import reals signed. (* metrizable. *) (* unif_continuous f <-> f is uniformly continuous *) (* entourage_ ball == entourages defined using balls *) -(* weak_uniformType == the uniform space for weak topologies *) -(* sup_uniformType == the uniform space for sup topologies *) -(* discrete_ent == entourages for the discrete topology *) (* ``` *) (* *) +(* `weak_topology`, `sup_ent`, `discrete_ent` are equipped with the `Uniform` *) +(* structure. *) (* We endow several standard types with the structure of uniform space, e.g.: *) -(* - products: prod_uniformType *) -(* - matrices: matrix_uniformType *) +(* - products `(U * V)%type` *) +(* - matrices `'M[T]_(m, n)` *) (* *) (* ### PseudoMetric spaces *) (* ``` *) (* entourage_ ball == entourages defined using balls *) (* pseudoMetricType == interface type for pseudo metric space *) (* structure: a type equipped with balls *) -(* PseudoMetricMixin brefl bsym btriangle nbhsb == builds the mixin for a *) -(* pseudo metric space from the properties *) -(* of balls and the compatibility between *) -(* balls and entourages *) -(* PseudoMetricType T m == packs the pseudo metric space mixin into *) -(* a pseudoMetricType *) -(* T must have a canonical structure of *) -(* uniformType. *) -(* [pseudoMetricType R of T for cT] == T-clone of the pseudoMetricType *) -(* structure cT, with R the ball radius *) -(* [pseudoMetricType R of T] == clone of a canonical structure of *) -(* pseudoMetricType on T, with R the ball *) -(* radius *) -(* uniformityOfBallMixin umixin == builds the mixin for a topological space *) -(* from a mixin for a pseudoMetric space. *) +(* The HB class is PseudoMetric. *) (* ball x e == ball of center x and radius e. *) +(* Nbhs_isPseudoMetric == factory to build a topological space *) +(* from a mixin for a pseudoMetric space *) (* nbhs_ball_ ball == nbhs defined using the given balls *) (* nbhs_ball == nbhs defined using balls in a *) (* pseudometric space *) @@ -390,10 +339,10 @@ Require Import reals signed. (* *) (* We endow several standard types with the structure of pseudometric space, *) (* e.g.: *) -(* - products: prod_pseudoMetricType *) -(* - matrices: matrix_pseudoMetricType *) -(* - weak_pseudoMetricType (the metric space for weak topologies) *) -(* - sup_pseudoMetricType *) +(* - products `(U * V)%type` *) +(* - matrices `'M[T]_(m, n)` *) +(* - `weak_topology` (the metric space for weak topologies) *) +(* - `sup_pseudoMetricType` *) (* *) (* ### Complete uniform spaces *) (* ``` *) @@ -401,21 +350,13 @@ Require Import reals signed. (* (entourage definition) *) (* completeType == interface type for a complete uniform *) (* space structure *) -(* CompleteType T cvgCauchy == packs the proof that every proper cauchy *) -(* filter on T converges into a *) -(* completeType structure *) -(* T must have a canonical structure of *) -(* uniformType. *) -(* [completeType of T for cT] == T-clone of the completeType structure *) -(* cT *) -(* [completeType of T] == clone of a canonical structure of *) -(* completeType on T *) +(* The HB class is Complete. *) (* ``` *) (* *) (* We endow several standard types with the structure of complete uniform *) (* space, e.g.: *) -(* - matrices: matrix_completeType *) -(* - functions: fun_completeType *) +(* - matrices `'M[T]_(m, n)` *) +(* - functions `T -> U` *) (* *) (* ### Complete pseudometric spaces *) (* ``` *) @@ -425,30 +366,18 @@ Require Import reals signed. (* (using the near notations) *) (* completePseudoMetricType == interface type for a complete *) (* pseudometric space structure *) -(* CompletePseudoMetricType T cvgCauchy == packs the proof that every proper *) -(* cauchy filter on T converges into a *) -(* completePseudoMetricType structure *) -(* T must have a canonical structure of *) -(* pseudoMetricType. *) -(* [completePseudoMetricType of T for cT] == T-clone of the *) -(* completePseudoMetricType structure cT. *) -(* [completePseudoMetricType of T] == clone of a canonical structure of *) -(* completePseudoMetricType on T. *) +(* The HB class is CompletePseudoMetric. *) (* ball_ N == balls defined by the norm/absolute *) (* value N *) (* ``` *) (* *) (* We endow several standard types with the structure of complete *) (* pseudometric space, e.g.: *) -(* - matrices: matrix_completePseudoMetricType *) -(* - functions: fct_completePseudoMetricType *) +(* - matrices `'M[T]_(m, n)` *) +(* - functions `T -> U` *) (* *) -(* We endow numFieldType with the types of topological notions *) -(* (accessible with "Import numFieldTopology.Exports."): *) -(* - numField_filteredType *) -(* - numField_topologicalType *) -(* - numField_uniformType *) -(* - numField_pseudoMetricType *) +(* We endow `numFieldType` with the types of topological notions *) +(* (accessible with `Import numFieldTopology.Exports.`) *) (* *) (* ### Function space topologies *) (* ``` *) @@ -474,7 +403,6 @@ Require Import reals signed. (* *) (* dense S == the set (S : set T) is dense in T, with T of *) (* type topologicalType *) -(* weak_pseudoMetricType == the metric space for weak topologies *) (* ``` *) (* *) (* ### Subspaces of topological spaces *) @@ -495,8 +423,7 @@ Require Import reals signed. (* includes `iter n split_ent E` *) (* Critically, `gauge E` forms a uniform space *) (* with a countable uniformity. *) -(* gauge_pseudoMetricType E == the pseudoMetricType associated with the *) -(* `gauge E` *) +(* gauge.type is endowed with a pseudoMetricType *) (* normal_space X == X is normal (sometimes called T4) *) (* regular_space X == X is regular (sometimes called T3) *) (* equicontinuous W x == the set (W : X -> Y) is equicontinuous at x *) @@ -694,7 +621,7 @@ HB.end. HB.structure Definition Nbhs := {T of Pointed T & hasNbhs T}. Definition filter_from {I T : Type} (D : set I) (B : I -> set T) : - set_system T := [set P | exists2 i, D i & B i `<=` P]. + set_system T := [set P | exists2 i, D i & B i `<=` P]. (* the canonical filter on matrices on X is the product of the canonical filter on X *) @@ -2085,7 +2012,6 @@ Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). (** Topology defined by a filter *) -(* was topologyOfFilterMixin *) HB.factory Record Nbhs_isNbhsTopological T of Nbhs T := { nbhs_filter : forall p : T, ProperFilter (nbhs p); nbhs_singleton : forall (p : T) (A : set T), nbhs p A -> A p; @@ -2119,7 +2045,6 @@ HB.end. Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) := exists B, [/\ op B, B p & B `<=` A]. -(* was topologyOfOpenMixin *) HB.factory Record Pointed_isOpenTopological T of Pointed T := { op : set T -> Prop; opT : op setT; @@ -2165,7 +2090,6 @@ HB.end. (** Topology defined by a base of open sets *) -(* was topologyOfBaseMixin *) HB.factory Record Pointed_isBaseTopological T of Pointed T := { I : pointedType; D : set I; @@ -2332,7 +2256,6 @@ Proof. by rewrite filterI_iter_finI filterI_iterE. Qed. End filter_supremums. -(* was TopologyOfSubbase *) HB.factory Record Pointed_isSubBaseTopological T of Pointed T := { I : pointedType; D : set I; @@ -3361,8 +3284,8 @@ Lemma bigsetU_compact I (F : I -> set X) (s : seq I) (P : pred I) : compact (\big[setU/set0]_(i <- s | P i) F i). Proof. by move=> ?; elim/big_ind : _ =>//; [exact:compact0|exact:compactU]. Qed. -(* The closed condition here is neccessary to make this definition work in a *) -(* non-hausdorff setting. *) +(** The closed condition here is neccessary to make this definition work in a + non-hausdorff setting. *) Definition compact_near (F : set_system X) := exists2 U, F U & compact U /\ closed U. @@ -4084,7 +4007,7 @@ End DiscreteMixin. Definition discrete_space (X : nbhsType) := @nbhs X _ = @principal_filter X. -Context {X : topologicalType} {dsc: discrete_space X}. +Context {X : topologicalType} {dsc : discrete_space X}. Lemma discrete_open (A : set X) : open A. Proof. @@ -4981,7 +4904,7 @@ HB.instance Definition _ (I : Type) (T : I -> uniformType) := (sup_topology (fun i => Uniform.class [the uniformType of weak_topology (@proj _ T i)])). -(** * PseudoMetric spaces defined using balls *) +(** PseudoMetric spaces defined using balls *) Definition entourage_ {R : numDomainType} {T T'} (ball : T -> R -> set T') := @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]).