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. monotonous A f := {in A &, {mono f : x y / x <= y}} \/ {in A &, {mono f : x y /~ x <= y}}.

Filters :

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 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 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. 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 is included in the canonical filter 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. [lim F in T] == limit of the canonical filter associated to F in T where T has type filteredType U. [cvg F in T] <-> the canonical filter associated to F 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. Filter F == type class proving that the set of sets F is a filter. ProperFilter F == type class proving that the set of 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. FilterType F FF == packs the set of sets F with the proof FF of Filter F to build a filter_on T structure. pfilter_on T == interface type for sets of sets on T 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. fmap f F == image of the filter F by the function f E @ [x --> F] == image of the canonical filter associated to F by the function (fun x => E). f @ F == image of the canonical filter 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 associated to F by the relation (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. @frechet_filter T := [set S : set T | finite_set (~` S) ] a.k.a. cofinite filter 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. 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 in_filter F == interface type for the sets that 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. \oo == "eventually" filter on nat: set of predicates on natural numbers that are 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 F, P} == the property P holds near the 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=>.

Topology :

topologicalType == interface type for topological space structure. 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 used to declare a filterType. topologyOfBaseMixin b_cover b_join == 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 == 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 topologicalType. sup_topologicalType 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 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. 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. compact_near F == the filter F contains a closed comapct 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 hausdorff_space T <-> T is a Hausdorff space (T_2). discrete_space T <-> every nbhs is a principal filter 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` 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). separated A B == the two sets A and B are separated 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. 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 :

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 entourage == set of entourages in 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 unif_continuous f <-> f is uniformly continuous. 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 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. 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

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. 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.

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). 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. 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

Arzela Ascoli' theorem :

singletons T := [set [set x] | x in [set: T] ]. 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 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.")

Making sure that [Program] does not automatically introduce

Index a family of filters on a type, one for each element of the type

filter on arrow sources

The default filter for an arbitrary element is the one obtained from its type

the canonical filter on matrices on X is the product of the canonical filter on X

Filters

Definitions

TODO: Reuse :> above and remove the following line and the coercion below after 8.17 is the minimum required version for Coq

Typeclasses Opaque filter.

Typeclasses Opaque pfilter.

Near Tactic

add ball x e as a canonical instance of nbhs x

Coercion PropInFilter.t : in_filter >-> Funclass.

Limits expressed with filters

Typeclasses Opaque fmap.