Module mathcomp.analysis.topology_theory.topology_structure

# 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. In the identifiers, "nbhs" is an abbreviation for "neighborhoods". ## Mathematical structures ### Topology ``` topologicalType == interface type for topological space structure the HB class is Topological. subTopologicalType S == join of SubNbhs and Topological where S has pred V with V a topologicalType the HB class is SubTopological. ptopologicalType == a pointed topologicalType 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 [locally P] := forall a, A a -> G (within A (nbhs x)) if P is convertible to G (globally A) U° == all of the points which are locally in U, i.e., the largest open set contained in U This is a notation for `interior U`. closure U == the smallest closed set containing U regopen U == U is regular open, i.e., equal to the interior of its closure regclosed U == U is regular closed, i.e., equal to the closure of its interior open_of_nbhs B == the open sets induced by neighborhoods nbhs_of_open B == the neighborhoods induced by open sets x^' == set of neighbourhoods of x where x is excluded (a "deleted neighborhood") limit_point E == the set of limit points of E isolated A == the set of isolated points of A 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 ``` 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 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 ```