Module mathcomp.analysis.topology

From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import cardinality mathcomp_extra fsbigop.
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.

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.

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

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

Theory of filters

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

Near notations and tactics

The purpose of the near notations and tactics is to make the manipulation
of filters easier. Instead of proving F  GF\; G, one can prove G  xG\; x for
xx "near F", i.e., for x such that H x for H arbitrarily precise as long
as F  HF\; H. The near tactics allow for a delayed introduction of HH:
HH 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


2. Basic topological notions

Mathematical structures

Topology

                 topologicalType == interface type for topological space   
                                    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   
                                    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.                            
       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.          
       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. 
                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                   
    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 `(T * U)%type`                                                  
- matrices `'M[T]_(m, n)`                                                  
- natural numbers `nat`                                                    
                                                                           
                 weak_topology f == weak topology by a function f : S -> T 
                                    on S                                   
                                    S must be a pointedType and T a        
                                    topologicalType.                       
                 sup_topology Tc == supremum topology of the family of     
                                    topologicalType structures Tc on T     
                                    T must be a pointedType.               
                 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   
                                    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 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              
               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 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     

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

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

We endow several standard types with the structure of pseudometric space,
e.g.:

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

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

We endow numFieldType with the types of topological notions
(accessible with Import numFieldTopology.Exports.)

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}        
 {compact_open, U -> V} == compact-open topology                           
{compact_open, F --> f} == F converges to f in {compact_open, U -> V}      
                                                                           
                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                  
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.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     
 pointwise_precompact W == for each (x : X), the set of images             
                           [f x | f in W] is precompact                    

Reserved Notation "{ 'near' x , P }" (at level 0, format "{ 'near' x , P }").
Reserved Notation "'\forall' x '\near' x_0 , P"
  (at level 200, x name, P at level 200,
   format "'\forall' x '\near' x_0 , P").
Reserved Notation "'\near' x , P"
  (at level 200, x at level 99, P at level 200,
   format "'\near' x , P", only parsing).
Reserved Notation "{ 'near' x & y , P }"
  (at level 0, format "{ 'near' x & y , P }").
Reserved Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P"
  (at level 200, x name, y name, P at level 200,
   format "'\forall' x '\near' x_0 & y '\near' y_0 , P").
Reserved Notation "'\forall' x & y '\near' z , P"
  (at level 200, x name, y name, P at level 200,
   format "'\forall' x & y '\near' z , P").
Reserved Notation "'\near' x & y , P"
  (at level 200, x, y at level 99, P at level 200,
   format "'\near' x & y , P", only parsing).
Reserved Notation "[ 'filter' 'of' x ]" (format "[ 'filter' 'of' x ]").
Reserved Notation "F `=>` G" (at level 70, format "F `=>` G").
Reserved Notation "F --> G" (at level 70, format "F --> G").
Reserved Notation "[ 'lim' F 'in' T ]" (format "[ 'lim' F 'in' T ]").
Reserved Notation "[ 'cvg' F 'in' T ]" (format "[ 'cvg' F 'in' T ]").
Reserved Notation "x \is_near F" (at level 10, format "x \is_near F").
Reserved Notation "E @[ x --> F ]"
  (at level 60, x name, format "E @[ x --> F ]").
Reserved Notation "E @[ x \oo ]"
  (at level 60, x name, format "E @[ x \oo ]").
Reserved Notation "f @ F" (at level 60, format "f @ F").
Reserved Notation "E `@[ x --> F ]"
  (at level 60, x name, format "E `@[ x --> F ]").
Reserved Notation "f `@ F" (at level 60, format "f `@ F").
Reserved Notation "A ^°" (at level 1, format "A ^°").
Reserved Notation "[ 'locally' P ]" (at level 0, format "[ 'locally' P ]").
Reserved Notation "x ^'" (at level 2, format "x ^'").
Reserved Notation "{ 'within' A , 'continuous' f }"
  (at level 70, A at level 69, format "{ 'within' A , 'continuous' f }").
Reserved Notation "{ 'uniform`' A -> V }"
  (at level 0, A at level 69, format "{ 'uniform`' A -> V }").
Reserved Notation "{ 'uniform' U -> V }"
  (at level 0, U at level 69, format "{ 'uniform' U -> V }").
Reserved Notation "{ 'uniform' A , F --> f }"
  (at level 0, A at level 69, F at level 69,
   format "{ 'uniform' A , F --> f }").
Reserved Notation "{ 'uniform' , F --> f }"
  (at level 0, F at level 69,
   format "{ 'uniform' , F --> f }").
Reserved Notation "{ 'ptws' U -> V }"
  (at level 0, U at level 69, format "{ 'ptws' U -> V }").
Reserved Notation "{ 'ptws' , F --> f }"
  (at level 0, F at level 69, format "{ 'ptws' , F --> f }").
Reserved Notation "{ 'family' fam , U -> V }"
  (at level 0, U at level 69, format "{ 'family' fam , U -> V }").
Reserved Notation "{ 'family' fam , F --> f }"
  (at level 0, F at level 69, format "{ 'family' fam , F --> f }").
Reserved Notation "{ 'compact-open' , U -> V }"
  (at level 0, U at level 69, format "{ 'compact-open' , U -> V }").
Reserved Notation "{ 'compact-open' , F --> f }"
  (at level 0, F at level 69, format "{ 'compact-open' , F --> f }").

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Obligation Tactic := idtac.

Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section bigmaxmin.
Local Notation max := Order.max.
Local Notation min := Order.min.
Local Open Scope order_scope.
Variables (d : unit) (T : orderType d) (x : T) (I : finType) (P : pred I)
          (m : T) (F : I -> T).

Lemma bigmax_geP : reflect (m <= x \/ exists2 i, P i & m <= F i)
                           (m <= \big[max/x]_(i | P i) F i).
Proof.

Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i)
                           (m < \big[max/x]_(i | P i) F i).
Proof.

Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m)
                           (\big[min/x]_(i | P i) F i <= m).
Proof.

Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m)
                           (\big[min/x]_(i | P i) F i < m).
Proof.

End bigmaxmin.

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

Lemma mem_inc_segment d (T : porderType d) (a b : T) (f : T -> T) :
    {in `[a, b] &, {mono f : x y / (x <= y)%O}} ->
  {homo f : x / x \in `[a, b] >-> x \in `[f a, f b]}.
Proof.

Lemma mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) :
    {in `[a, b] &, {mono f : x y /~ (x <= y)%O}} ->
  {homo f : x / x \in `[a, b] >-> x \in `[f b, f a]}.
Proof.

Section Linear1.
Context (R : ringType) (U : lmodType R) (V : zmodType) (s : R -> V -> V).
HB.instance Definition _ := gen_eqMixin {linear U -> V | s}.
HB.instance Definition _ := gen_choiceMixin {linear U -> V | s}.
End Linear1.
Section Linear2.
Context (R : ringType) (U : lmodType R) (V : zmodType) (s : GRing.Scale.law R V).
HB.instance Definition _ :=
  isPointed.Build {linear U -> V | GRing.Scale.Law.sort s} \0.
End Linear2.

Definition set_system U := set (set U).
Identity Coercion set_system_to_set : set_system >-> set.

HB.mixin Record isFiltered U T := {
  nbhs : T -> set_system U
}.

#[short(type="filteredType")]
HB.structure Definition Filtered (U : Type) := {T of Pointed T & isFiltered U T}.
Arguments nbhs {_ _} _ _ : simpl never.

Notation "[ 'filteredType' U 'of' T ]" := (Filtered.clone U T _)
  (at level 0, format "[ 'filteredType' U 'of' T ]") : form_scope.

HB.instance Definition _ T := Equality.on (set_system T).
HB.instance Definition _ T := Choice.on (set_system T).
HB.instance Definition _ T := Pointed.on (set_system T).
HB.instance Definition _ T := isFiltered.Build T (set_system T) id.

Arguments nbhs {_ _} _ _ : simpl never.

HB.mixin Record selfFiltered T := {}.

HB.factory Record hasNbhs T := { nbhs : T -> set_system T }.
HB.builders Context T of hasNbhs T.
  HB.instance Definition _ := isFiltered.Build T T nbhs.
  HB.instance Definition _ := selfFiltered.Build T.
HB.end.

#[short(type="nbhsType")]
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].

HB.instance Definition _ m n X (Z : filteredType X) :=
  isFiltered.Build 'M[X]_(m, n) 'M[Z]_(m, n) (fun mx => filter_from
    [set P | forall i j, nbhs (mx i j) (P i j)]
    (fun P => [set my : 'M[X]_(m, n) | forall i j, P i j (my i j)])).

HB.instance Definition _ m n (X : nbhsType) := selfFiltered.Build 'M[X]_(m, n).

Definition filter_prod {T U : Type}
  (F : set_system T) (G : set_system U) : set_system (T * U) :=
  filter_from (fun P => F P.1 /\ G P.2) (fun P => P.1 `*` P.2).

Section Near.

Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0).
Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0).
Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
Local Notation ph := (phantom _).

Definition prop_near1 {X} {fX : filteredType X} (x : fX)
   P (phP : ph {all1 P}) := nbhs x P.

Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'}
  (x : fX) (x' : fX') := fun P of ph {all2 P} =>
  filter_prod (nbhs x) (nbhs x') (fun x => P x.1 x.2).

End Near.

Notation "{ 'near' x , P }" := (@prop_near1 _ _ x _ (inPhantom P)) : type_scope.
Notation "'\forall' x '\near' x_0 , P" := {near x_0, forall x, P} : type_scope.
Notation "'\near' x , P" := (\forall x \near x, P) : type_scope.
Notation "{ 'near' x & y , P }" :=
  (@prop_near2 _ _ _ _ x y _ (inPhantom P)) : type_scope.
Notation "'\forall' x '\near' x_0 & y '\near' y_0 , P" :=
  {near x_0 & y_0, forall x y, P} : type_scope.
Notation "'\forall' x & y '\near' z , P" :=
  {near z & z, forall x y, P} : type_scope.
Notation "'\near' x & y , P" := (\forall x \near x & y \near y, P) : type_scope.
Arguments prop_near1 : simpl never.
Arguments prop_near2 : simpl never.

Lemma nearE {T} {F : set_system T} (P : set T) :
  (\forall x \near F, P x) = F P.
Proof.

Lemma eq_near {T} {F : set_system T} (P Q : set T) :
   (forall x, P x <-> Q x) ->
   (\forall x \near F, P x) = (\forall x \near F, Q x).
Proof.


Lemma nbhs_filterE {T : Type} (F : set_system T) : nbhs F = F.
Proof.

Module Export NbhsFilter.
Definition nbhs_simpl := (@nbhs_filterE).
End NbhsFilter.

Definition cvg_to {T : Type} (F G : set_system T) := G `<=` F.
Notation "F `=>` G" := (cvg_to F G) : classical_set_scope.
Lemma cvg_refl T (F : set_system T) : F `=>` F.
Proof.
Arguments cvg_refl {T F}.
#[global] Hint Resolve cvg_refl : core.

Lemma cvg_trans T (G F H : set_system T) :
  (F `=>` G) -> (G `=>` H) -> (F `=>` H).
Proof.

Notation "F --> G" := (cvg_to (nbhs F) (nbhs G)) : classical_set_scope.
Definition type_of_filter {T} (F : set_system T) := T.

Definition lim_in {U : Type} (T : filteredType U) :=
  fun F : set_system U => get (fun l : T => F --> l).
Notation "[ 'lim' F 'in' T ]" := (@lim_in _ T (nbhs F)) : classical_set_scope.
Definition lim {T : nbhsType} (F : set_system T) := [lim F in T].
Notation "[ 'cvg' F 'in' T ]" := (F --> [lim F in T]) : classical_set_scope.
Notation cvg F := (F --> lim F).

Definition eventually := filter_from setT (fun N => [set n | (N <= n)%N]).
Notation "'\oo'" := eventually : classical_set_scope.

Section FilteredTheory.

HB.instance Definition _ X1 X2 (Z1 : filteredType X1) (Z2 : filteredType X2) :=
  isFiltered.Build (X1 * X2)%type (Z1 * Z2)%type
    (fun x => filter_prod (nbhs x.1) (nbhs x.2)).

HB.instance Definition _ (X1 X2 : nbhsType) :=
  selfFiltered.Build (X1 * X2)%type.

Lemma cvg_prod T {U U' V V' : filteredType T} (x : U) (l : U') (y : V) (k : V') :
  x --> l -> y --> k -> (x, y) --> (l, k).
Proof.

Lemma cvg_in_ex {U : Type} (T : filteredType U) (F : set_system U) :
  [cvg F in T] <-> (exists l : T, F --> l).
Proof.

Lemma cvg_ex (T : nbhsType) (F : set_system T) :
  cvg F <-> (exists l : T, F --> l).
Proof.

Lemma cvg_inP {U : Type} (T : filteredType U) (F : set_system U) (l : T) :
   F --> l -> [cvg F in T].
Proof.

Lemma cvgP (T : nbhsType) (F : set_system T) (l : T) : F --> l -> cvg F.
Proof.

Lemma cvg_in_toP {U : Type} (T : filteredType U) (F : set_system U) (l : T) :
   [cvg F in T] -> [lim F in T] = l -> F --> l.
Proof.

Lemma cvg_toP (T : nbhsType) (F : set_system T) (l : T) :
  cvg F -> lim F = l -> F --> l.
Proof.

Lemma dvg_inP {U : Type} (T : filteredType U) (F : set_system U) :
  ~ [cvg F in T] -> [lim F in T] = point.
Proof.

Lemma dvgP (T : nbhsType) (F : set_system T) : ~ cvg F -> lim F = point.
Proof.

Lemma cvg_inNpoint {U} (T : filteredType U) (F : set_system U) :
  [lim F in T] != point -> [cvg F in T].
Proof.

Lemma cvgNpoint (T : nbhsType) (F : set_system T) : lim F != point -> cvg F.
Proof.

End FilteredTheory.
Arguments cvg_inP {U T F} l.
Arguments dvg_inP {U} T {F}.
Arguments cvgP {T F} l.
Arguments dvgP {T F}.

Lemma nbhs_nearE {U} {T : filteredType U} (x : T) (P : set U) :
  nbhs x P = \near x, P x.
Proof.

Lemma near_nbhs {U} {T : filteredType U} (x : T) (P : set U) :
  (\forall x \near nbhs x, P x) = \near x, P x.
Proof.

Lemma near2_curry {U V} (F : set_system U) (G : set_system V) (P : U -> set V) :
  {near F & G, forall x y, P x y} = {near (F, G), forall x, P x.1 x.2}.
Proof.

Lemma near2_pair {U V} (F : set_system U) (G : set_system V) (P : set (U * V)) :
  {near F & G, forall x y, P (x, y)} = {near (F, G), forall x, P x}.
Proof.

Definition near2E := (@near2_curry, @near2_pair).

Lemma filter_of_nearI (X : Type) (fX : filteredType X)
  (x : fX) : forall P,
  nbhs x P = @prop_near1 X fX x P (inPhantom (forall x, P x)).
Proof.

Module Export NearNbhs.
Definition near_simpl := (@near_nbhs, @nbhs_nearE, filter_of_nearI).
Ltac near_simpl := rewrite ?near_simpl.
End NearNbhs.

Lemma near_swap {U V} (F : set_system U) (G : set_system V) (P : U -> set V) :
  (\forall x \near F & y \near G, P x y) = (\forall y \near G & x \near F, P x y).
Proof.

Filters

Class Filter {T : Type} (F : set_system T) := {
  filterT : F setT ;
  filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ;
  filterS : forall P Q : set T, P `<=` Q -> F P -> F Q
}.
Global Hint Mode Filter - ! : typeclass_instances.

Class ProperFilter' {T : Type} (F : set_system T) := {
  filter_not_empty : not (F (fun _ => False)) ;
  filter_filter' : Filter F
}.
Global Existing Instance filter_filter'.
Global Hint Mode ProperFilter' - ! : typeclass_instances.
Arguments filter_not_empty {T} F {_}.

Notation ProperFilter := ProperFilter'.

Lemma filter_setT (T' : Type) : Filter [set: set T'].
Proof.

Lemma filterP_strong T (F : set_system T) {FF : Filter F} (P : set T) :
  (exists Q : set T, exists FQ : F Q, forall x : T, Q x -> P x) <-> F P.
Proof.

Structure filter_on T := FilterType {
  filter :> set_system T;
  _ : Filter filter
}.
Definition filter_class T (F : filter_on T) : Filter F :=
  let: FilterType _ class := F in class.
Arguments FilterType {T} _ _.
#[global] Existing Instance filter_class.
Coercion filter_filter' : ProperFilter >-> Filter.

Structure pfilter_on T := PFilterPack {
  pfilter :> (T -> Prop) -> Prop;
  _ : ProperFilter pfilter
}.
Definition pfilter_class T (F : pfilter_on T) : ProperFilter F :=
  let: PFilterPack _ class := F in class.
Arguments PFilterPack {T} _ _.
#[global] Existing Instance pfilter_class.
Canonical pfilter_filter_on T (F : pfilter_on T) :=
  FilterType F (pfilter_class F).
Coercion pfilter_filter_on : pfilter_on >-> filter_on.
Definition PFilterType {T} (F : (T -> Prop) -> Prop)
  {fF : Filter F} (fN0 : not (F set0)) :=
  PFilterPack F (Build_ProperFilter' fN0 fF).
Arguments PFilterType {T} F {fF} fN0.

HB.instance Definition _ T := gen_eqMixin (filter_on T).
HB.instance Definition _ T := gen_choiceMixin (filter_on T).
HB.instance Definition _ T := isPointed.Build (filter_on T)
  (FilterType _ (filter_setT T)).
HB.instance Definition _ T := isFiltered.Build T (filter_on T) (@filter T).

Global Instance filter_on_Filter T (F : filter_on T) : Filter F.
Proof.
Global Instance pfilter_on_ProperFilter T (F : pfilter_on T) : ProperFilter F.
Proof.

Lemma nbhs_filter_onE T (F : filter_on T) : nbhs F = nbhs (filter F).
Proof.
Definition nbhs_simpl := (@nbhs_simpl, @nbhs_filter_onE).

Lemma near_filter_onE T (F : filter_on T) (P : set T) :
  (\forall x \near F, P x) = \forall x \near filter F, P x.
Proof.
Definition near_simpl := (@near_simpl, @near_filter_onE).

Program Definition trivial_filter_on T := FilterType [set setT : set T] _.
Next Obligation.
Canonical trivial_filter_on.

Lemma filter_nbhsT {T : Type} (F : set_system T) :
   Filter F -> nbhs F setT.
Proof.
#[global] Hint Resolve filter_nbhsT : core.

Lemma nearT {T : Type} (F : set_system T) : Filter F -> \near F, True.
Proof.
#[global] Hint Resolve nearT : core.

Lemma filter_not_empty_ex {T : Type} (F : set_system T) :
    (forall P, F P -> exists x, P x) -> ~ F set0.
Proof.

Definition Build_ProperFilter {T : Type} (F : set_system T)
  (filter_ex : forall P, F P -> exists x, P x)
  (filter_filter : Filter F) :=
  Build_ProperFilter' (filter_not_empty_ex filter_ex) (filter_filter).

Lemma filter_ex_subproof {T : Type} (F : set_system T) :
     ~ F set0 -> (forall P, F P -> exists x, P x).
Proof.

Definition filter_ex {T : Type} (F : set_system T) {FF : ProperFilter F} :=
  filter_ex_subproof (filter_not_empty F).
Arguments filter_ex {T F FF _}.

Lemma filter_getP {T : pointedType} (F : set_system T) {FF : ProperFilter F}
      (P : set T) : F P -> P (get P).
Proof.


Record in_filter T (F : set_system T) := InFilter {
  prop_in_filter_proj : T -> Prop;
  prop_in_filterP_proj : F prop_in_filter_proj
}.

Module Type PropInFilterSig.
Axiom t : forall (T : Type) (F : set_system T), in_filter F -> T -> Prop.
Axiom tE : t = prop_in_filter_proj.
End PropInFilterSig.
Module PropInFilter : PropInFilterSig.
Definition t := prop_in_filter_proj.
Lemma tE : t = prop_in_filter_proj
Proof.
End PropInFilter.
Notation prop_of := PropInFilter.t.
Definition prop_ofE := PropInFilter.tE.
Notation "x \is_near F" := (@PropInFilter.t _ F _ x).
Definition is_nearE := prop_ofE.

Lemma prop_ofP T F (iF : @in_filter T F) : F (prop_of iF).
Proof.

Definition in_filterT T F (FF : Filter F) : @in_filter T F :=
  InFilter (filterT).
Canonical in_filterI T F (FF : Filter F) (P Q : @in_filter T F) :=
  InFilter (filterI (prop_in_filterP_proj P) (prop_in_filterP_proj Q)).

Lemma filter_near_of T F (P : @in_filter T F) (Q : set T) : Filter F ->
  (forall x, prop_of P x -> Q x) -> F Q.
Proof.

Fact near_key : unit
Proof.

Lemma mark_near (P : Prop) : locked_with near_key P -> P.
Proof.

Lemma near_acc T F (P : @in_filter T F) (Q : set T) (FF : Filter F)
   (FQ : \forall x \near F, Q x) :
   locked_with near_key (forall x, prop_of (in_filterI FF P (InFilter FQ)) x -> Q x).
Proof.

Lemma near_skip_subproof T F (P Q : @in_filter T F) (G : set T) (FF : Filter F) :
   locked_with near_key (forall x, prop_of P x -> G x) ->
   locked_with near_key (forall x, prop_of (in_filterI FF P Q) x -> G x).
Proof.

Tactic Notation "near=>" ident(x) := apply: filter_near_of => x ?.

Ltac just_discharge_near x :=
  tryif match goal with Hx : x \is_near _ |- _ => move: (x) (Hx); apply: mark_near end
        then idtac else fail "the variable" x "is not a ""near"" variable".
Ltac near_skip :=
  match goal with |- locked_with near_key (forall _, @PropInFilter.t _ _ ?P _ -> _) =>
    tryif is_evar P then fail "nothing to skip" else apply: near_skip_subproof end.

Tactic Notation "near:" ident(x) :=
  just_discharge_near x;
  tryif do ![apply: near_acc; first shelve|near_skip]
  then idtac
  else fail "the goal depends on variables introduced after" x.

Ltac under_near i tac := near=> i; tac; near: i.
Tactic Notation "near=>" ident(i) "do" tactic3(tac) := under_near i ltac:(tac).
Tactic Notation "near=>" ident(i) "do" "[" tactic4(tac) "]" := near=> i do tac.
Tactic Notation "near" "do" tactic3(tac) :=
  let i := fresh "i" in under_near i ltac:(tac).
Tactic Notation "near" "do" "[" tactic4(tac) "]" := near do tac.

Ltac end_near := do ?exact: in_filterT.

Ltac done :=
  trivial; hnf; intros; solve
   [ do ![solve [trivial | apply: sym_equal; trivial]
         | discriminate | contradiction | split]
   | case not_locked_false_eq_true; assumption
   | match goal with H : ~ _ |- _ => solve [case H; trivial] end
   | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ].

Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) :
  ProperFilter (nbhs x) -> (\forall x \near x, P) -> P.
Proof.
Arguments have_near {U fT} x.

Tactic Notation "near" constr(F) "=>" ident(x) :=
  apply: (have_near F); near=> x.

Lemma near T (F : set_system T) P (FP : F P) (x : T)
  (Px : prop_of (InFilter FP) x) : P x.
Proof.
Arguments near {T F P} FP x Px.

Lemma nearW {T : Type} {F : set_system T} (P : T -> Prop) :
  Filter F -> (forall x, P x) -> (\forall x \near F, P x).
Proof.

Lemma filterE {T : Type} {F : set_system T} :
  Filter F -> forall P : set T, (forall x, P x) -> F P.
Proof.

Lemma filter_app (T : Type) (F : set_system T) :
  Filter F -> forall P Q : set T, F (fun x => P x -> Q x) -> F P -> F Q.
Proof.

Lemma filter_app2 (T : Type) (F : set_system T) :
  Filter F -> forall P Q R : set T, F (fun x => P x -> Q x -> R x) ->
  F P -> F Q -> F R.
Proof.

Lemma filter_app3 (T : Type) (F : set_system T) :
  Filter F -> forall P Q R S : set T, F (fun x => P x -> Q x -> R x -> S x) ->
  F P -> F Q -> F R -> F S.
Proof.

Lemma filterS2 (T : Type) (F : set_system T) :
  Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) ->
  F P -> F Q -> F R.
Proof.

Lemma filterS3 (T : Type) (F : set_system T) :
  Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) ->
  F P -> F Q -> F R -> F S.
Proof.

Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) :
  F (fun=> P) -> P.
Proof.

Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) :
  D i -> filter_from D B (B i).
Proof.

Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F ->
  (\forall x \near F, b1 x /\ b2 x) <->
    (\forall x \near F, b1 x) /\ (\forall x \near F, b2 x).
Proof.

Lemma nearP_dep {T U} {F : set_system T} {G : set_system U}
   {FF : Filter F} {FG : Filter G} (P : T -> U -> Prop) :
  (\forall x \near F & y \near G, P x y) ->
  \forall x \near F, \forall y \near G, P x y.
Proof.

Lemma filter2P T U (F : set_system T) (G : set_system U)
  {FF : Filter F} {FG : Filter G} (P : set (T * U)) :
  (exists2 Q : set T * set U, F Q.1 /\ G Q.2
     & forall (x : T) (y : U), Q.1 x -> Q.2 y -> P (x, y))
   <-> \forall x \near (F, G), P x.
Proof.

Lemma filter_ex2 {T U : Type} (F : set_system T) (G : set_system U)
  {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) :
    F P -> G Q -> exists x : T, exists2 y : U, P x & Q y.
Proof.
Arguments filter_ex2 {T U F G FF FG _ _}.

Lemma filter_fromP {I T : Type} (D : set I) (B : I -> set T) (F : set_system T) :
  Filter F -> F `=>` filter_from D B <-> forall i, D i -> F (B i).
Proof.

Lemma filter_fromTP {I T : Type} (B : I -> set T) (F : set_system T) :
  Filter F -> F `=>` filter_from setT B <-> forall i, F (B i).
Proof.

Lemma filter_from_filter {I T : Type} (D : set I) (B : I -> set T) :
  (exists i : I, D i) ->
  (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) ->
  Filter (filter_from D B).
Proof.

Lemma filter_fromT_filter {I T : Type} (B : I -> set T) :
  (exists _ : I, True) ->
  (forall i j, exists k, B k `<=` B i `&` B j) ->
  Filter (filter_from setT B).
Proof.

Lemma filter_from_proper {I T : Type} (D : set I) (B : I -> set T) :
  Filter (filter_from D B) ->
  (forall i, D i -> B i !=set0) ->
  ProperFilter (filter_from D B).
Proof.

Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T)
  (F : set_system T) :
  Filter F -> (forall i, i \in D -> F (f i)) ->
  F (\bigcap_(i in [set` D]) f i).
Proof.

Lemma filter_forall T (I : finType) (f : I -> set T) (F : set_system T) :
    Filter F -> (forall i : I, \forall x \near F, f i x) ->
  \forall x \near F, forall i, f i x.
Proof.

Lemma filter_imply [T : Type] [P : Prop] [f : set T] [F : set_system T] :
  Filter F -> (P -> \near F, f F) -> \near F, P -> f F.
Proof.

Limits expressed with filters

Definition fmap {T U : Type} (f : T -> U) (F : set_system T) : set_system U :=
  [set P | F (f @^-1` P)].
Arguments fmap _ _ _ _ _ /.

Lemma fmapE {U V : Type} (f : U -> V)
  (F : set_system U) (P : set V) : fmap f F P = F (f @^-1` P).
Proof.

Notation "E @[ x --> F ]" :=
  (fmap (fun x => E) (nbhs F)) : classical_set_scope.
Notation "E @[ x \oo ]" :=
  (fmap (fun x => E) \oo) : classical_set_scope.
Notation "f @ F" := (fmap f (nbhs F)) : classical_set_scope.

Notation limn F := (lim (F @ \oo)).
Notation cvgn F := (cvg (F @ \oo)).

Global Instance fmap_filter T U (f : T -> U) (F : set_system T) :
  Filter F -> Filter (f @ F).
Proof.

Global Instance fmap_proper_filter T U (f : T -> U) (F : set_system T) :
  ProperFilter F -> ProperFilter (f @ F).
Proof.
Definition fmap_proper_filter' := fmap_proper_filter.

Definition fmapi {T U : Type} (f : T -> set U) (F : set_system T) :
    set_system _ :=
  [set P | \forall x \near F, exists y, f x y /\ P y].

Notation "E `@[ x --> F ]" :=
  (fmapi (fun x => E) (nbhs F)) : classical_set_scope.
Notation "f `@ F" := (fmapi f (nbhs F)) : classical_set_scope.

Lemma fmapiE {U V : Type} (f : U -> set V)
  (F : set_system U) (P : set V) :
  fmapi f F P = \forall x \near F, exists y, f x y /\ P y.
Proof.

Global Instance fmapi_filter T U (f : T -> set U) (F : set_system T) :
  infer {near F, is_totalfun f} -> Filter F -> Filter (f `@ F).
Proof.

#[global] Typeclasses Opaque fmapi.

Global Instance fmapi_proper_filter
  T U (f : T -> U -> Prop) (F : set_system T) :
  infer {near F, is_totalfun f} ->
  ProperFilter F -> ProperFilter (f `@ F).
Proof.
Definition filter_map_proper_filter' := fmapi_proper_filter.

Lemma cvg_id T (F : set_system T) : x @[x --> F] --> F.
Proof.
Arguments cvg_id {T F}.

Lemma fmap_comp {A B C} (f : B -> C) (g : A -> B) F:
  Filter F -> (f \o g)%FUN @ F = f @ (g @ F).
Proof.

Lemma appfilter U V (f : U -> V) (F : set_system U) :
  f @ F = [set P : set _ | \forall x \near F, P (f x)].
Proof.

Lemma cvg_app U V (F G : set_system U) (f : U -> V) :
  F --> G -> f @ F --> f @ G.
Proof.
Arguments cvg_app {U V F G} _.

Lemma cvgi_app U V (F G : set_system U) (f : U -> set V) :
  F --> G -> f `@ F --> f `@ G.
Proof.

Lemma cvg_comp T U V (f : T -> U) (g : U -> V)
  (F : set_system T) (G : set_system U) (H : set_system V) :
  f @ F `=>` G -> g @ G `=>` H -> g \o f @ F `=>` H.
Proof.

Lemma cvgi_comp T U V (f : T -> U) (g : U -> set V)
  (F : set_system T) (G : set_system U) (H : set_system V) :
  f @ F `=>` G -> g `@ G `=>` H -> g \o f `@ F `=>` H.
Proof.

Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
  {near F, f =1 g} -> g @ F `=>` f @ F.
Proof.

Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
  f =1 g -> (f @ F --> x) = (g @ F --> x).
Proof.

Lemma eq_is_cvg_in (T T' : Type) (fT : filteredType T') (F : set_system T) (f g : T -> T') :
  f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
Proof.

Lemma eq_is_cvg (T : Type) (T' : nbhsType) (F : set_system T) (f g : T -> T') :
  f =1 g -> cvg (f @ F) = cvg (g @ F).
Proof.

Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
  {near F, f =2 g} -> g `@ F `=>` f `@ F.
Proof.

Lemma cvg_near_const (T U : Type) (f : T -> U) (F : set_system T) (G : set_system U) :
  Filter F -> ProperFilter G ->
  (\forall y \near G, \forall x \near F, f x = y) -> f @ F --> G.
Proof.


Definition globally {T : Type} (A : set T) : set_system T :=
   [set P : set T | forall x, A x -> P x].
Arguments globally {T} A _ /.

Lemma globally0 {T : Type} (A : set T) : globally set0 A
Proof.

Global Instance globally_filter {T : Type} (A : set T) :
  Filter (globally A).
Proof.

Global Instance globally_properfilter {T : Type} (A : set T) a :
  infer (A a) -> ProperFilter (globally A).
Proof.

Specific filters

Section frechet_filter.
Variable T : Type.

Definition frechet_filter := [set S : set T | finite_set (~` S)].

Global Instance frechet_properfilter : infinite_set [set: T] ->
  ProperFilter frechet_filter.
Proof.

End frechet_filter.

Global Instance frechet_properfilter_nat : ProperFilter (@frechet_filter nat).
Proof.

Section at_point.

Context {T : Type}.

Definition at_point (a : T) (P : set T) : Prop := P a.

Global Instance at_point_filter (a : T) : ProperFilter (at_point a).
Proof.
Typeclasses Opaque at_point.

End at_point.

Filters for pairs

Global Instance filter_prod_filter T U (F : set_system T) (G : set_system U) :
  Filter F -> Filter G -> Filter (filter_prod F G).
Proof.

Canonical prod_filter_on T U (F : filter_on T) (G : filter_on U) :=
  FilterType (filter_prod F G) (filter_prod_filter _ _).

Global Instance filter_prod_proper {T1 T2 : Type}
  {F : (T1 -> Prop) -> Prop} {G : (T2 -> Prop) -> Prop}
  {FF : ProperFilter F} {FG : ProperFilter G} :
  ProperFilter (filter_prod F G).
Proof.
Definition filter_prod_proper' := @filter_prod_proper.

Lemma filter_prod1 {T U} {F : set_system T} {G : set_system U}
  {FG : Filter G} (P : set T) :
  (\forall x \near F, P x) -> \forall x \near F & _ \near G, P x.
Proof.
Lemma filter_prod2 {T U} {F : set_system T} {G : set_system U}
  {FF : Filter F} (P : set U) :
  (\forall y \near G, P y) -> \forall _ \near F & y \near G, P y.
Proof.

Program Definition in_filter_prod {T U} {F : set_system T} {G : set_system U}
  (P : in_filter F) (Q : in_filter G) : in_filter (filter_prod F G) :=
  @InFilter _ _ (fun x => prop_of P x.1 /\ prop_of Q x.2) _.
Next Obligation.

Lemma near_pair {T U} {F : set_system T} {G : set_system U}
      {FF : Filter F} {FG : Filter G}
      (P : in_filter F) (Q : in_filter G) x :
       prop_of P x.1 -> prop_of Q x.2 -> prop_of (in_filter_prod P Q) x.
Proof.

Lemma cvg_fst {T U F G} {FG : Filter G} :
  (@fst T U) @ filter_prod F G --> F.
Proof.

Lemma cvg_snd {T U F G} {FF : Filter F} :
  (@snd T U) @ filter_prod F G --> G.
Proof.

Lemma near_map {T U} (f : T -> U) (F : set_system T) (P : set U) :
  (\forall y \near f @ F, P y) = (\forall x \near F, P (f x)).
Proof.

Lemma near_map2 {T T' U U'} (f : T -> U) (g : T' -> U')
      (F : set_system T) (G : set_system T') (P : U -> set U') :
  Filter F -> Filter G ->
  (\forall y \near f @ F & y' \near g @ G, P y y') =
  (\forall x \near F & x' \near G , P (f x) (g x')).
Proof.

Lemma near_mapi {T U} (f : T -> set U) (F : set_system T) (P : set U) :
  (\forall y \near f `@ F, P y) = (\forall x \near F, exists y, f x y /\ P y).
Proof.

Lemma filter_pair_set (T T' : Type) (F : set_system T) (F' : set_system T') :
   Filter F -> Filter F' ->
   forall (P : set T) (P' : set T') (Q : set (T * T')),
   (forall x x', P x -> P' x' -> Q (x, x')) -> F P /\ F' P' ->
   filter_prod F F' Q.
Proof.

Lemma filter_pair_near_of (T T' : Type) (F : set_system T) (F' : set_system T') :
   Filter F -> Filter F' ->
   forall (P : @in_filter T F) (P' : @in_filter T' F') (Q : set (T * T')),
   (forall x x', prop_of P x -> prop_of P' x' -> Q (x, x')) ->
   filter_prod F F' Q.
Proof.

Tactic Notation "near=>" ident(x) ident(y) :=
  (apply: filter_pair_near_of => x y ? ?).
Tactic Notation "near" constr(F) "=>" ident(x) ident(y) :=
  apply: (have_near F); near=> x y.

Module Export NearMap.
Definition near_simpl := (@near_simpl, @near_map, @near_mapi, @near_map2).
Ltac near_simpl := rewrite ?near_simpl.
End NearMap.

Lemma cvg_pair {T U V F} {G : set_system U} {H : set_system V}
  {FF : Filter F} {FG : Filter G} {FH : Filter H} (f : T -> U) (g : T -> V) :
  f @ F --> G -> g @ F --> H ->
  (f x, g x) @[x --> F] --> (G, H).
Proof.

Lemma cvg_comp2 {T U V W}
  {F : set_system T} {G : set_system U} {H : set_system V} {I : set_system W}
  {FF : Filter F} {FG : Filter G} {FH : Filter H}
  (f : T -> U) (g : T -> V) (h : U -> V -> W) :
  f @ F --> G -> g @ F --> H ->
  h (fst x) (snd x) @[x --> (G, H)] --> I ->
  h (f x) (g x) @[x --> F] --> I.
Proof.
Arguments cvg_comp2 {T U V W F G H I FF FG FH f g h} _ _ _.
Definition cvg_to_comp_2 := @cvg_comp2.


Restriction of a filter to a domain

Section within.
Context {T : Type}.
Implicit Types (D : set T) (F : set_system T).

Definition within D F : set_system T := [set P | {near F, D `<=` P}].
Arguments within : simpl never.

Lemma near_withinE D F (P : set T) :
  (\forall x \near within D F, P x) = {near F, D `<=` P}.
Proof.

Lemma withinT F D : Filter F -> within D F D.
Proof.

Lemma near_withinT F D : Filter F -> \forall x \near within D F, D x.
Proof.

Lemma cvg_within {F} {FF : Filter F} D : within D F --> F.
Proof.

Lemma withinET {F} {FF : Filter F} : within setT F = F.
Proof.

End within.

Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
Proof.

#[global] Typeclasses Opaque within.

Canonical within_filter_on T D (F : filter_on T) :=
  FilterType (within D F) (within_filter _ _).

Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
  (F : set (set T)) (P : set T) :
  Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->
  F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]).
Proof.

Definition subset_filter {T} (F : set_system T) (D : set T) :=
  [set P : set {x | D x} | F [set x | forall Dx : D x, P (exist _ x Dx)]].
Arguments subset_filter {T} F D _.

Global Instance subset_filter_filter T F (D : set T) :
  Filter F -> Filter (subset_filter F D).
Proof.
#[global] Typeclasses Opaque subset_filter.

Lemma subset_filter_proper {T F} {FF : Filter F} (D : set T) :
  (forall P, F P -> ~ ~ exists x, D x /\ P x) ->
  ProperFilter (subset_filter F D).
Proof.

Section NearSet.
Context {Y : Type}.
Context (F : set_system Y) (PF : ProperFilter F).

Definition powerset_filter_from : set_system (set Y) := filter_from
  [set M | [/\ M `<=` F,
    (forall E1 E2, M E1 -> F E2 -> E2 `<=` E1 -> M E2) & M !=set0 ] ]
  id.

Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from.
Proof.

Lemma near_small_set : \forall E \near powerset_filter_from, F E.
Proof.

Lemma small_set_sub (E : set Y) : F E ->
  \forall E' \near powerset_filter_from, E' `<=` E.
Proof.

Lemma near_powerset_filter_fromP (P : set Y -> Prop) :
  (forall A B, A `<=` B -> P B -> P A) ->
  (\forall U \near powerset_filter_from, P U) <-> exists2 U, F U & P U.
Proof.

Lemma powerset_filter_fromP C :
  F C -> powerset_filter_from [set W | F W /\ W `<=` C].
Proof.

End NearSet.

Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set_system T)
  (P : set U -> Prop) :
  ProperFilter F ->
  (\forall y \near powerset_filter_from (f x @[x --> F]), P y) ->
  (\forall y \near powerset_filter_from F, P (f @` y)).
Proof.

Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set_system T)
  (P : set U -> Prop) :
  (forall X Y, X `<=` Y -> P Y -> P X) ->
  ProperFilter F ->
  (\forall y \near powerset_filter_from F, P (f @` y)) =
  (\forall y \near powerset_filter_from (f x @[x --> F]), P y).
Proof.

Section PrincipalFilters.

Definition principal_filter {X : Type} (x : X) : set_system X :=
  globally [set x].

Lemma principal_filterP {X} (x : X) (W : set X) : principal_filter x W <-> W x.
Proof.

Lemma principal_filter_proper {X} (x : X) : ProperFilter (principal_filter x).
Proof.

HB.instance Definition _ := hasNbhs.Build bool principal_filter.

End PrincipalFilters.

Topological spaces
HB.mixin Record Nbhs_isTopological (T : Type) of Nbhs T := {
  open : set_system T;
  nbhs_pfilter_subproof : forall p : T, ProperFilter (nbhs p) ;
  nbhsE_subproof : forall p : T, nbhs p =
    [set A : set T | exists B : set T, [/\ open B, B p & B `<=` A] ] ;
  openE_subproof : open = [set A : set T | A `<=` nbhs^~ A ]
}.

#[short(type="topologicalType")]
HB.structure Definition Topological :=
  {T of Nbhs T & Nbhs_isTopological T}.

Section Topological1.

Context {T : topologicalType}.

Definition open_nbhs (p : T) (A : set T) := open A /\ A p.

Definition basis (B : set (set T)) :=
  B `<=` open /\ forall x, filter_from [set U | B U /\ U x] id --> x.

Definition second_countable := exists2 B, countable B & basis B.

Global Instance nbhs_pfilter (p : T) : ProperFilter (nbhs p).
Proof.
Typeclasses Opaque nbhs.

Lemma nbhs_filter (p : T) : Filter (nbhs p).
Proof.

Canonical nbhs_filter_on (x : T) := FilterType (nbhs x) (@nbhs_filter x).

Lemma nbhsE (p : T) :
  nbhs p = [set A : set T | exists2 B : set T, open_nbhs p B & B `<=` A].
Proof.

Lemma open_nbhsE (p : T) (A : set T) : open_nbhs p A = (open A /\ nbhs p A).
Proof.

Definition interior (A : set T) := (@nbhs _ T)^~ A.

Local Notation "A ^°" := (interior A).

Lemma interior_subset (A : set T) : A^° `<=` A.
Proof.

Lemma openE : open = [set A : set T | A `<=` A^°].
Proof.

Lemma nbhs_singleton (p : T) (A : set T) : nbhs p A -> A p.
Proof.

Lemma nbhs_interior (p : T) (A : set T) : nbhs p A -> nbhs p A^°.
Proof.

Lemma open0 : open (set0 : set T).
Proof.

Lemma openT : open (setT : set T).
Proof.

Lemma openI (A B : set T) : open A -> open B -> open (A `&` B).
Proof.

Lemma bigcup_open (I : Type) (D : set I) (f : I -> set T) :
  (forall i, D i -> open (f i)) -> open (\bigcup_(i in D) f i).
Proof.

Lemma openU (A B : set T) : open A -> open B -> open (A `|` B).
Proof.

Lemma open_subsetE (A B : set T) : open A -> (A `<=` B) = (A `<=` B^°).
Proof.

Lemma open_interior (A : set T) : open A^°.
Proof.

Lemma interior_bigcup I (D : set I) (f : I -> set T) :
  \bigcup_(i in D) (f i)^° `<=` (\bigcup_(i in D) f i)^°.
Proof.

Lemma open_nbhsT (p : T) : open_nbhs p setT.
Proof.

Lemma open_nbhsI (p : T) (A B : set T) :
  open_nbhs p A -> open_nbhs p B -> open_nbhs p (A `&` B).
Proof.

Lemma open_nbhs_nbhs (p : T) (A : set T) : open_nbhs p A -> nbhs p A.
Proof.

Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°.
Proof.

End Topological1.

#[global] Hint Extern 0 (Filter (nbhs _)) =>
  solve [apply: nbhs_filter] : typeclass_instances.
#[global] Hint Extern 0 (ProperFilter (nbhs _)) =>
  solve [apply: nbhs_pfilter] : typeclass_instances.

Notation "A ^°" := (interior A) : classical_set_scope.

Definition continuous_at (T U : nbhsType) (x : T) (f : T -> U) :=
  (f%function @ x --> f%function x).
Notation continuous f := (forall x, continuous_at x f).

Lemma near_fun (T T' : nbhsType) (f : T -> T') (x : T) (P : T' -> Prop) :
    {for x, continuous f} ->
  (\forall y \near f x, P y) -> (\near x, P (f x)).
Proof.
Arguments near_fun {T T'} f x.

Lemma continuousP (S T : topologicalType) (f : S -> T) :
  continuous f <-> forall A, open A -> open (f @^-1` A).
Proof.

Lemma continuous_comp (R S T : topologicalType) (f : R -> S) (g : S -> T) x :
  {for x, continuous f} -> {for (f x), continuous g} ->
  {for x, continuous (g \o f)}.
Proof.

Lemma open_comp {T U : topologicalType} (f : T -> U) (D : set U) :
  {in f @^-1` D, continuous f} -> open D -> open (f @^-1` D).
Proof.

Lemma cvg_fmap {T: topologicalType} {U : topologicalType}
  (F : set_system T) x (f : T -> U) :
   {for x, continuous f} -> F --> x -> f @ F --> f x.
Proof.

Lemma near_join (T : topologicalType) (x : T) (P : set T) :
  (\near x, P x) -> \near x, \near x, P x.
Proof.

Lemma near_bind (T : topologicalType) (P Q : set T) (x : T) :
  (\near x, (\near x, P x) -> Q x) -> (\near x, P x) -> \near x, Q x.
Proof.


Lemma continuous_cvg {T : Type} {V U : topologicalType}
  (F : set_system T) (FF : Filter F)
  (f : T -> V) (h : V -> U) (a : V) :
  {for a, continuous h} ->
  f @ F --> a -> (h \o f) @ F --> h a.
Proof.

Lemma continuous_is_cvg {T : Type} {V U : topologicalType} [F : set_system T]
  (FF : Filter F) (f : T -> V) (h : V -> U) :
  (forall l, f x @[x --> F] --> l -> {for l, continuous h}) ->
  cvg (f x @[x --> F]) -> cvg ((h \o f) x @[x --> F]).
Proof.

Lemma continuous2_cvg {T : Type} {V W U : topologicalType}
  (F : set_system T) (FF : Filter F)
  (f : T -> V) (g : T -> W) (h : V -> W -> U) (a : V) (b : W) :
  h z.1 z.2 @[z --> (a, b)] --> h a b ->
  f @ F --> a -> g @ F --> b -> (fun x => h (f x) (g x)) @ F --> h a b.
Proof.

Lemma cvg_near_cst (T : Type) (U : topologicalType)
  (l : U) (f : T -> U) (F : set_system T) {FF : Filter F} :
  (\forall x \near F, f x = l) -> f @ F --> l.
Proof.
Arguments cvg_near_cst {T U} l {f F FF}.

Lemma is_cvg_near_cst (T : Type) (U : topologicalType)
  (l : U) (f : T -> U) (F : set_system T) {FF : Filter F} :
  (\forall x \near F, f x = l) -> cvg (f @ F).
Proof.
Arguments is_cvg_near_cst {T U} l {f F FF}.

Lemma near_cst_continuous (T U : topologicalType)
  (l : U) (f : T -> U) (x : T) :
  (\forall y \near x, f y = l) -> {for x, continuous f}.
Proof.
Arguments near_cst_continuous {T U} l [f x].

Lemma cvg_cst (U : topologicalType) (x : U) (T : Type)
    (F : set_system T) {FF : Filter F} :
  (fun _ : T => x) @ F --> x.
Proof.
Arguments cvg_cst {U} x {T F FF}.
#[global] Hint Resolve cvg_cst : core.

Lemma is_cvg_cst (U : topologicalType) (x : U) (T : Type)
  (F : set_system T) {FF : Filter F} :
  cvg ((fun _ : T => x) @ F).
Proof.
Arguments is_cvg_cst {U} x {T F FF}.
#[global] Hint Resolve is_cvg_cst : core.

Lemma cst_continuous {T U : topologicalType} (x : U) :
  continuous (fun _ : T => x).
Proof.

Section within_topologicalType.
Context {T : topologicalType} (A : set T).
Implicit Types B : set T.

Lemma within_nbhsW (x : T) : A x -> within A (nbhs x) `=>` globally A.
Proof.

Definition locally_of (P : set_system T -> Prop) of phantom Prop (P (globally A))
  := forall x, A x -> P (within A (nbhs x)).
Local Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).

Lemma within_interior (x : T) : A^° x -> within A (nbhs x) = nbhs x.
Proof.

Lemma within_subset B F : Filter F -> A `<=` B -> within A F `=>` within B F.
Proof.

Lemma withinE F : Filter F ->
  within A F = [set U | exists2 V, F V & U `&` A = V `&` A].
Proof.

Lemma fmap_within_eq {S : topologicalType} (F : set_system T) (f g : T -> S) :
  Filter F -> {in A, f =1 g} -> f @ within A F --> g @ within A F.
Proof.

End within_topologicalType.

Notation "[ 'locally' P ]" := (@locally_of _ _ _ (Phantom _ P)).

Topology defined by a filter

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;
  nbhs_nbhs : forall (p : T) (A : set T), nbhs p A -> nbhs p (nbhs^~ A);
}.

HB.builders Context T of Nbhs_isNbhsTopological T.

Definition open_of_nbhs := [set A : set T | A `<=` nbhs^~ A].

Lemma nbhsE_subproof (p : T) :
  nbhs p = [set A | exists B, [/\ open_of_nbhs B, B p & B `<=` A] ].
Proof.

Lemma openE_subproof : open_of_nbhs = [set A : set T | A `<=` nbhs^~ A].
Proof.

HB.instance Definition _ := Nbhs_isTopological.Build T
  nbhs_filter nbhsE_subproof openE_subproof.

HB.end.

Topology defined by open sets

Definition nbhs_of_open (T : Type) (op : set T -> Prop) (p : T) (A : set T) :=
  exists B, [/\ op B, B p & B `<=` A].

HB.factory Record Pointed_isOpenTopological T of Pointed T := {
  op : set T -> Prop;
  opT : op setT;
  opI : forall (A B : set T), op A -> op B -> op (A `&` B);
  op_bigU : forall (I : Type) (f : I -> set T), (forall i, op (f i)) ->
    op (\bigcup_i f i);
}.

HB.builders Context T of Pointed_isOpenTopological T.

HB.instance Definition _ := hasNbhs.Build T (nbhs_of_open op).

Lemma nbhs_pfilter_subproof (p : T) : ProperFilter (nbhs p).
Proof.

Lemma nbhsE_subproof (p : T) :
  nbhs p = [set A | exists B, [/\ op B, B p & B `<=` A] ].
Proof.

Lemma openE_subproof : op = [set A : set T | A `<=` nbhs^~ A].
Proof.

HB.instance Definition _ := Nbhs_isTopological.Build T
  nbhs_pfilter_subproof nbhsE_subproof openE_subproof.

HB.end.

Topology defined by a base of open sets

HB.factory Record Pointed_isBaseTopological T of Pointed T := {
  I : pointedType;
  D : set I;
  b : I -> (set T);
  b_cover : \bigcup_(i in D) b i = setT;
  b_join : forall i j t, D i -> D j -> b i t -> b j t ->
    exists k, [/\ D k, b k t & b k `<=` b i `&` b j];
}.

HB.builders Context T of Pointed_isBaseTopological T.

Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].

Lemma open_fromT : open_from setT.
Proof.

Lemma open_fromI (A B : set T) : open_from A -> open_from B ->
  open_from (A `&` B).
Proof.

Lemma open_from_bigU (I0 : Type) (f : I0 -> set T) :
  (forall i, open_from (f i)) -> open_from (\bigcup_i f i).
Proof.

HB.instance Definition _ := Pointed_isOpenTopological.Build T
  open_fromT open_fromI open_from_bigU.

HB.end.

Section filter_supremums.

Global Instance smallest_filter_filter {T : Type} (F : set (set T)) :
  Filter (smallest Filter F).
Proof.

Fixpoint filterI_iter {T : Type} (F : set (set T)) (n : nat) :=
  if n is m.+1
  then [set P `&` Q |
    P in filterI_iter F m & Q in filterI_iter F m]
  else setT |` F.

Lemma filterI_iter_sub {T : Type} (F : set (set T)) :
  {homo filterI_iter F : i j / (i <= j)%N >-> i `<=` j}.
Proof.

Lemma filterI_iterE {T : Type} (F : set (set T)) :
  smallest Filter F = filter_from (\bigcup_n (filterI_iter F n)) id.
Proof.

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 |
    D' in [set A : {fset I} | {subset A <= D}]].

Lemma finI_from_cover (I : choiceType) T (D : set I) (f : I -> set T) :
  \bigcup_(A in finI_from D f) A = setT.
Proof.

Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i :
  D i -> finI_from D f (f i).
Proof.

Lemma finI_from_countable (I : pointedType) T (D : set I) (f : I -> set T) :
  countable D -> countable (finI_from D f).
Proof.

Lemma finI_fromI {I : choiceType} T D (f : I -> set T) A B :
  finI_from D f A -> finI_from D f B -> finI_from D f (A `&` B) .
Proof.

Lemma filterI_iter_finI {I : choiceType} T D (f : I -> set T) :
  finI_from D f = \bigcup_n (filterI_iter (f @` D) n).
Proof.

Lemma smallest_filter_finI {T : choiceType} (D : set T) f :
  filter_from (finI_from D f) id = smallest (@Filter T) (f @` D).
Proof.

End filter_supremums.

HB.factory Record Pointed_isSubBaseTopological T of Pointed T := {
  I : pointedType;
  D : set I;
  b : I -> (set T);
}.

HB.builders Context T of Pointed_isSubBaseTopological T.

Local Notation finI_from := (finI_from D b).

Lemma finI_from_cover : \bigcup_(A in finI_from) A = setT.
Proof.

Lemma finI_from_join A B t : finI_from A -> finI_from B -> A t -> B t ->
  exists k, [/\ finI_from k, k t & k `<=` A `&` B].
Proof.

HB.instance Definition _ := Pointed_isBaseTopological.Build T
  finI_from_cover finI_from_join.

HB.end.

Topology on nat

Section nat_topologicalType.

Let D : set nat := setT.
Let b : nat -> set nat := fun i => [set i].
Let bT : \bigcup_(i in D) b i = setT.
Proof.

Let bD : forall i j t, D i -> D j -> b i t -> b j t ->
  exists k, [/\ D k, b k t & b k `<=` b i `&` b j].
Proof.

HB.instance Definition _ := Pointed_isBaseTopological.Build nat bT bD.

End nat_topologicalType.

Global Instance eventually_filter : ProperFilter eventually.
Proof.

Canonical eventually_filterType := FilterType eventually _.
Canonical eventually_pfilterType := PFilterType eventually (filter_not_empty _).

Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N.
Proof.
#[global] Hint Resolve nbhs_infty_gt : core.

Lemma nbhs_infty_ge N : \forall n \near \oo, (N <= n)%N.
Proof.

Lemma cvg_addnl N : addn N @ \oo --> \oo.
Proof.

Lemma cvg_addnr N : addn^~ N @ \oo --> \oo.
Proof.

Lemma cvg_subnr N : subn^~ N @ \oo --> \oo.
Proof.

Lemma cvg_mulnl N : (N > 0)%N -> muln N @ \oo --> \oo.
Proof.

Lemma cvg_mulnr N :(N > 0)%N -> muln^~ N @ \oo --> \oo.
Proof.

Lemma cvg_divnr N : (N > 0)%N -> divn^~ N @ \oo --> \oo.
Proof.

Lemma near_inftyS (P : set nat) :
  (\forall x \near \oo, P (S x)) -> (\forall x \near \oo, P x).
Proof.

Section infty_nat.
Local Open Scope nat_scope.

Let cvgnyP {F : set_system nat} {FF : Filter F} : [<->
F --> \oo;
forall A, \forall x \near F, A <= x;
forall A, \forall x \near F, A < x;
\forall A \near \oo, \forall x \near F, A < x;
\forall A \near \oo, \forall x \near F, A <= x ].
Proof.

Section map.

Context {I : Type} {F : set_system I} {FF : Filter F} (f : I -> nat).

Lemma cvgnyPge :
  f @ F --> \oo <-> forall A, \forall x \near F, A <= f x.
Proof.

Lemma cvgnyPgt :
  f @ F --> \oo <-> forall A, \forall x \near F, A < f x.
Proof.

Lemma cvgnyPgty :
  f @ F --> \oo <-> \forall A \near \oo, \forall x \near F, A < f x.
Proof.

Lemma cvgnyPgey :
  f @ F --> \oo <-> \forall A \near \oo, \forall x \near F, A <= f x.
Proof.

End map.

End infty_nat.

Topology on the product of two spaces

Section Prod_Topology.

Context {T U : topologicalType}.

Let prod_nbhs (p : T * U) := filter_prod (nbhs p.1) (nbhs p.2).

Lemma prod_nbhs_filter (p : T * U) : ProperFilter (prod_nbhs p).
Proof.

Lemma prod_nbhs_singleton (p : T * U) (A : set (T * U)) : prod_nbhs p A -> A p.
Proof.

Lemma prod_nbhs_nbhs (p : T * U) (A : set (T * U)) :
  prod_nbhs p A -> prod_nbhs p (prod_nbhs^~ A).
Proof.

HB.instance Definition _ := hasNbhs.Build (T * U)%type prod_nbhs.

HB.instance Definition _ := Nbhs_isNbhsTopological.Build (T * U)%type
  prod_nbhs_filter prod_nbhs_singleton prod_nbhs_nbhs.

End Prod_Topology.

Topology on matrices

Lemma fst_open {U V : topologicalType} (A : set (U * V)) :
  open A -> open (fst @` A).
Proof.

Lemma snd_open {U V : topologicalType} (A : set (U * V)) :
  open A -> open (snd @` A).
Proof.

Section matrix_Topology.

Variables (m n : nat) (T : topologicalType).

Implicit Types M : 'M[T]_(m, n).

Lemma mx_nbhs_filter M : ProperFilter (nbhs M).
Proof.

Lemma mx_nbhs_singleton M (A : set 'M[T]_(m, n)) : nbhs M A -> A M.
Proof.

Lemma mx_nbhs_nbhs M (A : set 'M[T]_(m, n)) : nbhs M A -> nbhs M (nbhs^~ A).
Proof.

HB.instance Definition _ := Nbhs_isNbhsTopological.Build 'M[T]_(m, n)
  mx_nbhs_filter mx_nbhs_singleton mx_nbhs_nbhs.

End matrix_Topology.

Weak topology by a function

Definition weak_topology {S : pointedType} {T : topologicalType}
  (f : S -> T) : Type := S.

Section Weak_Topology.

Variable (S : pointedType) (T : topologicalType) (f : S -> T).
Local Notation W := (weak_topology f).

Definition wopen := [set f @^-1` A | A in open].

Lemma wopT : wopen [set: W].
Proof.

Lemma wopI (A B : set W) : wopen A -> wopen B -> wopen (A `&` B).
Proof.

Lemma wop_bigU (I : Type) (g : I -> set W) :
  (forall i, wopen (g i)) -> wopen (\bigcup_i g i).
Proof.

HB.instance Definition _ := Pointed.on W.
HB.instance Definition _ :=
  Pointed_isOpenTopological.Build W wopT wopI wop_bigU.

Lemma weak_continuous : continuous (f : W -> T).
Proof.

Lemma cvg_image (F : set_system S) (s : S) :
  Filter F -> f @` setT = setT ->
  F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s.
Proof.

End Weak_Topology.

Supremum of a family of topologies

Definition sup_topology {T : pointedType} {I : Type}
  (Tc : I -> Topological T) : Type := T.

Section Sup_Topology.

Variable (T : pointedType) (I : Type) (Tc : I -> Topological T).
Local Notation S := (sup_topology Tc).

Let TS := fun i => Topological.Pack (Tc i).

Definition sup_subbase := \bigcup_i (@open (TS i) : set_system T).

HB.instance Definition _ := Pointed.on S.
HB.instance Definition _ := Pointed_isSubBaseTopological.Build S sup_subbase id.

Lemma cvg_sup (F : set_system T) (t : T) :
  Filter F -> F --> (t : S) <-> forall i, F --> (t : TS i).
Proof.

End Sup_Topology.

Product topology

Section Product_Topology.

Definition prod_topology {I : Type} (T : I -> Type) := forall i, T i.

Variable (I : Type) (T : I -> topologicalType).

Definition product_topology_def :=
  sup_topology (fun i => Topological.class
    (weak_topology (fun f : [the pointedType of (forall i : I, T i)] => f i))).

HB.instance Definition _ :=
  Topological.copy (prod_topology T) product_topology_def.

End Product_Topology.

deleted neighborhood

Definition dnbhs {T : topologicalType} (x : T) :=
  within (fun y => y != x) (nbhs x).
Notation "x ^'" := (dnbhs x) : classical_set_scope.

Lemma nbhs_dnbhs_neq {T : topologicalType} (p : T) :
  \forall x \near nbhs p^', x != p.
Proof.

Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x.
Proof.

Global Instance dnbhs_filter {T : topologicalType} (x : T) : Filter x^'.
Proof.
#[global] Typeclasses Opaque dnbhs.

Canonical dnbhs_filter_on (T : topologicalType) (x : T) :=
  FilterType x^' (dnbhs_filter _).

Lemma cvg_fmap2 (T U : Type) (f : T -> U):
  forall (F G : set_system T), G `=>` F -> f @ G `=>` f @ F.
Proof.

Lemma cvg_within_filter {T U} {f : T -> U} (F : set_system T) {FF : (Filter F) }
  (G : set_system U) : forall (D : set T), (f @ F) --> G -> (f @ within D F) --> G.
Proof.

Lemma cvg_app_within {T} {U : topologicalType} (f : T -> U) (F : set_system T)
  (D : set T): Filter F -> cvg (f @ F) -> cvg (f @ within D F).
Proof.

Lemma nbhs_dnbhs {T : topologicalType} (x : T) : x^' `=>` nbhs x.
Proof.

meets

Lemma meets_openr {T : topologicalType} (F : set_system T) (x : T) :
  F `#` nbhs x = F `#` open_nbhs x.
Proof.

Lemma meets_openl {T : topologicalType} (F : set_system T) (x : T) :
  nbhs x `#` F = open_nbhs x `#` F.
Proof.

Lemma meets_globallyl T (A : set T) G :
  globally A `#` G = forall B, G B -> A `&` B !=set0.
Proof.

Lemma meets_globallyr T F (B : set T) :
  F `#` globally B = forall A, F A -> A `&` B !=set0.
Proof.

Lemma meetsxx T (F : set_system T) (FF : Filter F) : F `#` F = ~ (F set0).
Proof.

Lemma proper_meetsxx T (F : set_system T) (FF : ProperFilter F) : F `#` F.
Proof.

Closed sets in topological spaces

Section Closed.

Context {T : topologicalType}.

Definition closure (A : set T) :=
  [set p : T | forall B, nbhs p B -> A `&` B !=set0].

Lemma closure0 : closure set0 = set0 :> set T.
Proof.

Lemma closureEnbhs A : closure A = [set p | globally A `#` nbhs p].
Proof.

Lemma closureEonbhs A : closure A = [set p | globally A `#` open_nbhs p].
Proof.

Lemma subset_closure (A : set T) : A `<=` closure A.
Proof.

Lemma closure_eq0 (A : set T) : closure A = set0 -> A = set0.
Proof.

Lemma closureI (A B : set T) : closure (A `&` B) `<=` closure A `&` closure B.
Proof.

Definition limit_point E := [set t : T |
  forall U, nbhs t U -> exists y, [/\ y != t, E y & U y]].

Lemma limit_pointEnbhs E :
  limit_point E = [set p | globally (E `\ p) `#` nbhs p].
Proof.

Lemma limit_pointEonbhs E :
  limit_point E = [set p | globally (E `\ p) `#` open_nbhs p].
Proof.

Lemma subset_limit_point E : limit_point E `<=` closure E.
Proof.

Lemma closure_limit_point E : closure E = E `|` limit_point E.
Proof.

Definition closed (D : set T) := closure D `<=` D.

Lemma open_closedC (D : set T) : open D -> closed (~` D).
Proof.

Lemma closed_bigI {I} (D : set I) (f : I -> set T) :
  (forall i, D i -> closed (f i)) -> closed (\bigcap_(i in D) f i).
Proof.

Lemma closedI (D E : set T) : closed D -> closed E -> closed (D `&` E).
Proof.

Lemma closedT : closed setT
Proof.

Lemma closed0 : closed set0.
Proof.

Lemma closedE : closed = [set A : set T | forall p, ~ (\near p, ~ A p) -> A p].
Proof.

Lemma closed_openC (D : set T) : closed D -> open (~` D).
Proof.

Lemma closedC (D : set T) : closed (~` D) = open D.
Proof.

Lemma openC (D : set T) : open (~`D) = closed (D).
Proof.

Lemma closed_closure (A : set T) : closed (closure A).
Proof.

End Closed.

Lemma closed_comp {T U : topologicalType} (f : T -> U) (D : set U) :
  {in ~` f @^-1` D, continuous f} -> closed D -> closed (f @^-1` D).
Proof.

Lemma closed_cvg {T} {V : topologicalType} {F} {FF : ProperFilter F}
    (u_ : T -> V) (A : V -> Prop) :
    closed A -> (\forall n \near F, A (u_ n)) ->
  forall l, u_ @ F --> l -> A l.
Proof.
Arguments closed_cvg {T V F FF u_} _ _ _ _ _.

Lemma continuous_closedP (S T : topologicalType) (f : S -> T) :
  continuous f <-> forall A, closed A -> closed (f @^-1` A).
Proof.

Lemma closedU (T : topologicalType) (D E : set T) :
  closed D -> closed E -> closed (D `|` E).
Proof.

Lemma closed_bigsetU (T : topologicalType) (I : eqType) (s : seq I)
    (F : I -> set T) : (forall x, x \in s -> closed (F x)) ->
  closed (\big[setU/set0]_(x <- s) F x).
Proof.

Lemma closed_bigcup (T : topologicalType) (I : choiceType) (A : set I)
    (F : I -> set T) :
    finite_set A -> (forall i, A i -> closed (F i)) ->
  closed (\bigcup_(i in A) F i).
Proof.

Section closure_lemmas.
Variable T : topologicalType.
Implicit Types E A B U : set T.

Lemma closure_subset A B : A `<=` B -> closure A `<=` closure B.
Proof.

Lemma closureE A : closure A = smallest closed A.
Proof.

Lemma closureC E :
  ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x.
Proof.

Lemma closure_id E : closed E <-> E = closure E.
Proof.

End closure_lemmas.

Compact sets

Section Compact.

Context {T : topologicalType}.

Definition cluster (F : set_system T) := [set p : T | F `#` nbhs p].

Lemma cluster_nbhs t : cluster (nbhs t) t.
Proof.

Lemma clusterEonbhs F : cluster F = [set p | F `#` open_nbhs p].
Proof.

Lemma clusterE F : cluster F = \bigcap_(A in F) (closure A).
Proof.

Lemma closureEcluster E : closure E = cluster (globally E).
Proof.

Lemma cvg_cluster F G : F --> G -> cluster F `<=` cluster G.
Proof.

Lemma cluster_cvgE F :
  Filter F ->
  cluster F = [set p | exists2 G, ProperFilter G & G --> p /\ F `<=` G].
Proof.

Lemma closureEcvg (E : set T):
  closure E =
  [set p | exists2 G, ProperFilter G & G --> p /\ globally E `<=` G].
Proof.

Definition compact A := forall (F : set_system T),
  ProperFilter F -> F A -> A `&` cluster F !=set0.

Lemma compact0 : compact set0.
Proof.

Lemma subclosed_compact (A B : set T) :
  closed A -> compact B -> A `<=` B -> compact A.
Proof.

Definition hausdorff_space := forall p q : T, cluster (nbhs p) q -> p = q.

Typeclasses Opaque within.
Global Instance within_nbhs_proper (A : set T) p :
  infer (closure A p) -> ProperFilter (within A (nbhs p)).
Proof.

Lemma compact_closed (A : set T) : hausdorff_space -> compact A -> closed A.
Proof.

Lemma compact_set1 (x : T) : compact [set x].
Proof.

End Compact.

Arguments hausdorff_space : clear implicits.

Section ClopenSets.
Implicit Type T : topologicalType.

Definition clopen {T} (A : set T) := open A /\ closed A.

Lemma clopenI {T} (A B : set T) : clopen A -> clopen B -> clopen (A `&` B).
Proof.

Lemma clopenU {T} (A B : set T) : clopen A -> clopen B -> clopen (A `|` B).
Proof.

Lemma clopenC {T} (A B : set T) : clopen A -> clopen (~`A).
Proof.

Lemma clopen0 {T} : @clopen T set0.
Proof.

Lemma clopenT {T} : clopen [set: T].
Proof.

Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) :
 clopen A -> continuous f -> clopen (f @^-1` A).
Proof.

End ClopenSets.

Section near_covering.
Context {X : topologicalType}.

Definition near_covering (K : set X) :=
  forall (I : Type) (F : set_system I) (P : I -> X -> Prop),
  Filter F ->
  (forall x, K x -> \forall x' \near x & i \near F, P i x') ->
  \near F, K `<=` P F.

Let near_covering_compact : near_covering `<=` compact.
Proof.

Let compact_near_covering : compact `<=` near_covering.
Proof.

Lemma compact_near_coveringP A : compact A <-> near_covering A.
Proof.

Definition near_covering_within (K : set X) :=
  forall (I : Type) (F : set_system I) (P : I -> X -> Prop),
  Filter F ->
  (forall x, K x -> \forall x' \near x & i \near F, K x' -> P i x') ->
  \near F, K `<=` P F.

Lemma near_covering_withinP (K : set X) :
  near_covering_within K <-> near_covering K.
Proof.

End near_covering.

Lemma compact_setM {U V : topologicalType} (P : set U) (Q : set V) :
  compact P -> compact Q -> compact (P `*` Q).
Proof.

Section Tychonoff.

Class UltraFilter T (F : set_system T) := {
  ultra_proper :> ProperFilter F ;
  max_filter : forall G : set_system T, ProperFilter G -> F `<=` G -> G = F
}.

Lemma ultra_cvg_clusterE (T : topologicalType) (F : set_system T) :
  UltraFilter F -> cluster F = [set p | F --> p].
Proof.

Lemma ultraFilterLemma T (F : set_system T) :
  ProperFilter F -> exists G, UltraFilter G /\ F `<=` G.
Proof.

Lemma compact_ultra (T : topologicalType) :
  compact = [set A | forall F : set_system T,
  UltraFilter F -> F A -> A `&` [set p | F --> p] !=set0].
Proof.

Lemma filter_image (T U : Type) (f : T -> U) (F : set_system T) :
  Filter F -> f @` setT = setT -> Filter [set f @` A | A in F].
Proof.

Lemma proper_image (T U : Type) (f : T -> U) (F : set_system T) :
  ProperFilter F -> f @` setT = setT -> ProperFilter [set f @` A | A in F].
Proof.

Lemma principal_filter_ultra {T : Type} (x : T) :
  UltraFilter (principal_filter x).
Proof.

Lemma in_ultra_setVsetC T (F : set_system T) (A : set T) :
  UltraFilter F -> F A \/ F (~` A).
Proof.

Lemma ultra_image (T U : Type) (f : T -> U) (F : set_system T) :
  UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | A in F].
Proof.

Lemma tychonoff (I : eqType) (T : I -> topologicalType)
  (A : forall i, set (T i)) :
  (forall i, compact (A i)) ->
  compact [set f : prod_topology T | forall i, A i (f i)].
Proof.

End Tychonoff.

Lemma compact_cluster_set1 {T : topologicalType} (x : T) F V :
  hausdorff_space T -> compact V -> nbhs x V ->
  ProperFilter F -> F V -> cluster F = [set x] -> F --> x.
Proof.
Section Precompact.

Context {X : topologicalType}.

Lemma compactU (A B : set X) : compact A -> compact B -> compact (A `|` B).
Proof.

Lemma bigsetU_compact I (F : I -> set X) (s : seq I) (P : pred I) :
    (forall i, P i -> compact (F i)) ->
  compact (\big[setU/set0]_(i <- s | P i) F i).
Proof.

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.

Definition precompact (C : set X) := compact_near (globally C).

Lemma precompactE (C : set X) : precompact C = compact (closure C).
Proof.

Lemma precompact_subset (A B : set X) :
  A `<=` B -> precompact B -> precompact A.
Proof.

Lemma compact_precompact (A : set X) :
  hausdorff_space X -> compact A -> precompact A.
Proof.

Lemma precompact_closed (A : set X) : closed A -> precompact A = compact A.
Proof.

Definition locally_compact (A : set X) := [locally precompact A].

End Precompact.

Section product_spaces.
Context {I : eqType} {K : I -> topologicalType}.

Definition prod_topo_apply x (f : forall i, K i) := f x.


Lemma proj_continuous i : continuous (proj i : prod_topology K -> K i).
Proof.

Lemma dfwith_continuous g (i : I) : continuous (dfwith g _ : K i -> prod_topology K).
Proof.

Lemma proj_open i (A : set (prod_topology K)) : open A -> open (proj i @` A).
Proof.

Lemma hausdorff_product :
  (forall x, hausdorff_space (K x)) -> hausdorff_space (prod_topology K).
Proof.

End product_spaces.

Definition finI (I : choiceType) T (D : set I) (f : I -> set T) :=
  forall D' : {fset I}, {subset D' <= D} ->
  \bigcap_(i in [set i | i \in D']) f i !=set0.

Lemma finI_filter (I : choiceType) T (D : set I) (f : I -> set T) :
  finI D f -> ProperFilter (filter_from (finI_from D f) id).
Proof.

Lemma filter_finI (T : pointedType) (F : set_system T) (D : set_system T)
  (f : set T -> set T) :
  ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f.
Proof.

Definition finite_subset_cover (I : choiceType) (D : set I)
    U (F : I -> set U) (A : set U) :=
  exists2 D' : {fset I}, {subset D' <= D} & A `<=` cover [set` D'] F.

Section Covers.

Variable T : topologicalType.

Definition cover_compact (A : set T) :=
  forall (I : choiceType) (D : set I) (f : I -> set T),
  (forall i, D i -> open (f i)) -> A `<=` cover D f ->
  finite_subset_cover D f A.

Definition open_fam_of (A : set T) I (D : set I) (f : I -> set T) :=
  exists2 g : I -> set T, (forall i, D i -> open (g i)) &
    forall i, D i -> f i = A `&` g i.

Lemma cover_compactE : cover_compact =
  [set A | forall (I : choiceType) (D : set I) (f : I -> set T),
    open_fam_of A D f ->
      A `<=` cover D f -> finite_subset_cover D f A].
Proof.

Definition closed_fam_of (A : set T) I (D : set I) (f : I -> set T) :=
  exists2 g : I -> set T, (forall i, D i -> closed (g i)) &
    forall i, D i -> f i = A `&` g i.

Lemma compact_In0 :
  compact = [set A | forall (I : choiceType) (D : set I) (f : I -> set T),
    closed_fam_of A D f -> finI D f -> \bigcap_(i in D) f i !=set0].
Proof.

Lemma compact_cover : compact = cover_compact.
Proof.

End Covers.

Lemma finite_compact {X : topologicalType} (A : set X) :
  finite_set A -> compact A.
Proof.

Lemma clopen_countable {T : topologicalType}:
  compact [set: T] -> @second_countable T -> countable (@clopen T).
Proof.

Section set_nbhs.
Context {T : topologicalType} (A : set T).

Definition set_nbhs := \bigcap_(x in A) nbhs x.

Global Instance set_nbhs_filter : Filter set_nbhs.
Proof.

Global Instance set_nbhs_pfilter : A!=set0 -> ProperFilter set_nbhs.
Proof.

Lemma set_nbhsP (B : set T) :
   set_nbhs B <-> (exists C, [/\ open C, A `<=` C & C `<=` B]).
Proof.

End set_nbhs.


Section separated_topologicalType.
Variable T : topologicalType.
Implicit Types x y : T.

Local Open Scope classical_set_scope.

Definition kolmogorov_space := forall x y, x != y ->
  exists A : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).

Definition accessible_space := forall x y, x != y ->
  exists A : set T, open A /\ x \in A /\ y \in ~` A.

Lemma accessible_closed_set1 : accessible_space -> forall x, closed [set x].
Proof.

Lemma accessible_kolmogorov : accessible_space -> kolmogorov_space.
Proof.

Lemma accessible_finite_set_closed :
  accessible_space <-> forall A : set T, finite_set A -> closed A.
Proof.

Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.

Lemma closeEnbhs x : close x = cluster (nbhs x).
Proof.

Lemma closeEonbhs x : close x = [set y | open_nbhs x `#` open_nbhs y].
Proof.

Lemma close_sym x y : close x y -> close y x.
Proof.

Lemma cvg_close {F} {FF : ProperFilter F} x y : F --> x -> F --> y -> close x y.
Proof.

Lemma close_refl x : close x x.
Proof.
Hint Resolve close_refl : core.

Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} :
  F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
Proof.

Lemma cvgx_close x y : x --> y -> close x y.
Proof.

Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
  {near F, is_fun f} -> f `@ F --> l -> f `@ F --> l' -> close l l'.
Proof.
Definition cvg_toi_locally_close := @cvgi_close.

Lemma open_hausdorff : hausdorff_space T =
  forall x y, x != y ->
    exists2 AB, (x \in AB.1 /\ y \in AB.2) &
                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
Proof.

Definition hausdorff_accessible : hausdorff_space T -> accessible_space.
Proof.

Definition normal_space :=
  forall A : set T, closed A ->
    filter_from (set_nbhs A) closure `=>` set_nbhs A.

Definition regular_space :=
  forall a : T, filter_from (nbhs a) closure --> a.

Hypothesis sep : hausdorff_space T.

Lemma closeE x y : close x y = (x = y).
Proof.

Lemma close_eq x y : close x y -> x = y.
Proof.


Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
Proof.

Lemma cvg_eq x y : x --> y -> x = y.
Proof.

Lemma lim_id x : lim (nbhs x) = x.
Proof.

Lemma cvg_lim {U : Type} {F} {FF : ProperFilter F} (f : U -> T) (l : T) :
  f @ F --> l -> lim (f @ F) = l.
Proof.

Lemma lim_near_cst {U} {F} {FF : ProperFilter F} (l : T) (f : U -> T) :
   (\forall x \near F, f x = l) -> lim (f @ F) = l.
Proof.

Lemma lim_cst {U} {F} {FF : ProperFilter F} (k : T) :
   lim ((fun _ : U => k) @ F) = k.
Proof.

Lemma cvgi_unique {U : Type} {F} {FF : ProperFilter F} (f : U -> set T) :
  {near F, is_fun f} -> is_subset1 [set x : T | f `@ F --> x].
Proof.

Lemma cvgi_lim {U} {F} {FF : ProperFilter F} (f : U -> T -> Prop) (l : T) :
  F (fun x : U => is_subset1 (f x)) ->
  f `@ F --> l -> lim (f `@ F) = l.
Proof.

Lemma compact_regular (x : T) V : compact V -> nbhs x V -> {for x, regular_space}.
Proof.

End separated_topologicalType.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvg_lim`")]
Notation cvg_map_lim := cvg_lim (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed to `cvgi_lim`")]
Notation cvgi_map_lim := cvgi_lim (only parsing).

Section connected_sets.
Variable T : topologicalType.
Implicit Types A B C D : set T.

Definition connected A :=
  forall B, B !=set0 -> (exists2 C, open C & B = A `&` C) ->
  (exists2 C, closed C & B = A `&` C) -> B = A.

Lemma connected0 : connected (@set0 T).
Proof.

Definition separated A B :=
  (closure A) `&` B = set0 /\ A `&` (closure B) = set0.

Lemma separatedC A B : separated A B = separated B A.
Proof.

Lemma separated_disjoint A B : separated A B -> A `&` B = set0.
Proof.

Lemma connectedPn A : ~ connected A <->
  exists E : bool -> set T, [/\ forall b, E b !=set0,
    A = E false `|` E true & separated (E false) (E true)].
Proof.

Lemma connectedP A : connected A <->
  forall E : bool -> set T, ~ [/\ forall b, E b !=set0,
    A = E false `|` E true & separated (E false) (E true)].
Proof.

Lemma connected_subset A B C : separated A B -> C `<=` A `|` B ->
  connected C -> C `<=` A \/ C `<=` B.
Proof.

Lemma connected1 x : connected [set x].
Proof.
Hint Resolve connected1 : core.

Lemma bigcup_connected I (A : I -> set T) (P : I -> Prop) :
  \bigcap_(i in P) (A i) !=set0 -> (forall i, P i -> connected (A i)) ->
  connected (\bigcup_(i in P) (A i)).
Proof.

Lemma connectedU A B : A `&` B !=set0 -> connected A -> connected B ->
   connected (A `|` B).
Proof.

Lemma connected_closure A : connected A -> connected (closure A).
Proof.

Definition connected_component (A : set T) (x : T) :=
  \bigcup_(A in [set C : set T | [/\ C x, C `<=` A & connected C]]) A.

Lemma component_connected A x : connected (connected_component A x).
Proof.

Lemma connected_component_sub A x : connected_component A x `<=` A.
Proof.

Lemma connected_component_id A x :
  A x -> connected A -> connected_component A x = A.
Proof.

Lemma connected_component_out A x :
  ~ A x -> connected_component A x = set0.
Proof.

Lemma connected_component_max A B x : B x -> B `<=` A ->
  connected B -> B `<=` connected_component A x.
Proof.

Lemma connected_component_refl A x : A x -> connected_component A x x.
Proof.

Lemma connected_component_cover A :
  \bigcup_(A in connected_component A @` A) A = A.
Proof.

Lemma connected_component_sym A x y :
  connected_component A x y -> connected_component A y x.
Proof.

Lemma connected_component_trans A y x z :
    connected_component A x y -> connected_component A y z ->
  connected_component A x z.
Proof.

Lemma same_connected_component A x y : connected_component A x y ->
  connected_component A x = connected_component A y.
Proof.

Lemma component_closed A x : closed A -> closed (connected_component A x).
Proof.

Lemma clopen_separatedP A : clopen A <-> separated A (~` A).
Proof.

End connected_sets.
Arguments connected {T}.
Arguments connected_component {T}.
Section DiscreteTopology.
Section DiscreteMixin.
Context {X : Type}.

Lemma discrete_sing (p : X) (A : set X) : principal_filter p A -> A p.
Proof.

Lemma discrete_nbhs (p : X) (A : set X) :
  principal_filter p A -> principal_filter p (principal_filter^~ A).
Proof.

End DiscreteMixin.

Definition discrete_space (X : nbhsType) := @nbhs X _ = @principal_filter X.

Context {X : topologicalType} {dsc : discrete_space X}.

Lemma discrete_open (A : set X) : open A.
Proof.

Lemma discrete_set1 (x : X) : nbhs x [set x].
Proof.

Lemma discrete_closed (A : set X) : closed A.
Proof.

Lemma discrete_cvg (F : set_system X) (x : X) :
  Filter F -> F --> x <-> F [set x].
Proof.

Lemma discrete_hausdorff : hausdorff_space X.
Proof.

HB.instance Definition _ := Nbhs_isNbhsTopological.Build bool
  principal_filter_proper discrete_sing discrete_nbhs.

Lemma discrete_bool : discrete_space [the topologicalType of bool : Type].
Proof.

Lemma bool_compact : compact [set: bool].
Proof.

End DiscreteTopology.

#[global] Hint Resolve discrete_bool : core.

Section perfect_sets.

Implicit Types (T : topologicalType).

Definition perfect_set {T} (A : set T) := closed A /\ limit_point A = A.

Lemma perfectTP {T} : perfect_set [set: T] <-> forall x : T, ~ open [set x].
Proof.

Lemma perfect_prod {I : Type} (i : I) (K : I -> topologicalType) :
  perfect_set [set: K i] -> perfect_set [set: prod_topology K].
Proof.

Lemma perfect_diagonal (K : nat -> topologicalType) :
  (forall i, exists (xy: K i * K i), xy.1 != xy.2) ->
  perfect_set [set: prod_topology K].
Proof.

Lemma perfect_set2 {T} : perfect_set [set: T] <->
  forall (U : set T), open U -> U !=set0 ->
  exists x y, [/\ U x, U y & x != y] .
Proof.

End perfect_sets.

Section totally_disconnected.
Implicit Types T : topologicalType.

Definition totally_disconnected {T} (A : set T) :=
  forall x, A x -> connected_component A x = [set x].

Definition zero_dimensional T :=
  (forall x y, x != y -> exists U : set T, [/\ clopen U, U x & ~ U y]).

Lemma zero_dimension_prod (I : choiceType) (T : I -> topologicalType) :
  (forall i, zero_dimensional (T i)) ->
  zero_dimensional (prod_topology T).
Proof.

Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T.
Proof.

Lemma zero_dimension_totally_disconnected {T} :
  zero_dimensional T -> totally_disconnected [set: T].
Proof.

Lemma totally_disconnected_cvg {T : topologicalType} (x : T) :
  hausdorff_space T -> zero_dimensional T -> compact [set: T] ->
  filter_from [set D : set T | D x /\ clopen D] id --> x.
Proof.

End totally_disconnected.

Uniform spaces

Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.

Local Notation "'to_set' A x" := ([set y | A (x, y)])
  (at level 0, A at level 0) : classical_set_scope.

Definition nbhs_ {T T'} (ent : set_system (T * T')) (x : T) :=
  filter_from ent (fun A => to_set A x).

Lemma nbhs_E {T T'} (ent : set_system (T * T')) x :
  nbhs_ ent x = filter_from ent (fun A => to_set A x).
Proof.

HB.mixin Record Nbhs_isUniform_mixin M of Nbhs M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_refl_subproof : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
  entourage_inv_subproof : forall A, entourage A -> entourage (A^-1)%classic;
  entourage_split_ex_subproof :
    forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
  nbhsE_subproof : nbhs = nbhs_ entourage;
}.

#[short(type="uniformType")]
HB.structure Definition Uniform :=
  {T of Topological T & Nbhs_isUniform_mixin T}.

HB.factory Record Nbhs_isUniform M of Nbhs M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
  entourage_inv : forall A, entourage A -> entourage (A^-1)%classic;
  entourage_split_ex :
    forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
  nbhsE : nbhs = nbhs_ entourage;
}.

HB.builders Context M of Nbhs_isUniform M.

Lemma nbhs_filter (p : M) : ProperFilter (nbhs p).
Proof.

Lemma nbhs_singleton (p : M) A : nbhs p A -> A p.
Proof.

Lemma nbhs_nbhs (p : M) A : nbhs p A -> nbhs p (nbhs^~ A).
Proof.

HB.instance Definition _ := Nbhs_isNbhsTopological.Build M
  nbhs_filter nbhs_singleton nbhs_nbhs.

HB.instance Definition _ := Nbhs_isUniform_mixin.Build M
  entourage_filter entourage_refl entourage_inv entourage_split_ex nbhsE.

HB.end.

HB.factory Record isUniform M of Pointed M := {
  entourage : set_system (M * M);
  entourage_filter : Filter entourage;
  entourage_refl : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A;
  entourage_inv : forall A, entourage A -> entourage (A^-1)%classic;
  entourage_split_ex :
    forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A;
}.

HB.builders Context M of isUniform M.
  HB.instance Definition _ := @hasNbhs.Build M (nbhs_ entourage).
  HB.instance Definition _ := @Nbhs_isUniform.Build M entourage
    entourage_filter entourage_refl entourage_inv entourage_split_ex erefl.
HB.end.

Lemma nbhs_entourageE {M : uniformType} : nbhs_ (@entourage M) = nbhs.
Proof.

Lemma entourage_sym {X Y : Type} E (x : X) (y : Y) :
  E (x, y) <-> (E ^-1)%classic (y, x).
Proof.

Lemma filter_from_entourageE {M : uniformType} x :
  filter_from (@entourage M) (fun A => to_set A x) = nbhs x.
Proof.

Module Export NbhsEntourage.
Definition nbhs_simpl :=
  (nbhs_simpl,@filter_from_entourageE,@nbhs_entourageE).
End NbhsEntourage.

Lemma nbhsP {M : uniformType} (x : M) P : nbhs x P <-> nbhs_ entourage x P.
Proof.

Lemma filter_inv {T : Type} (F : set (set (T * T))) :
  Filter F -> Filter [set (V^-1)%classic | V in F].
Proof.

Section uniformType1.
Context {M : uniformType}.

Lemma entourage_refl (A : set (M * M)) x :
  entourage A -> A (x, x).
Proof.

Global Instance entourage_pfilter : ProperFilter (@entourage M).
Proof.

Lemma entourageT : entourage [set: M * M].
Proof.

Lemma entourage_inv (A : set (M * M)) : entourage A -> entourage (A^-1)%classic.
Proof.

Lemma entourage_split_ex (A : set (M * M)) :
  entourage A -> exists2 B, entourage B & B \; B `<=` A.
Proof.

Definition split_ent (A : set (M * M)) :=
  get (entourage `&` [set B | B \; B `<=` A]).

Lemma split_entP (A : set (M * M)) : entourage A ->
  entourage (split_ent A) /\ split_ent A \; split_ent A `<=` A.
Proof.

Lemma entourage_split_ent (A : set (M * M)) : entourage A ->
  entourage (split_ent A).
Proof.

Lemma subset_split_ent (A : set (M * M)) : entourage A ->
  split_ent A \; split_ent A `<=` A.
Proof.

Lemma entourage_split (z x y : M) A : entourage A ->
  split_ent A (x,z) -> split_ent A (z,y) -> A (x,y).
Proof.

Lemma nbhs_entourage (x : M) A : entourage A -> nbhs x (to_set A x).
Proof.

Lemma cvg_entourageP F (FF : Filter F) (p : M) :
  F --> p <-> forall A, entourage A -> \forall q \near F, A (p, q).
Proof.

Lemma cvg_entourage {F} {FF : Filter F} (y : M) :
  F --> y -> forall A, entourage A -> \forall y' \near F, A (y,y').
Proof.

Lemma cvg_app_entourageP T (f : T -> M) F (FF : Filter F) p :
  f @ F --> p <-> forall A, entourage A -> \forall t \near F, A (p, f t).
Proof.

Lemma entourage_invI (E : set (M * M)) :
  entourage E -> entourage (E `&` E^-1)%classic.
Proof.

Lemma split_ent_subset (E : set (M * M)) : entourage E -> split_ent E `<=` E.
Proof.

End uniformType1.

#[global]
Hint Extern 0 (entourage (split_ent _)) => exact: entourage_split_ent : core.
#[global]
Hint Extern 0 (entourage (get _)) => exact: entourage_split_ent : core.
#[global]
Hint Extern 0 (entourage (_^-1)%classic) => exact: entourage_inv : core.
Arguments entourage_split {M} z {x y A}.
#[global]
Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core.

Lemma ent_closure {M : uniformType} (x : M) E : entourage E ->
  closure (to_set (split_ent E) x) `<=` to_set E x.
Proof.

Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x :
  {for x, continuous f} <-> f @ x^' --> f x.
Proof.

Definition countable_uniformity (T : uniformType) :=
  exists R : set (set (T * T)), [/\
    countable R,
    R `<=` entourage &
    forall P, entourage P -> exists2 Q, R Q & Q `<=` P].

Lemma countable_uniformityP {T : uniformType} :
  countable_uniformity T <-> exists2 f : nat -> set (T * T),
    (forall A, entourage A -> exists N, f N `<=` A) &
    (forall n, entourage (f n)).
Proof.

Section uniform_closeness.

Variable (U : uniformType).

Lemma open_nbhs_entourage (x : U) (A : set (U * U)) :
  entourage A -> open_nbhs x (to_set A x)^°.
Proof.

Lemma entourage_close (x y : U) : close x y = forall A, entourage A -> A (x, y).
Proof.

Lemma close_trans (y x z : U) : close x y -> close y z -> close x z.
Proof.

Lemma close_cvgxx (x y : U) : close x y -> x --> y.
Proof.

Lemma cvg_closeP (F : set_system U) (l : U) : ProperFilter F ->
  F --> l <-> ([cvg F in U] /\ close (lim F) l).
Proof.

End uniform_closeness.

Definition unif_continuous (U V : uniformType) (f : U -> V) :=
  (fun xy => (f xy.1, f xy.2)) @ entourage --> entourage.

product of two uniform spaces

Section prod_Uniform.

Context {U V : uniformType}.
Implicit Types A : set ((U * V) * (U * V)).

Definition prod_ent :=
  [set A : set ((U * V) * (U * V)) |
    filter_prod (@entourage U) (@entourage V)
    [set ((xy.1.1,xy.2.1),(xy.1.2,xy.2.2)) | xy in A]].

Lemma prod_entP (A : set (U * U)) (B : set (V * V)) :
  entourage A -> entourage B ->
  prod_ent [set xy | A (xy.1.1, xy.2.1) /\ B (xy.1.2, xy.2.2)].
Proof.

Lemma prod_ent_filter : Filter prod_ent.
Proof.

Lemma prod_ent_refl A : prod_ent A -> [set xy | xy.1 = xy.2] `<=` A.
Proof.

Lemma prod_ent_inv A : prod_ent A -> prod_ent (A^-1)%classic.
Proof.

Lemma prod_ent_split A : prod_ent A -> exists2 B, prod_ent B & B \; B `<=` A.
Proof.

Lemma prod_ent_nbhsE : nbhs = nbhs_ prod_ent.
Proof.

HB.instance Definition _ := Nbhs_isUniform.Build (U * V)%type
  prod_ent_filter prod_ent_refl prod_ent_inv prod_ent_split prod_ent_nbhsE.

End prod_Uniform.

matrices

Section matrix_Uniform.

Variables (m n : nat) (T : uniformType).

Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)).

Definition mx_ent :=
  filter_from
  [set P : 'I_m -> 'I_n -> set (T * T) | forall i j, entourage (P i j)]
  (fun P => [set MN : 'M[T]_(m, n) * 'M[T]_(m, n) |
    forall i j, P i j (MN.1 i j, MN.2 i j)]).

Lemma mx_ent_filter : Filter mx_ent.
Proof.

Lemma mx_ent_refl A : mx_ent A -> [set MN | MN.1 = MN.2] `<=` A.
Proof.

Lemma mx_ent_inv A : mx_ent A -> mx_ent (A^-1)%classic.
Proof.

Lemma mx_ent_split A : mx_ent A -> exists2 B, mx_ent B & B \; B `<=` A.
Proof.

Lemma mx_ent_nbhsE : nbhs = nbhs_ mx_ent.
Proof.

HB.instance Definition _ := Nbhs_isUniform.Build 'M[T]_(m, n)
  mx_ent_filter mx_ent_refl mx_ent_inv mx_ent_split mx_ent_nbhsE.

End matrix_Uniform.

Lemma cvg_mx_entourageP (T : uniformType) m n (F : set_system 'M[T]_(m,n))
  (FF : Filter F) (M : 'M[T]_(m,n)) :
  F --> M <->
  forall A, entourage A -> \forall N \near F,
  forall i j, A (M i j, (N : 'M[T]_(m,n)) i j).
Proof.

Functional metric spaces

Definition map_pair {S U} (f : S -> U) (x : (S * S)) : (U * U) :=
  (f x.1, f x.2).

Section weak_uniform.

Variable (pS : pointedType) (U : uniformType) (f : pS -> U).

Let S := weak_topology f.

Definition weak_ent : set_system (S * S) :=
  filter_from (@entourage U) (fun V => (map_pair f)@^-1` V).

Lemma weak_ent_filter : Filter weak_ent.
Proof.

Lemma weak_ent_refl A : weak_ent A -> [set fg | fg.1 = fg.2] `<=` A.
Proof.

Lemma weak_ent_inv A : weak_ent A -> weak_ent (A^-1)%classic.
Proof.

Lemma weak_ent_split A : weak_ent A -> exists2 B, weak_ent B & B \; B `<=` A.
Proof.

Lemma weak_ent_nbhs : nbhs = nbhs_ weak_ent.
Proof.

HB.instance Definition _ := @Nbhs_isUniform.Build (weak_topology f)
  weak_ent weak_ent_filter weak_ent_refl weak_ent_inv weak_ent_split weak_ent_nbhs.

End weak_uniform.

Section fct_Uniform.

Variable (T : choiceType) (U : uniformType).

Definition fct_ent :=
  filter_from
  (@entourage U)
  (fun P => [set fg | forall t : T, P (fg.1 t, fg.2 t)]).

Lemma fct_ent_filter : Filter fct_ent.
Proof.

Lemma fct_ent_refl A : fct_ent A -> [set fg | fg.1 = fg.2] `<=` A.
Proof.

Lemma fct_ent_inv A : fct_ent A -> fct_ent (A^-1)%classic.
Proof.

Lemma fct_ent_split A : fct_ent A -> exists2 B, fct_ent B & B \; B `<=` A.
Proof.

Definition arrow_uniform := isUniform.Build (T -> U)
  fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split.

End fct_Uniform.

Module Import DefaultUniformFun.
HB.instance Definition _ T U := @arrow_uniform T U.
End DefaultUniformFun.

Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType)
  (F : set_system (T -> U)) (FF : Filter F) (f : T -> U) :
  F --> f <->
  forall A, entourage A ->
  \forall g \near F, forall t, A (f t, g t).
Proof.

Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) :=
  exists2 B, entourage B & forall PQ, A PQ -> forall p q,
    PQ.1 p -> PQ.2 q -> B (p,q).

Section sup_uniform.

Variable (T : pointedType) (Ii : Type) (Tc : Ii -> Uniform T).

Let I : choiceType := {classic Ii}.
Let TS := fun i => Uniform.Pack (Tc i).
Notation Tt := (sup_topology Tc).
Let ent_of (p : I * set (T * T)) := `[< @entourage (TS p.1) p.2>].
Let IEntType := {p : (I * set (T * T)) | ent_of p}.
Let IEnt : choiceType := IEntType.

Local Lemma IEnt_pointT (i : I) : ent_of (i, setT).
Proof.

Definition sup_ent : set_system (T * T) :=
  filter_from (finI_from [set: IEnt] (fun p => (projT1 p).2)) id.

Ltac IEntP := move=> [[ /= + + /[dup] /asboolP]].

Definition sup_ent_filter : Filter sup_ent.
Proof.

Lemma sup_ent_refl A : sup_ent A -> [set fg | fg.1 = fg.2] `<=` A.
Proof.

Lemma sup_ent_inv A : sup_ent A -> sup_ent (A^-1)%classic.
Proof.

Lemma sup_ent_split A : sup_ent A -> exists2 B, sup_ent B & B \; B `<=` A.
Proof.

Lemma sup_ent_nbhs : @nbhs Tt Tt = nbhs_ sup_ent.
Proof.

HB.instance Definition _ := @Nbhs_isUniform.Build Tt sup_ent
   sup_ent_filter sup_ent_refl sup_ent_inv sup_ent_split sup_ent_nbhs.

Lemma countable_sup_ent :
  countable [set: Ii] -> (forall n, countable_uniformity (TS n)) ->
  countable_uniformity Tt.
Proof.

End sup_uniform.

HB.instance Definition _ (I : Type) (T : I -> uniformType) :=
  Uniform.copy (prod_topology T)
    (sup_topology (fun i => Uniform.class
      [the uniformType of weak_topology (@proj _ T i)])).

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

Lemma entourage_E {R : numDomainType} {T T'} (ball : T -> R -> set T') :
  entourage_ ball =
  @filter_from R _ [set x | 0 < x] (fun e => [set xy | ball xy.1 e xy.2]).
Proof.

HB.mixin Record Uniform_isPseudoMetric (R : numDomainType) M of Uniform M := {
  ball : M -> R -> M -> Prop ;
  ball_center_subproof : forall x (e : R), 0 < e -> ball x e x ;
  ball_sym_subproof : forall x y (e : R), ball x e y -> ball y e x ;
  ball_triangle_subproof :
    forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z;
  entourageE_subproof : entourage = entourage_ ball
}.

#[short(type="pseudoMetricType")]
HB.structure Definition PseudoMetric (R : numDomainType) :=
  {T of Uniform T & Uniform_isPseudoMetric R T}.

Definition discrete_topology T (dsc : discrete_space T) : Type := T.

Section discrete_uniform.

Context {T : nbhsType} {dsc: discrete_space T}.

Definition discrete_ent : set (set (T * T)) :=
  globally (range (fun x => (x, x))).

Program Definition discrete_uniform_mixin :=
  @isUniform.Build (discrete_topology dsc) discrete_ent _ _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.

HB.instance Definition _ := Choice.on (discrete_topology dsc).
HB.instance Definition _ := Pointed.on (discrete_topology dsc).
HB.instance Definition _ := discrete_uniform_mixin.

End discrete_uniform.

HB.factory Record Nbhs_isPseudoMetric (R : numFieldType) M of Nbhs M := {
  ent : set_system (M * M);
  nbhsE : nbhs = nbhs_ ent;
  ball : M -> R -> M -> Prop ;
  ball_center : forall x (e : R), 0 < e -> ball x e x ;
  ball_sym : forall x y (e : R), ball x e y -> ball y e x ;
  ball_triangle :
    forall x y z e1 e2, ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z;
  entourageE : ent = entourage_ ball
}.

HB.builders Context R M of Nbhs_isPseudoMetric R M.

Lemma ball_le x : {homo ball x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
Proof.

Lemma entourage_filter_subproof : Filter ent.
Proof.

Lemma ball_sym_subproof A : ent A -> [set xy | xy.1 = xy.2] `<=` A.
Proof.

Lemma ball_triangle_subproof A : ent A -> ent (A^-1)%classic.
Proof.

Lemma entourageE_subproof A : ent A -> exists2 B, ent B & B \; B `<=` A.
Proof.

HB.instance Definition _ := Nbhs_isUniform.Build M
  entourage_filter_subproof ball_sym_subproof ball_triangle_subproof
  entourageE_subproof nbhsE.

HB.instance Definition _ := Uniform_isPseudoMetric.Build R M
  ball_center ball_sym ball_triangle entourageE.

HB.end.

Lemma entourage_ballE {R : numDomainType} {M : pseudoMetricType R} : entourage_ (@ball R M) = entourage.
Proof.

Lemma entourage_from_ballE {R : numDomainType} {M : pseudoMetricType R} :
  @filter_from R _ [set x : R | 0 < x]
    (fun e => [set xy | @ball R M xy.1 e xy.2]) = entourage.
Proof.

Lemma entourage_ball {R : numDomainType} (M : pseudoMetricType R)
  (e : {posnum R}) : entourage [set xy : M * M | ball xy.1 e%:num xy.2].
Proof.
#[global] Hint Resolve entourage_ball : core.

Definition nbhs_ball_ {R : numDomainType} {T T'} (ball : T -> R -> set T')
  (x : T) := @filter_from R _ [set e | e > 0] (ball x).

Definition nbhs_ball {R : numDomainType} {M : pseudoMetricType R} :=
  nbhs_ball_ (@ball R M).

Lemma nbhs_ballE {R : numDomainType} {M : pseudoMetricType R} : (@nbhs_ball R M) = nbhs.
Proof.

Lemma filter_from_ballE {R : numDomainType} {M : pseudoMetricType R} x :
  @filter_from R _ [set x : R | 0 < x] (@ball R M x) = nbhs x.
Proof.

Module Export NbhsBall.
Definition nbhs_simpl := (nbhs_simpl,@filter_from_ballE,@nbhs_ballE).
End NbhsBall.

Lemma nbhs_ballP {R : numDomainType} {M : pseudoMetricType R} (x : M) P :
  nbhs x P <-> nbhs_ball x P.
Proof.

Lemma ball_center {R : numDomainType} (M : pseudoMetricType R) (x : M)
  (e : {posnum R}) : ball x e%:num x.
Proof.
#[global] Hint Resolve ball_center : core.

Section pseudoMetricType_numDomainType.
Context {R : numDomainType} {M : pseudoMetricType R}.

Lemma ballxx (x : M) (e : R) : 0 < e -> ball x e x.
Proof.

Lemma ball_sym (x y : M) (e : R) : ball x e y -> ball y e x.
Proof.

Lemma ball_symE (x y : M) (e : R) : ball x e y = ball y e x.
Proof.

Lemma ball_triangle (y x z : M) (e1 e2 : R) :
  ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z.
Proof.

Lemma nbhsx_ballx (x : M) (eps : R) : 0 < eps -> nbhs x (ball x eps).
Proof.

Lemma open_nbhs_ball (x : M) (eps : {posnum R}) : open_nbhs x ((ball x eps%:num)^°).
Proof.

Lemma le_ball (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2.
Proof.

Global Instance entourage_proper_filter : ProperFilter (@entourage M).
Proof.

Lemma near_ball (y : M) (eps : R) : 0 < eps -> \forall y' \near y, ball y eps y'.
Proof.

Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a).
Proof.

Lemma fcvg_ballP {F} {FF : Filter F} (y : M) :
  F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'.
Proof.

Lemma __deprecated__cvg_ballPpos {F} {FF : Filter F} (y : M) :
  F --> y <-> forall eps : {posnum R}, \forall y' \near F, ball y eps%:num y'.
Proof.
#[deprecated(since="mathcomp-analysis 0.6.0",
  note="use a combination of `cvg_ballP` and `posnumP`")]
Notation cvg_ballPpos := __deprecated__cvg_ballPpos (only parsing).

Lemma fcvg_ball {F} {FF : Filter F} (y : M) :
  F --> y -> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'.
Proof.

Lemma cvg_ballP {T} {F} {FF : Filter F} (f : T -> M) y :
  f @ F --> y <-> forall eps : R, 0 < eps -> \forall x \near F, ball y eps (f x).
Proof.

Lemma cvg_ball {T} {F} {FF : Filter F} (f : T -> M) y :
  f @ F --> y -> forall eps : R, 0 < eps -> \forall x \near F, ball y eps (f x).
Proof.

Lemma cvgi_ballP T {F} {FF : Filter F} (f : T -> M -> Prop) y :
  f `@ F --> y <->
  forall eps : R, 0 < eps -> \forall x \near F, exists z, f x z /\ ball y eps z.
Proof.
Definition cvg_toi_locally := @cvgi_ballP.

Lemma cvgi_ball T {F} {FF : Filter F} (f : T -> M -> Prop) y :
  f `@ F --> y ->
  forall eps : R, 0 < eps -> F [set x | exists z, f x z /\ ball y eps z].
Proof.

End pseudoMetricType_numDomainType.
#[global] Hint Resolve nbhsx_ballx : core.
#[global] Hint Resolve close_refl : core.
Arguments close_cvg {T} F1 F2 {FF2} _.

Arguments nbhsx_ballx {R M} x eps.
Arguments near_ball {R M} y eps.

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `cvg_ball`")]
Notation app_cvg_locally := cvg_ball (only parsing).

Section pseudoMetricType_numFieldType.
Context {R : numFieldType} {M : pseudoMetricType R}.

Lemma ball_split (z x y : M) (e : R) :
  ball x (e / 2) z -> ball z (e / 2) y -> ball x e y.
Proof.

Lemma ball_splitr (z x y : M) (e : R) :
  ball z (e / 2) x -> ball z (e / 2) y -> ball x e y.
Proof.

Lemma ball_splitl (z x y : M) (e : R) :
  ball x (e / 2) z -> ball y (e / 2) z -> ball x e y.
Proof.

Lemma ball_close (x y : M) :
  close x y = forall eps : {posnum R}, ball x eps%:num y.
Proof.

End pseudoMetricType_numFieldType.

Section ball_hausdorff.
Variables (R : numDomainType) (T : pseudoMetricType R).

Lemma ball_hausdorff : hausdorff_space T =
  forall (a b : T), a != b ->
  exists r : {posnum R} * {posnum R},
    ball a r.1%:num `&` ball b r.2%:num == set0.
Proof.
End ball_hausdorff.

Section entourages.
Variable R : numDomainType.
Lemma unif_continuousP (U V : pseudoMetricType R) (f : U -> V) :
  unif_continuous f <->
  forall e, e > 0 -> exists2 d, d > 0 &
    forall x, ball x.1 d x.2 -> ball (f x.1) e (f x.2).
Proof.
End entourages.

Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} :
  countable_uniformity T.
Proof.

Specific pseudoMetric spaces

matrices
Section matrix_PseudoMetric.
Variables (m n : nat) (R : numDomainType) (T : pseudoMetricType R).
Implicit Types x y : 'M[T]_(m, n).
Definition mx_ball x (e : R) y := forall i j, ball (x i j) e (y i j).
Lemma mx_ball_center x (e : R) : 0 < e -> mx_ball x e x.
Proof.
Lemma mx_ball_sym x y (e : R) : mx_ball x e y -> mx_ball y e x.
Proof.
Lemma mx_ball_triangle x y z (e1 e2 : R) :
  mx_ball x e1 y -> mx_ball y e2 z -> mx_ball x (e1 + e2) z.
Proof.

Lemma mx_entourage : entourage = entourage_ mx_ball.
Proof.

HB.instance Definition _ := Uniform_isPseudoMetric.Build R 'M[T]_(m, n)
  mx_ball_center mx_ball_sym mx_ball_triangle mx_entourage.
End matrix_PseudoMetric.

product of two pseudoMetric spaces
Section prod_PseudoMetric.
Context {R : numDomainType} {U V : pseudoMetricType R}.
Implicit Types (x y : U * V).
Definition prod_point : U * V := (point, point).
Definition prod_ball x (eps : R) y :=
  ball (fst x) eps (fst y) /\ ball (snd x) eps (snd y).
Lemma prod_ball_center x (eps : R) : 0 < eps -> prod_ball x eps x.
Proof.
Lemma prod_ball_sym x y (eps : R) : prod_ball x eps y -> prod_ball y eps x.
Proof.
Lemma prod_ball_triangle x y z (e1 e2 : R) :
  prod_ball x e1 y -> prod_ball y e2 z -> prod_ball x (e1 + e2) z.
Proof.
Lemma prod_entourage : entourage = entourage_ prod_ball.
Proof.

HB.instance Definition _ := Uniform_isPseudoMetric.Build R (U * V)%type
  prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage.
End prod_PseudoMetric.

Section Nbhs_fct2.
Context {T : Type} {R : numDomainType} {U V : pseudoMetricType R}.
Lemma fcvg_ball2P {F : set_system U} {G : set_system V}
  {FF : Filter F} {FG : Filter G} (y : U) (z : V):
  (F, G) --> (y, z) <->
  forall eps : R, eps > 0 -> \forall y' \near F & z' \near G,
                ball y eps y' /\ ball z eps z'.
Proof.

Lemma cvg_ball2P {I J} {F : set_system I} {G : set_system J}
  {FF : Filter F} {FG : Filter G} (f : I -> U) (g : J -> V) (y : U) (z : V):
  (f @ F, g @ G) --> (y, z) <->
  forall eps : R, eps > 0 -> \forall i \near F & j \near G,
                ball y eps (f i) /\ ball z eps (g j).
Proof.

End Nbhs_fct2.

Functional metric spaces
Section fct_PseudoMetric.
Variable (T : choiceType) (R : numFieldType) (U : pseudoMetricType R).
Definition fct_ball (x : T -> U) (eps : R) (y : T -> U) :=
  forall t : T, ball (x t) eps (y t).
Lemma fct_ball_center (x : T -> U) (e : R) : 0 < e -> fct_ball x e x.
Proof.

Lemma fct_ball_sym (x y : T -> U) (e : R) : fct_ball x e y -> fct_ball y e x.
Proof.
Lemma fct_ball_triangle (x y z : T -> U) (e1 e2 : R) :
  fct_ball x e1 y -> fct_ball y e2 z -> fct_ball x (e1 + e2) z.
Proof.
Lemma fct_entourage : entourage = entourage_ fct_ball.
Proof.

HB.instance Definition _ := Uniform_isPseudoMetric.Build R (T -> U)
  fct_ball_center fct_ball_sym fct_ball_triangle fct_entourage.
End fct_PseudoMetric.

Definition quotient_topology (T : topologicalType) (Q : quotType T) : Type := Q.

Section quotients.
Local Open Scope quotient_scope.
Context {T : topologicalType} {Q0 : quotType T}.

Local Notation Q := (quotient_topology Q0).

HB.instance Definition _ := Quotient.copy Q Q0.
HB.instance Definition _ := [Sub Q of T by %/].
HB.instance Definition _ := [Choice of Q by <:].
HB.instance Definition _ := isPointed.Build Q (\pi_Q point : Q).

Definition quotient_open U := open (\pi_Q @^-1` U).

Program Definition quotient_topologicalType_mixin :=
  @Pointed_isOpenTopological.Build Q quotient_open _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
HB.instance Definition _ := quotient_topologicalType_mixin.

Lemma pi_continuous : continuous (\pi_Q : T -> Q).
Proof.

Lemma quotient_continuous {Z : topologicalType} (f : Q -> Z) :
  continuous f <-> continuous (f \o \pi_Q).
Proof.

Lemma repr_comp_continuous (Z : topologicalType) (g : T -> Z) :
  continuous g -> {homo g : a b / \pi_Q a == \pi_Q b :> Q >-> a == b} ->
  continuous (g \o repr : Q -> Z).
Proof.

End quotients.

Section discrete_pseudoMetric.
Context {R : numDomainType} {T : nbhsType} {dsc : discrete_space T}.

Definition discrete_ball (x : T) (eps : R) y : Prop := x = y.

Lemma discrete_ball_center x (eps : R) : 0 < eps -> discrete_ball x eps x.
Proof.

Program Definition discrete_pseudometric_mixin :=
  @Uniform_isPseudoMetric.Build R (discrete_topology dsc) discrete_ball
    _ _ _ _.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.

HB.instance Definition _ := discrete_pseudometric_mixin.

End discrete_pseudoMetric.

Definition pseudoMetric_bool {R : realType} :=
  [the pseudoMetricType R of discrete_topology discrete_bool : Type].

Complete uniform spaces

Definition cauchy {T : uniformType} (F : set_system T) := (F, F) --> entourage.

Lemma cvg_cauchy {T : uniformType} (F : set_system T) : Filter F ->
  [cvg F in T] -> cauchy F.
Proof.

HB.mixin Record Uniform_isComplete T of Uniform T := {
  cauchy_cvg :
    forall (F : set_system T), ProperFilter F -> cauchy F -> cvg F
}.

#[short(type="completeType")]
HB.structure Definition Complete := {T of Uniform T & Uniform_isComplete T}.

#[deprecated(since="mathcomp-analysis 2.0", note="use cauchy_cvg instead")]
Notation complete_ax := cauchy_cvg (only parsing).

Section completeType1.

Context {T : completeType}.

Lemma cauchy_cvgP (F : set_system T) (FF : ProperFilter F) : cauchy F <-> cvg F.
Proof.

End completeType1.
Arguments cauchy_cvg {T} F {FF} _ : rename.
Arguments cauchy_cvgP {T} F {FF}.

Section matrix_Complete.

Variables (T : completeType) (m n : nat).

Lemma mx_complete (F : set_system 'M[T]_(m, n)) :
  ProperFilter F -> cauchy F -> cvg F.
Proof.

HB.instance Definition _ := Uniform_isComplete.Build 'M[T]_(m, n) mx_complete.

End matrix_Complete.

Section fun_Complete.

Context {T : choiceType} {U : completeType}.

Lemma fun_complete (F : set_system (T -> U))
  {FF : ProperFilter F} : cauchy F -> cvg F.
Proof.

HB.instance Definition _ := Uniform_isComplete.Build (T -> U) fun_complete.

End fun_Complete.

Limit switching
Section Cvg_switch.
Context {T1 T2 : choiceType}.
Lemma cvg_switch_1 {U : uniformType}
  F1 {FF1 : ProperFilter F1} F2 {FF2 : Filter F2}
  (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) (l : U) :
  f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> h @ F1 --> l ->
  g @ F2 --> l.
Proof.

Lemma cvg_switch_2 {U : completeType}
  F1 {FF1 : ProperFilter F1} F2 {FF2 : ProperFilter F2}
  (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) :
  f @ F1 --> g -> (forall x, f x @ F2 --> h x) ->
  [cvg h @ F1 in U].
Proof.

Lemma cvg_switch {U : completeType}
  F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2)
  (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) :
  f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) ->
  exists l : U, h @ F1 --> l /\ g @ F2 --> l.
Proof.

End Cvg_switch.

Complete pseudoMetric spaces

Definition cauchy_ex {R : numDomainType} {T : pseudoMetricType R} (F : set_system T) :=
  forall eps : R, 0 < eps -> exists x, F (ball x eps).

Definition cauchy_ball {R : numDomainType} {T : pseudoMetricType R} (F : set_system T) :=
  forall e, e > 0 -> \forall x & y \near F, ball x e y.

Lemma cauchy_ballP (R : numDomainType) (T : pseudoMetricType R)
    (F : set_system T) (FF : Filter F) :
  cauchy_ball F <-> cauchy F.
Proof.
Arguments cauchy_ballP {R T} F {FF}.

Lemma cauchy_exP (R : numFieldType) (T : pseudoMetricType R)
    (F : set_system T) (FF : Filter F) :
  cauchy_ex F -> cauchy F.
Proof.
Arguments cauchy_exP {R T} F {FF}.

Lemma cauchyP (R : numFieldType) (T : pseudoMetricType R)
    (F : set_system T) (PF : ProperFilter F) :
  cauchy F <-> cauchy_ex F.
Proof.
Arguments cauchyP {R T} F {PF}.

#[short(type="completePseudoMetricType")]
HB.structure Definition CompletePseudoMetric R :=
  {T of Complete T & PseudoMetric R T}.

HB.instance Definition _ (R : numFieldType) (T : completePseudoMetricType R)
  (m n : nat) := Uniform_isComplete.Build 'M[T]_(m, n) cauchy_cvg.

HB.instance Definition _ (T : choiceType) (R : numFieldType)
    (U : completePseudoMetricType R) :=
  Uniform_isComplete.Build (T -> U) cauchy_cvg.

HB.instance Definition _ (R : zmodType) := isPointed.Build R 0.

Lemma compact_cauchy_cvg {T : uniformType} (U : set T) (F : set_system T) :
  ProperFilter F -> cauchy F -> F U -> compact U -> cvg F.
Proof.

Definition ball_
  (R : numDomainType) (V : zmodType) (norm : V -> R) (x : V) (e : R) :=
  [set y | norm (x - y) < e].
Arguments ball_ {R} {V} norm x e%R y /.

Lemma subset_ball_prop_in_itv (R : realDomainType) (x : R) e P :
  (ball_ Num.Def.normr x e `<=` P)%classic <->
  {in `](x - e), (x + e)[, forall y, P y}.
Proof.

Lemma subset_ball_prop_in_itvcc (R : realDomainType) (x : R) e P : 0 < e ->
  (ball_ Num.Def.normr x (2 * e) `<=` P)%classic ->
  {in `[(x - e), (x + e)], forall y, P y}.
Proof.

Global Instance ball_filter (R : realDomainType) (t : R) : Filter
  [set P | exists2 i : R, 0 < i & ball_ Num.norm t i `<=` P].
Proof.

#[global] Hint Extern 0 (Filter [set P | exists2 i, _ & ball_ _ _ i `<=` P]) =>
  (apply: ball_filter) : typeclass_instances.

Section pseudoMetric_of_normedDomain.
Context {K : numDomainType} {R : normedZmodType K}.
Lemma ball_norm_center (x : R) (e : K) : 0 < e -> ball_ Num.norm x e x.
Proof.
Lemma ball_norm_symmetric (x y : R) (e : K) :
  ball_ Num.norm x e y -> ball_ Num.norm y e x.
Proof.
Lemma ball_norm_triangle (x y z : R) (e1 e2 : K) :
  ball_ Num.norm x e1 y -> ball_ Num.norm y e2 z -> ball_ Num.norm x (e1 + e2) z.
Proof.

Lemma nbhs_ball_normE :
  @nbhs_ball_ K R R (ball_ Num.norm) = nbhs_ (entourage_ (ball_ Num.norm)).
Proof.
End pseudoMetric_of_normedDomain.

HB.instance Definition _ (R : zmodType) := Pointed.on R^o.

HB.instance Definition _ (R : numDomainType) := hasNbhs.Build R^o
  (nbhs_ball_ (ball_ (fun x => `|x|))).

HB.instance Definition _ (R : numFieldType) :=
  Nbhs_isPseudoMetric.Build R R^o
    nbhs_ball_normE ball_norm_center ball_norm_symmetric ball_norm_triangle erefl.

Module numFieldTopology.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : realType) := PseudoMetric.copy R R^o.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : rcfType) := PseudoMetric.copy R R^o.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : archiFieldType) := PseudoMetric.copy R R^o.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : realFieldType) := PseudoMetric.copy R R^o.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : numClosedFieldType) := PseudoMetric.copy R R^o.

#[export, non_forgetful_inheritance]
HB.instance Definition _ (R : numFieldType) := PseudoMetric.copy R R^o.

Module Exports. HB.reexport. End Exports.

End numFieldTopology.
Import numFieldTopology.Exports.

Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) :
  ProperFilter x^'.
Proof.

Definition uniform_fun {U : Type} (A : set U) (V : Type) := U -> V.

Notation "{ 'uniform`' A -> V }" := (@uniform_fun _ A V) : type_scope.
Notation "{ 'uniform' U -> V }" := ({uniform` [set: U] -> V}) : type_scope.
Notation "{ 'uniform' A , F --> f }" :=
  (cvg_to F (nbhs (f : {uniform` A -> _}))) : classical_set_scope.
Notation "{ 'uniform' , F --> f }" :=
  (cvg_to F (nbhs (f : {uniform _ -> _}))) : classical_set_scope.

Module Export UniformFun.
HB.instance Definition _ (U : choiceType) (A : set U) (V : uniformType) :=
  Uniform.copy {uniform` A -> V} (weak_topology (@sigL _ V A)).
End UniformFun.

Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
Proof.

Section RestrictedUniformTopology.
Context {U : choiceType} (A : set U) {V : uniformType} .

Lemma uniform_nbhs (f : {uniform` A -> V}) P:
  nbhs f P <-> (exists E, entourage E /\
    [set h | forall y, A y -> E(f y, h y)] `<=` P).
Proof.

Lemma uniform_entourage :
  @entourage [the uniformType of {uniform` A -> V}] =
  filter_from
    (@entourage V)
    (fun P => [set fg | forall t : U, A t -> P (fg.1 t, fg.2 t)]).
Proof.

End RestrictedUniformTopology.


Lemma restricted_cvgE {U : choiceType} {V : uniformType}
    (F : set_system (U -> V)) A (f : U -> V) :
  {uniform A, F --> f} = (F --> (f : {uniform` A -> V})).
Proof.

Definition pointwise_fun (U V : Type) := U -> V.
Notation "{ 'ptws' U -> V }" := (@pointwise_fun U V) : type_scope.
Notation "{ 'ptws' , F --> f }" :=
  (cvg_to F (nbhs (f : {ptws _ -> _}))) : classical_set_scope.

Module Export PtwsFun.
HB.instance Definition _ (U : Type) (V : topologicalType) :=
  Topological.copy {ptws U -> V} (prod_topology (fun _ : U => V)).
End PtwsFun.

Lemma pointwise_cvgE {U : Type} {V : topologicalType}
    (F : set_system (U -> V)) (A : set U) (f : U -> V) :
  {ptws, F --> f} = (F --> (f : {ptws U -> V})).
Proof.

Definition uniform_fun_family {U} V (fam : set U -> Prop) := U -> V.

Notation "{ 'family' fam , U -> V }" := (@uniform_fun_family U V fam).
Notation "{ 'family' fam , F --> f }" :=
  (cvg_to F (@nbhs _ {family fam, _ -> _} f)) : type_scope.

Module Export FamilyFun.
HB.instance Definition _
    {U : choiceType} {V : uniformType} (fam : set U -> Prop) :=
  Uniform.copy {family fam, U -> V}
    (sup_topology (fun k : sigT fam =>
       Uniform.class [the uniformType of {uniform` projT1 k -> V}])).
End FamilyFun.

Section UniformCvgLemmas.
Context {U : choiceType} {V : uniformType}.

Lemma uniform_set1 F (f : U -> V) (x : U) :
  Filter F -> {uniform [set x], F --> f} = (g x @[g --> F] --> f x).
Proof.

Lemma uniform_subset_nbhs (f : U -> V) (A B : set U) :
  B `<=` A -> nbhs (f : {uniform` A -> V}) `=>` nbhs (f : {uniform` B -> V}).
Proof.

Lemma uniform_subset_cvg (f : U -> V) (A B : set U) F :
  Filter F -> B `<=` A -> {uniform A, F --> f} -> {uniform B, F --> f}.
Proof.

Lemma pointwise_uniform_cvg (f : U -> V) (F : set_system (U -> V)) :
  Filter F -> {uniform, F --> f} -> {ptws, F --> f}.
Proof.

Lemma cvg_sigL (A : set U) (f : U -> V) (F : set_system (U -> V)) :
    Filter F ->
  {uniform A, F --> f} <->
  {uniform, sigL A @ F --> sigL A f}.
Proof.

Lemma eq_in_close (A : set U) (f g : {uniform` A -> V}) :
  {in A, f =1 g} -> close f g.
Proof.

Lemma hausdorrf_close_eq_in (A : set U) (f g : {uniform` A -> V}) :
  hausdorff_space V -> close f g = {in A, f =1 g}.
Proof.

Lemma uniform_restrict_cvg
    (F : set_system (U -> V)) (f : U -> V) A : Filter F ->
  {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
Proof.

Lemma uniform_nbhsT (f : U -> V) :
  (nbhs (f : {uniform U -> V})) = nbhs (f : [the topologicalType of U -> V]).
Proof.

Lemma cvg_uniformU (f : U -> V) (F : set_system (U -> V)) A B : Filter F ->
  {uniform A, F --> f} -> {uniform B, F --> f} ->
  {uniform (A `|` B), F --> f}.
Proof.

Lemma cvg_uniform_set0 (F : set_system (U -> V)) (f : U -> V) : Filter F ->
  {uniform set0, F --> f}.
Proof.

Lemma fam_cvgP (fam : set U -> Prop) (F : set_system (U -> V)) (f : U -> V) :
  Filter F -> {family fam, F --> f} <->
  (forall A : set U, fam A -> {uniform A, F --> f }).
Proof.

Lemma family_cvg_subset (famA famB : set U -> Prop) (F : set_system (U -> V))
    (f : U -> V) : Filter F ->
  famA `<=` famB -> {family famB, F --> f} -> {family famA, F --> f}.
Proof.

Lemma family_cvg_finite_covers (famA famB : set U -> Prop)
  (F : set_system (U -> V)) (f : U -> V) : Filter F ->
  (forall P, famA P ->
    exists (I : choiceType) f,
      (forall i, famB (f i)) /\ finite_subset_cover [set: I] f P) ->
  {family famB, F --> f} -> {family famA, F --> f}.
Proof.

End UniformCvgLemmas.

Lemma fam_cvgE {U : choiceType} {V : uniformType} (F : set_system (U -> V))
    (f : U -> V) fam :
  {family fam, F --> f} = (F --> (f : {family fam, U -> V})).
Proof.

Lemma fam_nbhs {U : choiceType} {V : uniformType} (fam : set U -> Prop)
    (A : set U) (E : set (V * V)) (f : {family fam, U -> V}) :
  entourage E -> fam A -> nbhs f [set g | forall y, A y -> E (f y, g y)].
Proof.

Lemma fam_compact_nbhs {U : topologicalType} {V : uniformType}
    (A : set U) (O : set V) (f : {family compact, U -> V}) :
  open O -> f @` A `<=` O -> compact A -> continuous f ->
  nbhs (f : {family compact, U -> V}) [set g | forall y, A y -> O (g y)].
Proof.

It turns out {family compact, U -> V} can be generalized to only assume topologicalType on V. This topology is called the compact-open topology. This topology is special because it is the only topology that will allow curry/uncurry to be continuous.


Section compact_open.
Context {T U : topologicalType}.

Definition compact_open : Type := T -> U.

Section compact_open_setwise.
Context {K : set T}.

Definition compact_openK := let _ := K in compact_open.

Definition compact_openK_nbhs (f : compact_openK) :=
  filter_from
    [set O | f @` K `<=` O /\ open O]
    (fun O => [set g | g @` K `<=` O]).

Global Instance compact_openK_nbhs_filter (f : compact_openK) :
  ProperFilter (compact_openK_nbhs f).
Proof.

HB.instance Definition _ := Pointed.on compact_openK.

HB.instance Definition _ := hasNbhs.Build compact_openK compact_openK_nbhs.

Definition compact_open_of_nbhs := [set A : set compact_openK | A `<=` nbhs^~ A].

Lemma compact_openK_nbhsE_subproof (p : compact_openK) :
  compact_openK_nbhs p =
    [set A | exists B : set compact_openK,
      [/\ compact_open_of_nbhs B, B p & B `<=` A]].
Proof.

Lemma compact_openK_openE_subproof :
  compact_open_of_nbhs = [set A | A `<=` compact_openK_nbhs^~ A].
Proof.

HB.instance Definition _ :=
  Nbhs_isTopological.Build compact_openK compact_openK_nbhs_filter
  compact_openK_nbhsE_subproof compact_openK_openE_subproof.

End compact_open_setwise.

HB.instance Definition _ := Pointed.on compact_open.

Definition compact_open_def :=
  sup_topology (fun i : sigT (@compact T) =>
    Topological.class (@compact_openK (projT1 i))).

HB.instance Definition _ := Nbhs.copy compact_open compact_open_def.

HB.instance Definition _ : Nbhs_isTopological compact_open :=
  Topological.copy compact_open compact_open_def.

Lemma compact_open_cvgP (F : set_system compact_open)
    (f : compact_open) :
  Filter F ->
  F --> f <-> forall K O, @compact T K -> @open U O -> f @` K `<=` O ->
    F [set g | g @` K `<=` O].
Proof.

Lemma compact_open_open (K : set T) (O : set U) :
  compact K -> open O -> open ([set g | g @` K `<=` O] : set compact_open).
Proof.

End compact_open.

Lemma compact_closedI {T : topologicalType} (A B : set T) :
  compact A -> closed B -> compact (A `&` B).
Proof.

Notation "{ 'compact-open' , U -> V }" := (@compact_open U V).
Notation "{ 'compact-open' , F --> f }" :=
  (F --> (f : @compact_open _ _)).

Section compact_open_uniform.
Context {U : topologicalType} {V : uniformType}.

Let small_ent_sub := @small_set_sub _ (@entourage V).

Lemma compact_open_fam_compactP (f : U -> V) (F : set_system (U -> V)) :
  continuous f -> Filter F ->
  {compact-open, F --> f} <-> {family compact, F --> f}.
Proof.

End compact_open_uniform.

Definition compactly_in {U : topologicalType} (A : set U) :=
  [set B | B `<=` A /\ compact B].

Lemma compact_cvg_within_compact {U : topologicalType} {V : uniformType}
    (C : set U) (F : set_system (U -> V)) (f : U -> V) :
  Filter F -> compact C ->
  {uniform C, F --> f} <-> {family compactly_in C, F --> f}.
Proof.

Global Instance Proper_dnbhs_numFieldType (R : numFieldType) (x : R) :
  ProperFilter x^'.
Proof.

Definition dense (T : topologicalType) (S : set T) :=
  forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.

Lemma denseNE (T : topologicalType) (S : set T) : ~ dense S ->
  exists O, (exists x, open_nbhs x O) /\ (O `&` S = set0).
Proof.

Lemma dense_rat (R : realType) : dense (@ratr R @` setT).
Proof.

Lemma separated_open_countable
    {R : realType} (I : Type) (B : I -> set R) (D : set I) :
    (forall i, open (B i)) -> (forall i, B i !=set0) ->
  trivIset D B -> countable D.
Proof.

Section weak_pseudoMetric.
Context {R : realType} (pS : pointedType) (U : pseudoMetricType R) .
Variable (f : pS -> U).

Notation S := (weak_topology f).

Definition weak_ball (x : S) (r : R) (y : S) := ball (f x) r (f y).

Lemma weak_pseudo_metric_ball_center (x : S) (e : R) : 0 < e -> weak_ball x e x.
Proof.

Lemma weak_pseudo_metric_entourageE : entourage = entourage_ weak_ball.
Proof.

HB.instance Definition _ := Uniform_isPseudoMetric.Build R S
  weak_pseudo_metric_ball_center (fun _ _ _ => @ball_sym _ _ _ _ _)
  (fun _ _ _ _ _ => @ball_triangle _ _ _ _ _ _ _)
  weak_pseudo_metric_entourageE.

Lemma weak_ballE (e : R) (x : S) : f@^-1` (ball (f x) e) = ball x e.
Proof.

End weak_pseudoMetric.

Lemma compact_second_countable {R : realType} {T : pseudoMetricType R} :
  compact [set: T] -> @second_countable T.
Proof.

Lemma clopen_surj {R : realType} {T : pseudoMetricType R} :
  compact [set: T] -> $|{surjfun [set: nat] >-> @clopen T}|.
Proof.

Module countable_uniform.
Section countable_uniform.
Context {R : realType} {T : uniformType}.

Hypothesis cnt_unif : @countable_uniformity T.

Let f_ := projT1 (cid2 (iffLR countable_uniformityP cnt_unif)).

Local Lemma countableBase : forall A, entourage A -> exists N, f_ N `<=` A.
Proof.

Let entF : forall n, entourage (f_ n).
Proof.


Local Fixpoint g_ (n : nat) : set (T * T) :=
  if n is S n then let W := split_ent (split_ent (g_ n)) `&` f_ n in W `&` W^-1
  else [set: T*T].

Let entG (n : nat) : entourage (g_ n).
Proof.

Local Lemma symG (n : nat) : ((g_ n)^-1)%classic = g_ n.
Proof.

Local Lemma descendG1 n : g_ n.+1 `<=` g_ n.
Proof.

Local Lemma descendG (n m : nat) : (m <= n)%N -> g_ n `<=` g_ m.
Proof.

Local Lemma splitG3 n : g_ n.+1 \; g_ n.+1 \; g_ n.+1 `<=` g_ n.
Proof.

Local Lemma gsubf n : g_ n.+1 `<=` f_ n.
Proof.

Local Lemma countableBaseG A : entourage A -> exists N, g_ N `<=` A.
Proof.


Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Local Definition distN (e : R) : nat := `|floor e^-1|%N.

Local Lemma distN0 : distN 0 = 0%N.
Proof.

Local Lemma distN_nat (n : nat): distN (n%:R^-1) = n.
Proof.

Local Lemma distN_le e1 e2 : e1 > 0 -> e1 <= e2 -> (distN e2 <= distN e1)%N.
Proof.

Local Fixpoint n_step_ball n x e z :=
  if n is n.+1 then exists y d1 d2,
    [/\ n_step_ball n x d1 y,
        0 < d1,
        0 < d2,
        g_ (distN d2) (y, z) &
        d1 + d2 = e]
  else e > 0 /\ g_ (distN e) (x, z).

Local Definition step_ball x e z := exists i, (n_step_ball i x e z).

Local Lemma n_step_ball_pos n x e z : n_step_ball n x e z -> 0 < e.
Proof.

Local Lemma step_ball_pos x e z : step_ball x e z -> 0 < e.
Proof.

Local Lemma entourage_nball e :
  0 < e -> entourage [set xy | step_ball xy.1 e xy.2].
Proof.

Local Lemma n_step_ball_center x e : 0 < e -> n_step_ball 0 x e x.
Proof.

Local Lemma step_ball_center x e : 0 < e -> step_ball x e x.
Proof.

Local Lemma n_step_ball_triangle n m x y z d1 d2 :
  n_step_ball n x d1 y ->
  n_step_ball m y d2 z ->
  n_step_ball (n + m).+1 x (d1 + d2) z.
Proof.

Local Lemma step_ball_triangle x y z d1 d2 :
  step_ball x d1 y -> step_ball y d2 z -> step_ball x (d1 + d2) z.
Proof.

Local Lemma n_step_ball_sym n x y e :
  n_step_ball n x e y -> n_step_ball n y e x.
Proof.

Local Lemma step_ball_sym x y e : step_ball x e y -> step_ball y e x.
Proof.


Local Lemma n_step_ball_le n x e1 e2 :
  e1 <= e2 -> n_step_ball n x e1 `<=` n_step_ball n x e2.
Proof.

Local Lemma step_ball_le x e1 e2 :
  e1 <= e2 -> step_ball x e1 `<=` step_ball x e2.
Proof.

Local Lemma distN_half (n : nat) : n.+1%:R^-1 / (2:R) <= n.+2%:R^-1.
Proof.

Local Lemma split_n_step_ball n x e1 e2 z :
  0 < e1 -> 0 < e2 -> n_step_ball n.+1 x (e1 + e2) z ->
    exists t1 t2 a b,
    [/\
      n_step_ball a x e1 t1,
      n_step_ball 0 t1 (e1 + e2) t2,
      n_step_ball b t2 e2 z &
      (a + b = n)%N
    ].
Proof.

Local Lemma n_step_ball_le_g x n :
  n_step_ball 0 x n%:R^-1 `<=` [set y | g_ n (x,y)].
Proof.

Local Lemma subset_n_step_ball n x N :
  n_step_ball n x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
Proof.

Local Lemma subset_step_ball x N :
  step_ball x N.+1%:R^-1 `<=` [set y | (g_ N) (x, y)].
Proof.

Local Lemma step_ball_entourage : entourage = entourage_ step_ball.
Proof.

Definition type : Type := let _ := countableBase in let _ := entF in T.

#[export] HB.instance Definition _ := Uniform.on type.
#[export] HB.instance Definition _ := Uniform_isPseudoMetric.Build R type
  step_ball_center step_ball_sym step_ball_triangle step_ball_entourage.

Lemma countable_uniform_bounded (x y : T) :
  let U := [the pseudoMetricType R of type]
  in @ball _ U x 2 y.
Proof.

End countable_uniform.
Module Exports. HB.reexport. End Exports.
End countable_uniform.
Export countable_uniform.Exports.

Notation countable_uniform := countable_uniform.type.

Definition sup_pseudometric (R : realType) (T : pointedType) (Ii : Type)
  (Tc : Ii -> PseudoMetric R T) (Icnt : countable [set: Ii]) : Type := T.

Section sup_pseudometric.
Variable (R : realType) (T : pointedType) (Ii : Type).
Variable (Tc : Ii -> PseudoMetric R T).

Hypothesis Icnt : countable [set: Ii].

Local Notation S := (sup_pseudometric Tc Icnt).

Let TS := fun i => PseudoMetric.Pack (Tc i).

Definition countable_uniformityT := @countable_sup_ent T Ii Tc Icnt
  (fun i => @countable_uniformity_metric _ (TS i)).

HB.instance Definition _ : PseudoMetric R S :=
  PseudoMetric.on (countable_uniform countable_uniformityT).

End sup_pseudometric.

HB.instance Definition _ (R : realType) (Ii : countType)
    (Tc : Ii -> pseudoMetricType R) := PseudoMetric.copy (prod_topology Tc)
  (sup_pseudometric (fun i => PseudoMetric.class
     [the pseudoMetricType R of weak_topology (@proj _ Tc i)]) (countableP _)).

Definition subspace {T : Type} (A : set T) := T.
Arguments subspace {T} _ : simpl never.

Definition incl_subspace {T A} (x : subspace A) : T := x.

Section Subspace.
Context {T : topologicalType} (A : set T).

Definition nbhs_subspace (x : subspace A) : set_system (subspace A) :=
  if x \in A then within A (nbhs x) else globally [set x].

Variant nbhs_subspace_spec x : Prop -> Prop -> bool -> set_system T -> Type :=
  | WithinSubspace :
      A x -> nbhs_subspace_spec x True False true (within A (nbhs x))
  | WithoutSubspace :
    ~ A x -> nbhs_subspace_spec x False True false (globally [set x]).

Lemma nbhs_subspaceP_subproof x :
  nbhs_subspace_spec x (A x) (~ A x) (x \in A) (nbhs_subspace x).
Proof.

Lemma nbhs_subspace_in (x : T) : A x -> within A (nbhs x) = nbhs_subspace x.
Proof.

Lemma nbhs_subspace_out (x : T) : ~ A x -> globally [set x] = nbhs_subspace x.
Proof.

Lemma nbhs_subspace_filter (x : subspace A) : ProperFilter (nbhs_subspace x).
Proof.

HB.instance Definition _ := Choice.copy (subspace A) _.

HB.instance Definition _ := isPointed.Build (subspace A) point.

HB.instance Definition _ := hasNbhs.Build (subspace A) nbhs_subspace.

Lemma nbhs_subspaceP (x : subspace A) :
  nbhs_subspace_spec x (A x) (~ A x) (x \in A) (nbhs x).
Proof.

Lemma nbhs_subspace_singleton (p : subspace A) B : nbhs p B -> B p.
Proof.

Lemma nbhs_subspace_nbhs (p : subspace A) B : nbhs p B -> nbhs p (nbhs^~ B).
Proof.

HB.instance Definition _ := Nbhs_isNbhsTopological.Build (subspace A)
  nbhs_subspace_filter nbhs_subspace_singleton nbhs_subspace_nbhs.

Lemma subspace_cvgP (F : set_system T) (x : T) : Filter F -> A x ->
  (F --> (x : subspace A)) <-> (F --> within A (nbhs x)).
Proof.

Lemma subspace_continuousP {S : topologicalType} (f : T -> S) :
  continuous (f : subspace A -> S) <->
  (forall x, A x -> f @ within A (nbhs x) --> f x) .
Proof.

Lemma subspace_eq_continuous {S : topologicalType} (f g : subspace A -> S) :
  {in A, f =1 g} -> continuous f -> continuous g.
Proof.

Lemma continuous_subspace_in {U : topologicalType} (f : subspace A -> U) :
  continuous f = {in A, continuous f}.
Proof.

Lemma nbhs_subspace_interior (x : T) :
  A^° x -> nbhs x = (nbhs (x : subspace A)).
Proof.

Lemma nbhs_subspace_ex (U : set T) (x : T) : A x ->
  nbhs (x : subspace A) U <->
  exists2 V, nbhs (x : T) V & U `&` A = V `&` A.
Proof.

Lemma incl_subspace_continuous : continuous incl_subspace.
Proof.

Section SubspaceOpen.

Lemma open_subspace1out (x : subspace A) : ~ A x -> open [set x].
Proof.

Lemma open_subspace_out (U : set (subspace A)) : U `<=` ~` A -> open U.
Proof.

Lemma open_subspaceT : open (A : set (subspace A)).
Proof.

Lemma open_subspaceIT (U : set (subspace A)) : open (U `&` A) = open U.
Proof.

Lemma open_subspaceTI (U : set (subspace A)) :
  open (A `&` U : set (subspace A)) = open U.
Proof.

Lemma closed_subspaceT : closed (A : set (subspace A)).
Proof.

Lemma open_subspaceP (U : set T) :
  open (U : set (subspace A)) <->
  exists V, open (V : set T) /\ V `&` A = U `&` A.
Proof.

Lemma closed_subspaceP (U : set T) :
  closed (U : set (subspace A)) <->
  exists V, closed (V : set T) /\ V `&` A = U `&` A.
Proof.

Lemma open_subspaceW (U : set T) :
  open (U : set T) -> open (U : set (subspace A)).
Proof.

Lemma closed_subspaceW (U : set T) :
  closed (U : set T) -> closed (U : set (subspace A)).
Proof.

Lemma open_setIS (U : set (subspace A)) : open A ->
  open (U `&` A : set T) = open U.
Proof.

Lemma open_setSI (U : set (subspace A)) : open A -> open (A `&` U) = open U.
Proof.

Lemma closed_setIS (U : set (subspace A)) : closed A ->
  closed (U `&` A : set T) = closed U.
Proof.

Lemma closed_setSI (U : set (subspace A)) :
  closed A -> closed (A `&` U) = closed U.
Proof.

Lemma closure_subspaceW (U : set T) :
  U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A.
Proof.

Lemma subspace_hausdorff :
  hausdorff_space T -> hausdorff_space [the topologicalType of subspace A].
Proof.
End SubspaceOpen.

Lemma compact_subspaceIP (U : set T) :
  compact (U `&` A : set (subspace A)) <-> compact (U `&` A : set T).
Proof.

Lemma clopen_connectedP : connected A <->
  (forall U, @clopen [the topologicalType of subspace A] U ->
    U `<=` A -> U !=set0 -> U = A).
Proof.

End Subspace.

Global Instance subspace_filter {T : topologicalType}
     (A : set T) (x : subspace A) :
   Filter (nbhs_subspace x) := nbhs_subspace_filter x.

Global Instance subspace_proper_filter {T : topologicalType}
     (A : set T) (x : subspace A) :
   ProperFilter (nbhs_subspace x) := nbhs_subspace_filter x.

Notation "{ 'within' A , 'continuous' f }" :=
  (continuous (f : subspace A -> _)) : classical_set_scope.

Arguments nbhs_subspaceP {T} A x.

Section SubspaceRelative.
Context {T : topologicalType}.
Implicit Types (U : topologicalType) (A B : set T).

Lemma nbhs_subspace_subset A B (x : T) :
  A `<=` B -> nbhs (x : subspace B) `<=` nbhs (x : subspace A).
Proof.

Lemma continuous_subspaceW {U} A B (f : T -> U) :
  A `<=` B ->
  {within B, continuous f} -> {within A, continuous f}.
Proof.

Lemma nbhs_subspaceT (x : T) : nbhs (x : subspace setT) = nbhs x.
Proof.

Lemma continuous_subspaceT_for {U} A (f : T -> U) (x : T) :
  A x -> {for x, continuous f} -> {for x, continuous (f : subspace A -> U)}.
Proof.

Lemma continuous_in_subspaceT {U} A (f : T -> U) :
  {in A, continuous f} -> {within A, continuous f}.
Proof.

Lemma continuous_subspaceT {U} A (f : T -> U) :
  continuous f -> {within A, continuous f}.
Proof.

Lemma continuous_open_subspace {U} A (f : T -> U) :
  open A -> {within A, continuous f} = {in A, continuous f}.
Proof.

Lemma continuous_inP {U} A (f : T -> U) : open A ->
  {in A, continuous f} <-> forall X, open X -> open (A `&` f @^-1` X).
Proof.

Lemma withinU_continuous {U} A B (f : T -> U) : closed A -> closed B ->
  {within A, continuous f} -> {within B, continuous f} ->
  {within A `|` B, continuous f}.
Proof.

Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) :
  {within A, continuous f} -> continuous (f : subspace A -> subspace B).
Proof.


Lemma continuous_subspace0 {U} (f : T -> U) : {within set0, continuous f}.
Proof.

Lemma continuous_subspace1 {U} (a : T) (f : T -> U) :
  {within [set a], continuous f}.
Proof.

End SubspaceRelative.

Section SubspaceUniform.
Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
Context {X : uniformType} (A : set X).

Definition subspace_ent :=
  filter_from (@entourage X)
  (fun E => [set xy | (xy.1 = xy.2) \/ (A xy.1 /\ A xy.2 /\ E xy)]).

Let Filter_subspace_ent : Filter subspace_ent.
Proof.

Let subspace_uniform_entourage_refl : forall X : set (subspace A * subspace A),
  subspace_ent X -> [set xy | xy.1 = xy.2] `<=` X.
Proof.

Let subspace_uniform_entourage_inv : forall A : set (subspace A * subspace A),
  subspace_ent A -> subspace_ent (A^-1)%classic.
Proof.

Let subspace_uniform_entourage_split_ex :
  forall A : set (subspace A * subspace A),
    subspace_ent A -> exists2 B, subspace_ent B & B \; B `<=` A.
Proof.

Let subspace_uniform_nbhsE : @nbhs _ (subspace A) = nbhs_ subspace_ent.
Proof.

HB.instance Definition _ := Nbhs_isUniform_mixin.Build (subspace A)
  Filter_subspace_ent subspace_uniform_entourage_refl
  subspace_uniform_entourage_inv subspace_uniform_entourage_split_ex
  subspace_uniform_nbhsE.

End SubspaceUniform.

Section SubspacePseudoMetric.
Context {R : numDomainType} {X : pseudoMetricType R} (A : set X).

Definition subspace_ball (x : subspace A) (r : R) :=
  if x \in A then A `&` ball (x : X) r else [set x].

Lemma subspace_pm_ball_center x (e : R) : 0 < e -> subspace_ball x e x.
Proof.

Lemma subspace_pm_ball_sym x y (e : R) :
  subspace_ball x e y -> subspace_ball y e x.
Proof.

Lemma subspace_pm_ball_triangle x y z e1 e2 :
  subspace_ball x e1 y -> subspace_ball y e2 z -> subspace_ball x (e1 + e2) z.
Proof.

Lemma subspace_pm_entourageE :
  @entourage (subspace A) = entourage_ subspace_ball.
Proof.

HB.instance Definition _ :=
  @Uniform_isPseudoMetric.Build R (subspace A) subspace_ball
    subspace_pm_ball_center subspace_pm_ball_sym subspace_pm_ball_triangle
    subspace_pm_entourageE.

End SubspacePseudoMetric.

Section SubspaceWeak.
Context {T : topologicalType} {U : pointedType}.
Variables (f : U -> T).

Lemma weak_subspace_open (A : set (weak_topology f)) :
  open A -> open (f @` A : set (subspace (range f))).
Proof.

End SubspaceWeak.

Definition separate_points_from_closed {I : Type} {T : topologicalType}
    {U_ : I -> topologicalType} (f_ : forall i, T -> U_ i) :=
  forall (U : set T) x,
  closed U -> ~ U x -> exists i, ~ (closure (f_ i @` U)) (f_ i x).

Section product_embeddings.
Context {I : choiceType} {T : topologicalType} {U_ : I -> topologicalType}.
Variable (f_ : forall i, T -> U_ i).

Hypothesis sepf : separate_points_from_closed f_.
Hypothesis ctsf : forall i, continuous (f_ i).

Let weakT := [the topologicalType of
  sup_topology (fun i => Topological.on (weak_topology (f_ i)))].

Let PU := [the topologicalType of prod_topology U_].

Local Notation sup_open := (@open weakT).
Local Notation "'weak_open' i" := (@open weakT) (at level 0).
Local Notation natural_open := (@open T).

Lemma weak_sep_cvg (F : set_system T) (x : T) :
  Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)).
Proof.

Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x.
Proof.

Lemma weak_sep_openE : @open T = @open weakT.
Proof.

Definition join_product (x : T) : PU := f_ ^~ x.

Lemma join_product_continuous : continuous join_product.
Proof.

Local Notation prod_open := (@open (subspace (range join_product))).

Lemma join_product_open (A : set T) : open A ->
  open ((join_product @` A) : set (subspace (range join_product))).
Proof.

Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product.
Proof.

Lemma join_product_weak : set_inj [set: T] join_product ->
  @open T = @open (weak_topology join_product).
Proof.

End product_embeddings.

Lemma continuous_compact {T U : topologicalType} (f : T -> U) A :
  {within A, continuous f} -> compact A -> compact (f @` A).
Proof.

Lemma connected_continuous_connected (T U : topologicalType)
    (A : set T) (f : T -> U) :
  connected A -> {within A, continuous f} -> connected (f @` A).
Proof.

Lemma uniform_limit_continuous {U : topologicalType} {V : uniformType}
    (F : set_system (U -> V)) (f : U -> V) :
  ProperFilter F -> (\forall g \near F, continuous (g : U -> V)) ->
  {uniform, F --> f} -> continuous f.
Proof.

Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : uniformType}
    (K : set U) (F : set_system (U -> V)) (f : subspace K -> V) :
  ProperFilter F -> (\forall g \near F, continuous (g : subspace K -> V)) ->
  {uniform K, F --> f} -> {within K, continuous f}.
Proof.

Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) :
  continuous f <->
  forall (x : X), \forall U \near powerset_filter_from (nbhs x),
    {within U, continuous f}.
Proof.

Lemma totally_disconnected_prod (I : choiceType)
  (T : I -> topologicalType) (A : forall i, set (T i)) :
  (forall i, totally_disconnected (A i)) ->
  @totally_disconnected (prod_topology T)
    (fun f => forall i, A i (f i)).
Proof.

Section UniformPointwise.
Context {U : topologicalType} {V : uniformType}.

Definition singletons {T : Type} := [set [set x] | x in [set: T]].

Lemma pointwise_cvg_family_singleton F (f: U -> V):
  Filter F -> {ptws, F --> f} = {family @singletons U, F --> f}.
Proof.

Lemma pointwise_cvg_compact_family F (f : U -> V) :
  Filter F -> {family compact, F --> f} -> {ptws, F --> f}.
Proof.

Lemma pointwise_cvgP F (f: U -> V):
  Filter F -> {ptws, F --> f} <-> forall (t : U), (fun g => g t) @ F --> f t.
Proof.

End UniformPointwise.

Module gauge.
Section gauge.

Let split_sym {T : uniformType} (W : set (T * T)) :=
  (split_ent W) `&` (split_ent W)^-1.

Section entourage_gauge.
Context {T : uniformType} (E : set (T * T)) (entE : entourage E).

Definition gauge :=
  filter_from [set: nat] (fun n => iter n split_sym (E `&` E^-1)).

Lemma iter_split_ent j : entourage (iter j split_sym (E `&` E^-1)).
Proof.

Lemma gauge_ent A : gauge A -> entourage A.
Proof.

Lemma gauge_filter : Filter gauge.
Proof.

Lemma gauge_refl A : gauge A -> [set fg | fg.1 = fg.2] `<=` A.
Proof.

Lemma gauge_inv A : gauge A -> gauge (A^-1)%classic.
Proof.

Lemma gauge_split A : gauge A -> exists2 B, gauge B & B \; B `<=` A.
Proof.

Let gauged : Type := T.

HB.instance Definition _ := Pointed.on gauged.
HB.instance Definition _ :=
  @isUniform.Build gauged gauge gauge_filter gauge_refl gauge_inv gauge_split.

Lemma gauge_countable_uniformity : countable_uniformity gauged.
Proof.

Definition type := countable_uniform.type gauge_countable_uniformity.

#[export] HB.instance Definition _ := Uniform.on type.
#[export] HB.instance Definition _ {R : realType} : PseudoMetric R _ :=
  PseudoMetric.on type.

End entourage_gauge.
End gauge.
Module Exports. HB.reexport. End Exports.
End gauge.
Export gauge.Exports.

Lemma uniform_pseudometric_sup {R : realType} {T : uniformType} :
    @entourage T = @sup_ent T {E : set (T * T) | @entourage T E}
  (fun E => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).
Proof.

Section ArzelaAscoli.
Context {X : topologicalType}.
Context {Y : uniformType}.
Context {hsdf : hausdorff_space Y}.
Implicit Types (I : Type).


Definition equicontinuous {I} (W : set I) (d : I -> (X -> Y)) :=
  forall x (E : set (Y * Y)), entourage E ->
    \forall y \near x, forall i, W i -> E (d i x, d i y).

Lemma equicontinuous_subset {I J} (W : set I) (V : set J)
    {fW : I -> X -> Y} {fV : J -> X -> Y} :
  fW @`W `<=` fV @` V -> equicontinuous V fV -> equicontinuous W fW.
Proof.

Lemma equicontinuous_subset_id (W V : set (X -> Y)) :
  W `<=` V -> equicontinuous V id -> equicontinuous W id.
Proof.

Lemma equicontinuous_continuous_for {I} (W : set I) (fW : I -> X -> Y) i x :
  {for x, equicontinuous W fW} -> W i -> {for x, continuous (fW i)}.
Proof.

Lemma equicontinuous_continuous {I} (W : set I) (fW : I -> (X -> Y)) (i : I) :
  equicontinuous W fW -> W i -> continuous (fW i).
Proof.

Definition pointwise_precompact {I} (W : set I) (d : I -> X -> Y) :=
  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} :
  fW @` W `<=` fV @` V -> pointwise_precompact V fV ->
  pointwise_precompact W fW.
Proof.

Lemma pointwise_precompact_precompact {I} (W : set I) (fW : I -> (X -> Y)) :
  pointwise_precompact W fW -> precompact ((fW @` W) : set {ptws X -> Y}).
Proof.

Lemma uniform_pointwise_compact (W : set (X -> Y)) :
  compact (W : set (@uniform_fun_family X Y compact)) ->
  compact (W : set {ptws X -> Y}).
Proof.

Lemma precompact_pointwise_precompact (W : set {family compact, X -> Y}) :
  precompact W -> pointwise_precompact W id.
Proof.

Lemma pointwise_cvg_entourage (x : X) (f : {ptws X -> Y}) E :
  entourage E -> \forall g \near f, E (f x, g x).
Proof.

Lemma equicontinuous_closure (W : set {ptws X -> Y}) :
  equicontinuous W id -> equicontinuous (closure W) id.
Proof.

Definition small_ent_sub := @small_set_sub _ (@entourage Y).

Lemma pointwise_compact_cvg (F : set_system {ptws X -> Y}) (f : {ptws X -> Y}) :
  ProperFilter F ->
  (\forall W \near powerset_filter_from F, equicontinuous W id) ->
  {ptws, F --> f} <-> {family compact, F --> f}.
Proof.

Lemma pointwise_compact_closure (W : set (X -> Y)) :
  equicontinuous W id ->
  closure (W : set {family compact, X -> Y}) =
  closure (W : set {ptws X -> Y}).
Proof.

Lemma pointwise_precompact_equicontinuous (W : set (X -> Y)) :
  pointwise_precompact W id ->
  equicontinuous W id ->
  precompact (W : set {family compact, X -> Y }).
Proof.

Section precompact_equicontinuous.
Hypothesis lcptX : locally_compact [set: X].

Lemma compact_equicontinuous (W : set {family compact, X -> Y}) :
  (forall f, W f -> continuous f) ->
  compact (W : set {family compact, X -> Y}) ->
  equicontinuous W id.
Proof.

Lemma precompact_equicontinuous (W : set {family compact, X -> Y}) :
  (forall f, W f -> continuous f) ->
  precompact (W : set {family compact, X -> Y}) ->
  equicontinuous W id.
Proof.

End precompact_equicontinuous.

Theorem Ascoli (W : set {family compact, X -> Y}) :
    locally_compact [set: X] ->
  pointwise_precompact W id /\ equicontinuous W id <->
    (forall f, W f -> continuous f) /\
    precompact (W : set {family compact, X -> Y}).
Proof.

End ArzelaAscoli.

Lemma uniform_regular {T : uniformType} : @regular_space T.
Proof.

#[global] Hint Resolve uniform_regular : core.

Section currying.
Local Notation "U '~>' V" :=
  ({compact-open, [the topologicalType of U] -> [the topologicalType of V]})
  (at level 99, right associativity).

Section cartesian_closed.
Context {U V W : topologicalType}.

In this section, we consider under what conditions
[f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)]
and
[f in U * V ~> W | continuous f]
are homeomorphic.

So the category of locally compact regular spaces is cartesian closed.


Lemma continuous_curry (f : (U * V)%type ~> W) :
  continuous f ->
    continuous (curry f : U ~> V ~> W) /\ forall u, continuous (curry f u).
Proof.

Lemma continuous_uncurry_regular (f : U ~> V ~> W) :
  locally_compact [set: V] -> @regular_space V -> continuous f ->
  (forall u, continuous (f u)) -> continuous (uncurry f : (U * V)%type ~> W).
Proof.

Lemma continuous_uncurry (f : U ~> V ~> W) :
  locally_compact [set: V] -> hausdorff_space V -> continuous f ->
  (forall u, continuous (f u)) ->
  continuous ((uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W)) f).
Proof.

Lemma curry_continuous (f : (U * V)%type ~> W) : continuous f -> @regular_space U ->
  {for f, continuous (curry : ((U * V)%type ~> W) -> (U ~> V ~> W))}.
Proof.

Lemma uncurry_continuous (f : U ~> V ~> W) :
  locally_compact [set: V] -> @regular_space V -> @regular_space U ->
  continuous f -> (forall u, continuous (f u)) ->
  {for f, continuous (uncurry : (U ~> V ~> W) -> ((U * V)%type ~> W))}.
Proof.

End cartesian_closed.

End currying.