From 1fd0e85771cd798bf15a2c5c5b5cbcefedd136b1 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 8 Jan 2024 00:43:49 +0900 Subject: [PATCH] format doc (#1130) * format doc --------- Co-authored-by: Pierre Roux --- CHANGELOG_UNRELEASED.md | 2 + classical/mathcomp_extra.v | 5 + theories/topology.v | 540 +++++++++++++++++++++---------------- 3 files changed, 309 insertions(+), 238 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 68c07cac5..adbff8b22 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -120,6 +120,8 @@ - in `sequences.v`: + change the implicit arguments of `trivIset_seqDU` +- moved from `topology.v` to `mathcomp_extra.v` + + definition `monotonous` ### Renamed diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index e01a9795b..5b67586e5 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -27,6 +27,8 @@ 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) *) +(* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) +(* {in A &, {mono f : x y /~ x <= y}} *) (* *) (******************************************************************************) @@ -929,3 +931,6 @@ exists n.+1; rewrite nm2/= -addn1. rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r. by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l. Qed. + +Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := + {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. diff --git a/theories/topology.v b/theories/topology.v index b55ad5410..8762fa2f2 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -9,282 +9,306 @@ Require Import reals signed. (* Filters and basic topological notions *) (* *) (* This file develops tools for the manipulation of filters and basic *) -(* topological notions. The development of topological notions builds on *) -(* "filtered types". They are types equipped with an interface that *) -(* associates to each element a set of sets, intended to represent a filter. *) -(* The notions of limit and convergence are defined for filtered types and in *) -(* the documentation below we call "canonical filter" of an element the set *) -(* of sets associated to it by the interface of filtered types. *) +(* topological notions. *) +(* The development of topological notions builds on "filtered types". They *) +(* are types equipped with an interface that associates to each element a *) +(* set of sets, intended to represent a filter. The notions of limit and *) +(* convergence are defined for filtered types and in the documentation below *) +(* we call "canonical filter" of an element the set of sets associated to it *) +(* by the interface of filtered types. *) +(* We used these topological notions to prove, e.g., Tychonoff's Theorem, *) +(* which states that any product of compact sets is compact according to the *) +(* product topology or Arzela-Ascoli's theorem. *) (* *) -(* monotonous A f := {in A &, {mono f : x y / x <= y}} \/ *) -(* {in A &, {mono f : x y /~ x <= y}}. *) +(* Table of contents of the documentation: *) +(* 1. Filters *) +(* - Structure of filter *) +(* - Theory of filters *) +(* - Near notations and tactics *) +(* + Notations *) +(* + Tactics *) +(* 2. Basic topological notions *) +(* - Mathematical structures *) +(* + Topology *) +(* + Uniform spaces *) +(* + Pseudometric spaces *) +(* + Complete uniform spaces *) +(* + Complete pseudometric spaces *) +(* + Function space topologies *) +(* + Subspaces of topological spaces *) +(******************************************************************************) + +(******************************************************************************) +(* 1. Filters *) (* *) -(* * Filters : *) +(* * Structure of filter *) (* filteredType U == interface type for types whose *) (* 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 *) +(* T must have a pointedType structure. *) (* [filteredType U of T for cT] == T-clone of the filteredType U *) -(* structure cT. *) +(* structure cT *) (* [filteredType U of T] == clone of a canonical structure of *) -(* filteredType U on T. *) +(* 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 *) +(* 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. *) +(* structure *) +(* *) +(* We endow several standard types with the structure of filter, e.g.: *) +(* - products: filtered_prod *) +(* - matrices: matrix_filtered *) +(* - natural numbers: nat_filteredType *) +(* *) +(* * Theory of filters *) (* nbhs p == set of sets associated to p (in a *) -(* filtered type). *) +(* 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. *) +(* 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. *) +(* 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 *) (* is included in the canonical filter *) -(* associated to F. *) +(* associated to F *) (* lim F == limit of the canonical filter *) (* associated with F if there is such a *) (* limit, i.e., an element l such that *) (* the canonical filter associated to l *) -(* is a subset of F. *) +(* is a subset of F *) (* [lim F in T] == limit of the canonical filter *) (* associated to F in T where T has type *) -(* filteredType U. *) +(* filteredType U *) (* [cvg F in T] <-> the canonical filter associated to F *) -(* converges in T. *) +(* converges in T *) (* cvg F <-> same as [cvg F in T] where T is *) (* inferred from the type of the *) -(* canonical filter associated to F. *) +(* canonical filter associated to F *) (* Filter F == type class proving that the set of *) -(* sets F is a filter. *) +(* sets F is a filter *) (* ProperFilter F == type class proving that the set of *) -(* sets F is a proper filter. *) +(* sets F is a proper filter *) (* UltraFilter F == type class proving that the set of *) (* sets F is an ultrafilter *) (* filter_on T == interface type for sets of sets on T *) -(* that are filters. *) +(* that are filters *) (* FilterType F FF == packs the set of sets F with the proof *) (* FF of Filter F to build a filter_on T *) -(* structure. *) +(* structure *) (* pfilter_on T == interface type for sets of sets on T *) -(* that are proper filters. *) +(* that are proper filters *) (* PFilterPack F FF == packs the set of sets F with the proof *) (* FF of ProperFilter F to build a *) -(* pfilter_on T structure. *) +(* pfilter_on T structure *) (* fmap f F == image of the filter F by the function *) (* f *) -(* E @[x --> F] == image of the canonical filter *) +(* E @[x --> F] == image of the canonical filter *) (* associated to F by the function *) -(* (fun x => E). *) +(* (fun x => E) *) (* f @ F == image of the canonical filter *) -(* associated to F by the function f. *) +(* associated to F by the function f *) (* fmapi f F == image of the filter F by the relation *) (* f *) -(* E `@[x --> F] == image of the canonical filter *) +(* E `@[x --> F] == image of the canonical filter *) (* associated to F by the relation *) -(* (fun x => E). *) +(* (fun x => E) *) (* f `@ F == image of the canonical filter *) -(* associated to F by the relation f. *) -(* globally A == filter of the sets containing A. *) +(* associated to F by the relation f *) +(* globally A == filter of the sets containing A *) (* @frechet_filter T := [set S : set T | finite_set (~` S)] *) (* a.k.a. cofinite filter *) -(* at_point a == filter of the sets containing a. *) +(* at_point a == filter of the sets containing a *) (* within D F == restriction of the filter F to the *) -(* domain D. *) -(* principal_filter x == filter containing every superset of x. *) +(* domain D *) +(* principal_filter x == filter containing every superset of x *) (* subset_filter F D == similar to within D F, but with *) -(* dependent types. *) -(* powerset_filter_from F == The filter of downward closed subsets *) -(* of F. Enables use of near notation to *) -(* pick suitably small members of F *) +(* dependent types *) +(* powerset_filter_from F == the filter of downward closed subsets *) +(* of F. *) +(* Enables use of near notation to pick *) +(* suitably small members of F *) (* in_filter F == interface type for the sets that *) -(* belong to the set of sets F. *) +(* belong to the set of sets F *) (* InFilter FP == packs a set P with a proof of F P to *) -(* build a in_filter F structure. *) +(* build a in_filter F structure *) (* \oo == "eventually" filter on nat: set of *) (* predicates on natural numbers that are *) -(* eventually true. *) +(* eventually true *) (* clopen U == U is both open and closed *) -(* normal_space X == X is normal, sometimes called T4 *) -(* regular_space X == X is regular, sometimes called T3 *) -(* separate_points_from_closed f == For a closed set U and point x outside *) -(* some member of the family f sends *) -(* f_i(x) outside (closure (f_i @` U)). *) -(* Used together with join_product. *) -(* join_product f == The function (x => f ^~ x). When the *) -(* family f separates points from closed *) -(* sets, join_product is an embedding. *) (* *) -(* * Near notations and tactics: *) -(* --> The purpose of the near notations and tactics is to make the *) -(* manipulation of filters easier. Instead of proving F G, one can *) -(* prove G x for x "near F", i.e. for x such that H x for H arbitrarily *) -(* precise as long as F H. The near tactics allow for a delayed *) -(* introduction of H: H is introduced as an existential variable and *) -(* progressively instantiated during the proof process. *) -(* --> Notations: *) +(* * Near notations and tactics *) +(* The purpose of the near notations and tactics is to make the manipulation *) +(* of filters easier. Instead of proving F G, one can prove G x for x *) +(* "near F", i.e., for x such that H x for H arbitrarily precise as long as *) +(* F H. The near tactics allow for a delayed introduction of H: *) +(* H is introduced as an existential variable and progressively instantiated *) +(* during the proof process. *) +(* *) +(* ** Notations *) (* {near F, P} == the property P holds near the *) -(* canonical filter associated to F; P *) -(* must have the form forall x, Q x. *) +(* canonical filter associated to F *) +(* P must have the form forall x, Q x. *) (* Equivalent to F Q. *) (* \forall x \near F, P x <-> F (fun x => P x). *) (* \near x, P x := \forall y \near x, P y. *) (* {near F & G, P} == same as {near H, P}, where H is the *) -(* product of the filters F and G. *) -(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y}. *) -(* \forall x & y \near F, P x y == same as before, with G = F. *) -(* \near x & y, P x y := \forall z \near x & t \near y, P x y. *) -(* x \is_near F == x belongs to a set P : in_filter F. *) -(* --> Tactics: *) -(* - near=> x introduces x: *) -(* On the goal \forall x \near F, G x, introduces the variable x and an *) -(* "existential", and unaccessible hypothesis ?H x and asks the user to *) -(* prove (G x) in this context. *) -(* Under the hood delays the proof of F ?H and waits for near: x *) -(* Also exists under the form near=> x y. *) -(* - near: x discharges x: *) -(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) -(* that (\forall x \near F, H_i x), provided that H_i x does not depend *) -(* on variables introduced after x. *) -(* Under the hood, it refines by intersection the existential variable *) -(* ?H attached to x, computes the intersection with F, and asks the *) -(* user to prove F H_i, right now *) -(* - end_near should be used to close remaining existentials trivially *) -(* - near F => x poses a variable near F, where F is a proper filter *) -(* adds to the context a variable x that \is_near F, i.e. one may *) -(* assume H x for any H in F. This new variable x can be dealt with *) -(* using near: x, as for variables introduced by near=>. *) +(* product of the filters F and G *) +(* \forall x \near F & y \near G, P x y := {near F & G, forall x y, P x y} *) +(* \forall x & y \near F, P x y == same as before, with G = F *) +(* \near x & y, P x y := \forall z \near x & t \near y, P x y *) +(* x \is_near F == x belongs to a set P : in_filter F *) +(* ** Tactics *) +(* - near=> x introduces x: *) +(* On the goal \forall x \near F, G x, introduces the variable x and an *) +(* "existential", and an unaccessible hypothesis ?H x and asks the user to *) +(* prove (G x) in this context. *) +(* Under the hood, it delays the proof of F ?H and waits for near: x. *) +(* Also exists under the form near=> x y. *) +(* - near: x discharges x: *) +(* On the goal H_i x, and where x \is_near F, it asks the user to prove *) +(* that (\forall x \near F, H_i x), provided that H_i x does not depend on *) +(* variables introduced after x. *) +(* Under the hood, it refines by intersection the existential variable ?H *) +(* attached to x, computes the intersection with F, and asks the user to *) +(* prove F H_i, right now. *) +(* - end_near should be used to close remaining existentials trivially. *) +(* - near F => x poses a variable near F, where F is a proper filter *) +(* It adds to the context a variable x that \is_near F, i.e., one may *) +(* assume H x for any H in F. This new variable x can be dealt with using *) +(* near: x, as for variables introduced by near=>. *) (* *) -(* * Topology : *) +(******************************************************************************) + +(******************************************************************************) +(* 2. Basic topological notions *) +(* *) +(* * Mathematical structures *) +(* ** 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. *) -(* topologyOfFilterMixin nbhs_filt nbhs_sing nbhs_nbhs == 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 == 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 *) +(* [topologicalType of T for cT] == T-clone of the topologicalType *) +(* structure cT *) +(* [topologicalType of T] == clone of a canonical structure of *) +(* topologicalType on T *) +(* open == set of open sets *) +(* open_nbhs p == set of open neighbourhoods of p *) +(* basis B == a family of open sets that converges *) +(* to each point *) +(* second_countable T == T has a countable basis *) +(* 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 *) +(* 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 *) +(* 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 == builds the mixin for a topological *) +(* topologyOfBaseMixin b_cover b_join == 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 *) +(* 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 == builds the mixin for a topological *) +(* topologyOfSubbaseMixin D b == 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. *) -(* TopologicalType T m == packs the mixin m to build a *) -(* topologicalType; T must have a *) -(* canonical structure of filteredType T. *) -(* weak_topologicalType f == weak topology by f : S -> T on S; S *) -(* must be a pointedType and T a *) +(* *) +(* We endow several standard types with the structure of topology, e.g.: *) +(* - products: prod_topologicalType *) +(* - matrices: matrix_topologicalType *) +(* - natural numbers: nat_topologicalType *) +(* *) +(* weak_topologicalType 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 *) -(* topologicalType structures Tc on T; T *) -(* must be a pointedType. *) +(* topologicalType structures Tc on T *) +(* T must be a pointedType. *) (* product_topologicalType T == product topology of the family of *) (* topologicalTypes T. *) -(* [topologicalType of T for cT] == T-clone of the topologicalType *) -(* structure cT. *) -(* [topologicalType of T] == clone of a canonical structure of *) -(* topologicalType on T. *) -(* open == set of open sets. *) -(* open_nbhs p == set of open neighbourhoods of p. *) -(* basis B == a family of open sets that converges *) -(* to each point *) -(* second_countable T == T has a countable basis *) -(* continuous f <-> f is continuous w.r.t the topology. *) +(* quotient_topology Q == the quotient topology corresponding to *) +(* quotient Q : quotType T. where T has *) +(* type topologicalType *) (* x^' == set of neighbourhoods of x where x is *) -(* excluded (a "deleted neighborhood"). *) +(* excluded (a "deleted neighborhood") *) (* closure A == closure of the set A. *) (* limit_point E == the set of limit points of E *) (* closed == set of closed sets. *) -(* cluster F == set of cluster points of F. *) +(* cluster F == set of cluster points of F *) (* compact == set of compact sets w.r.t. the filter- *) -(* based definition of compactness. *) +(* based definition of compactness *) +(* hausdorff_space T <-> T is a Hausdorff space (T2) *) (* compact_near F == the filter F contains a closed comapct *) (* set *) -(* precompact A == The set A is contained in a closed and *) +(* precompact A == the set A is contained in a closed and *) (* compact set *) (* locally_compact A == every point in A has a compact *) (* (and closed) neighborhood *) -(* hausdorff_space T <-> T is a Hausdorff space (T_2). *) (* discrete_space T <-> every nbhs is a principal filter *) (* discrete_topology dscT == the discrete topology on T, provided *) (* dscT : discrete space T *) (* finite_subset_cover D F A == the family of sets F is a cover of A *) (* for a finite number of indices in D *) (* cover_compact == set of compact sets w.r.t. the open *) -(* cover-based definition of compactness. *) +(* cover-based definition of compactness *) (* near_covering == a reformulation of covering compact *) (* better suited for use with `near` *) +(* kolmogorov_space T <-> T is a Kolmogorov space (T0) *) +(* accessible_space T <-> T is an accessible space (T1) *) +(* close x y <-> x and y are arbitrarily close w.r.t. *) +(* to balls *) (* connected A <-> the only non empty subset of A which *) -(* is both open and closed in A is A. *) -(* kolmogorov_space T <-> T is a Kolmogorov space (T_0). *) -(* accessible_space T <-> T is an accessible space (T_1). *) +(* is both open and closed in A is A *) (* separated A B == the two sets A and B are separated *) -(* component x == the connected component of point x *) +(* connected_component x == the connected component of point x *) (* perfect_set A == A is closed, and is every point in A *) -(* is a limit point of A. *) -(* totally_disconnected A == The only connected subsets of A are *) -(* empty or singletons. *) -(* zero_dimensional T == Points are separable by a clopen set. *) +(* is a limit point of A *) +(* totally_disconnected A == the only connected subsets of A are *) +(* empty or singletons *) +(* zero_dimensional T == points are separable by a clopen set *) (* set_nbhs A == filter from open sets containing A *) (* *) -(* *) -(* [locally P] := forall a, A a -> G (within A (nbhs x)) *) -(* if P is convertible to G (globally A) *) -(* quotient_topology Q == the quotient topology corresponding to *) -(* quotient Q : quotType T where T has *) -(* type topologicalType *) -(* *) -(* * Function space topologies : *) -(* {uniform` A -> V} == The space U -> V, equipped with the topology of *) -(* uniform convergence from a set A to V, where *) -(* V is a uniformType. *) -(* {uniform U -> V} := {uniform` [set: U] -> V} *) -(* {uniform A, F --> f} == F converges to f in {uniform A -> V}. *) -(* {uniform, F --> f} := {uniform setT, F --> f} *) -(* {ptws U -> V} == The space U -> V, equipped with the topology of *) -(* pointwise convergence from U to V, where V is a *) -(* topologicalType; notation for @fct_Pointwise U V. *) -(* {ptws, F --> f} == F converges to f in {ptws U -> V}. *) -(* {family fam, U -> V} == The space U -> V, equipped with the supremum *) -(* topology of {uniform A -> f} for each A in 'fam' *) -(* In particular {family compact, U -> V} is the *) -(* topology of compact convergence. *) -(* {family fam, F --> f} == F converges to f in {family fam, U -> V}. *) -(* *) -(* --> We used these topological notions to prove Tychonoff's Theorem, which *) -(* states that any product of compact sets is compact according to the *) -(* product topology. *) -(* * Uniform spaces : *) +(* ** Uniform spaces *) (* nbhs_ ent == neighbourhoods defined using entourages *) (* uniformType == interface type for uniform spaces: a *) (* type equipped with entourages *) @@ -304,107 +328,150 @@ Require Import reals signed. (* 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 *) -(* unif_continuous f <-> f is uniformly continuous. *) +(* countable_uniformity T == T's entourage has a countable base *) +(* This is equivalent to `T` being *) +(* 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 *) -(* countable_uniformity T == T's entourage has a countable base. This *) -(* is equivalent to `T` being metrizable *) -(* gauge E == For an entourage E, gauge E is a filter *) -(* which includes `iter n split_ent E`. *) -(* Critically, `gauge E` forms a uniform *) -(* space with a countable uniformity *) -(* gauge_psuedoMetricType E == the pseudoMetricType associated with the *) -(* `gauge E` *) (* discrete_ent == entourages for the discrete topology *) (* *) -(* * PseudoMetric spaces : *) -(* entourage_ ball == entourages defined using balls *) +(* We endow several standard types with the structure of uniform space, e.g.: *) +(* - products: prod_uniformType *) +(* - matrices: matrix_uniformType *) +(* *) +(* ** Pseudometric spaces *) (* pseudoMetricType == interface type for pseudo metric space *) -(* structure: a type equipped with balls. *) +(* 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. *) +(* balls and entourages *) (* PseudoMetricType T m == packs the pseudo metric space mixin into *) -(* a pseudoMetricType. T must have a *) -(* canonical structure of uniformType. *) +(* 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. *) +(* 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. *) +(* radius *) (* uniformityOfBallMixin umixin == builds the mixin for a topological space *) (* from a mixin for a pseudoMetric space. *) (* 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 *) -(* close x y <-> x and y are arbitrarily close w.r.t. to *) -(* balls. *) -(* weak_pseudoMetricType == the metric space for weak topologies *) -(* quotient_topology Q == the quotient topology corresponding to *) -(* quotient Q : quotType T. where T has *) -(* type topologicalType *) -(* discrete_ball == singleton balls for thediscrete topology *) +(* discrete_ball == singleton balls for the discrete *) +(* topology *) (* *) -(* * Complete uniform spaces : *) +(* We endow several standard types with the structure of pseudometric space, *) +(* e.g.: *) +(* - products: prod_pseudoMetricType *) +(* - matrices: matrix_pseudoMetricType *) +(* - weak_pseudoMetricType *) +(* - sup_pseudoMetricType *) +(* - product_pseudoMetricType *) +(* *) +(* ** Complete uniform spaces *) (* cauchy F <-> the set of sets F is a cauchy filter *) (* (entourage definition) *) (* completeType == interface type for a complete uniform *) -(* space structure. *) +(* 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 structure *) +(* T must have a canonical structure of *) +(* uniformType. *) (* [completeType of T for cT] == T-clone of the completeType structure *) -(* cT. *) +(* cT *) (* [completeType of T] == clone of a canonical structure of *) -(* completeType on T. *) +(* completeType on T *) +(* *) +(* We endow several standard types with the structure of complete uniform *) +(* space, e.g.: *) +(* - matrices: matrix_completeType *) +(* - functions: fun_completeType *) (* *) -(* * Complete pseudometric spaces : *) +(* ** Complete pseudometric spaces *) (* cauchy_ex F <-> the set of sets F is a cauchy filter *) -(* (epsilon-delta definition). *) -(* cauchy F <-> the set of sets F is a cauchy filter *) -(* (using the near notations). *) +(* (epsilon-delta definition) *) +(* cauchy_ball F <-> the set of sets F is a cauchy filter *) +(* (using the near notations) *) (* completePseudoMetricType == interface type for a complete *) -(* pseudometric space structure. *) +(* 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 *) +(* 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. *) -(* *) (* ball_ N == balls defined by the norm/absolute *) (* value N *) -(* dense S == the set (S : set T) is dense in T, with *) -(* T of type topologicalType *) (* *) -(* * Subspaces of topological spaces : *) -(* subspace A == for (A : set T), this is a copy of T with *) -(* a topology that ignores points outside A *) -(* incl_subspace x == with x of type subspace A with (A : set T), *) -(* inclusion of subspace A into T *) +(* We endow several standard types with the structure of complete *) +(* pseudometric space, e.g.: *) +(* - matrices: matrix_completePseudoMetricType *) +(* - functions: fct_completePseudoMetricType *) +(* *) +(* We endow numFieldType with the types of topological notions *) +(* (accessible with "Import numFieldTopology.Exports."): *) +(* - numField_filteredType *) +(* - numField_topologicalType *) +(* - numField_uniformType *) +(* - numField_pseudoMetricType *) +(* *) +(* ** Function space topologies *) +(* {uniform` A -> V} == the space U -> V, equipped with the topology of *) +(* uniform convergence from a set A to V, where *) +(* V is a uniformType *) +(* {uniform U -> V} := {uniform` [set: U] -> V} *) +(* {uniform A, F --> f} == F converges to f in {uniform A -> V} *) +(* {uniform, F --> f} := {uniform setT, F --> f} *) +(* {ptws U -> V} == the space U -> V, equipped with the topology of *) +(* pointwise convergence from U to V, where V is a *) +(* topologicalType *) +(* This is a notation for @fct_Pointwise U V. *) +(* {ptws, F --> f} == F converges to f in {ptws U -> V} *) +(* {family fam, U -> V} == The space U -> V, equipped with the supremum *) +(* topology of {uniform A -> f} for each A in 'fam' *) +(* In particular {family compact, U -> V} is the *) +(* topology of compact convergence. *) +(* {family fam, F --> f} == F converges to f in {family fam, U -> V} *) +(* *) +(* dense S == the set (S : set T) is dense in T, with T of *) +(* type topologicalType *) +(* weak_pseudoMetricType == the metric space for weak topologies *) (* *) -(* * Arzela Ascoli' theorem : *) -(* singletons T := [set [set x] | x in [set: T]]. *) +(* ** Subspaces of topological spaces *) +(* subspace A == for (A : set T), this is a copy of T with a *) +(* topology that ignores points outside A *) +(* incl_subspace x == with x of type subspace A with (A : set T), *) +(* inclusion of subspace A into T *) +(* separate_points_from_closed f == for a closed set U and point x outside *) +(* some member of the family f, it sends f_i(x) *) +(* outside (closure (f_i @` U)) *) +(* Used together with join_product. *) +(* join_product f == the function (x => f ^~ x) *) +(* When the family f separates points from closed *) +(* sets, join_product is an embedding. *) +(* singletons T := [set [set x] | x in [set: T]] *) +(* gauge E == for an entourage E, gauge E is a filter which *) +(* 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` *) +(* 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 *) -(* pointwise_precompact W == For each (x : X), set of images [f x | f in W] *) -(* is precompact *) +(* pointwise_precompact W == for each (x : X), the set of images *) +(* [f x | f in W] is precompact *) (* *) -(* We endow several standard types with the types of topological notions: *) -(* - products: prod_topologicalType, prod_uniformType, prod_pseudoMetricType *) -(* sup_pseudoMetricType, weak_pseudoMetricType, product_pseudoMetricType *) -(* - matrices: matrix_filtered, matrix_topologicalType, matrix_uniformType, *) -(* matrix_pseudoMetricType, matrix_completeType, *) -(* matrix_completePseudoMetricType *) -(* - nat: nat_filteredType, nat_topologicalType *) -(* - numFieldType: numField_filteredType, numField_topologicalType, *) -(* numField_uniformType, numField_pseudoMetricType (accessible with *) -(* "Import numFieldTopology.Exports.") *) (******************************************************************************) Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }"). @@ -523,9 +590,6 @@ Qed. End bigmaxmin. -Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := - {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. - Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) : {in p, forall x, P x /\ Q x} <-> {in p, forall x, P x} /\ {in p, forall x, Q x}. @@ -1944,7 +2008,7 @@ End within_topologicalType. Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)). -(** ** Topology defined by a filter *) +(** Topology defined by a filter *) (* was topologyOfFilterMixin *) HB.factory Record Nbhs_isNbhsTopological T of Nbhs T := { @@ -1975,7 +2039,7 @@ HB.instance Definition _ := Nbhs_isTopological.Build T HB.end. -(** ** Topology defined by open sets *) +(** Topology defined by open sets *) Definition nbhs_of_open (T : pointedType) (op : set T -> Prop) (p : T) (A : set T) := exists B, [/\ op B, B p & B `<=` A]. @@ -2024,7 +2088,7 @@ HB.instance Definition _ := Nbhs_isTopological.Build T HB.end. -(** ** Topology defined by a base of open sets *) +(** Topology defined by a base of open sets *) (* was topologyOfBaseMixin *) HB.factory Record Pointed_isBaseTopological T of Pointed T := { @@ -2129,7 +2193,7 @@ move=> [P sFP] [Q sFQ] PQB /filterS; apply; rewrite -PQB. by apply: (filterI _ _); [exact: (IH _ _ sFP)|exact: (IH _ _ sFQ)]. Qed. -(** ** Topology defined by a subbase of open sets *) +(** Topology defined by a subbase of open sets *) Definition finI_from (I : choiceType) T (D : set I) (f : I -> set T) := [set \bigcap_(i in [set` D']) f i | @@ -2407,7 +2471,7 @@ HB.instance Definition _ := Nbhs_isNbhsTopological.Build 'M[T]_(m, n) End matrix_Topology. -(** ** Weak topology by a function *) +(** Weak topology by a function *) Definition weak_topology {S : pointedType} {T : topologicalType} (f : S -> T) : Type := S. @@ -2465,7 +2529,7 @@ Qed. End Weak_Topology. -(** ** Supremum of a family of topologies *) +(** Supremum of a family of topologies *) Definition sup_topology {T : pointedType} {I : Type} (Tc : I -> Topological T) : Type := T. @@ -2503,7 +2567,7 @@ Qed. End Sup_Topology. -(** ** Product topology *) +(** Product topology *) Section Product_Topology. @@ -3921,7 +3985,7 @@ by move=> ->; have := projT2 (sigW (npts N)). Qed. Lemma perfect_set2 {T} : perfect_set [set: T] <-> - forall (U : set T), open U -> U !=set0 -> + forall (U : set T), open U -> U !=set0 -> exists x y, [/\ U x, U y & x != y] . Proof. apply: iff_trans; first exact: perfectTP; split. @@ -4001,9 +4065,9 @@ Qed. End totally_disconnected. Section set_nbhs. - Context {T : topologicalType} (A : set T). -Definition set_nbhs := \bigcap_(x in A) (nbhs x). + +Definition set_nbhs := \bigcap_(x in A) nbhs x. Global Instance set_nbhs_filter : Filter set_nbhs. Proof. @@ -5089,7 +5153,7 @@ rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor. Qed. -(** ** Specific pseudoMetric spaces *) +(** Specific pseudoMetric spaces *) (** matrices *) Section matrix_PseudoMetric. @@ -7332,7 +7396,7 @@ Qed. (* A convenient notion that is in between compactness in {family compact, X -> y} and compactness in {ptws X -> y}.*) Definition pointwise_precompact {I} (W : set I) (d : I -> X -> Y) := - forall x, precompact [set (d i x) | i in W]. + forall x, precompact [set d i x | i in W]. Lemma pointwise_precompact_subset {I J} (W : set I) (V : set J) {fW : I -> X -> Y} {fV : J -> X -> Y} :