Module mathcomp.analysis.topology

# Basic topological notions This file develops tools for the manipulation of basic topological notions. The development of topological notions builds on "filtered types" by extending the hierarchy. ## Mathematical structures ### Topology ``` topologicalType == interface type for topological space structure the HB class is Topological. ptopologicalType == a pointed topologicalType orderTopologicalType == a topology built from intervals open == set of open sets closed == set of closed sets clopen U == U is both open and closed 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) 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. isOpenTopological == factory for a topology defined by open sets It builds the mixin for a topological space from the properties of open sets, nbhs_of_open must be used to declare a filterType. 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 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 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 ``` We endow several standard types with the structure of topology, e.g.: - products `(T * U)%type` - matrices `'M[T]_(m, n)` - natural numbers `nat` ``` \oo == "eventually" filter on nat: set of predicates on natural numbers that are eventually true weak_topology f == weak topology by a function f : S -> T on S S must be a choiceType and T a topologicalType. sup_topology Tc == supremum topology of the family of topologicalType structures Tc on T order_topology T == the induced order topology on T 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") 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 compact == set of compact sets w.r.t. the filter- based definition of compactness hausdorff_space T <-> T is a Hausdorff space (T2) compact_near F == the filter F contains a closed compact set 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 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 near_covering == a reformulation of covering compact better suited for use with `near` near_covering_within == equivalent definition of near_covering 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 separated A B == the two sets A and B are separated connected_component x == the connected component of point x perfect_set A == A is closed, and 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 set_nbhs A == filter from open sets containing A ``` ### Uniform spaces ``` nbhs_ ent == neighborhoods defined using entourages uniformType == interface type for uniform spaces: a type equipped with entourages The HB class is Uniform. puniformType == a pointed and uniform space 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 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_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 `(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 The HB class is PseudoMetric. pseudoPMetricType == a pointed an pseudoMetric space 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 discrete_ball == singleton balls for the discrete topology discrete_topology_type == equip choice types with a discrete topology ``` We endow several standard types with the structure of pseudometric space, e.g.: - products `(U * V)%type` - matrices `'M[T]_(m, n)` - `weak_topology` (the metric space for weak topologies) - `sup_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 The HB class is Complete. ``` We endow several standard types with the structure of complete uniform space, e.g.: - matrices `'M[T]_(m, n)` - functions `T -> U` ### Complete pseudometric spaces ``` cauchy_ex F <-> the set of sets F is a cauchy filter (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 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 `'M[T]_(m, n)` - functions `T -> U` We endow `numFieldType` with the types of topological notions (accessible with `Import numFieldTopology.Exports.`) ``` 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 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.type is endowed with a pseudoMetricType normal_space X == X is normal (sometimes called T4) regular_space X == X is regular (sometimes called T3) ```