docs cleanup

classical/mathcomp_extra.v

@@ -13,6 +13,7 @@ From mathcomp Require Import finset interval.
 (*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
 (*                           given x : T i                                    *)
 (*                 swap x := (x.2, x.1)                                       *)
+(*           map_pair f x := (f x.1, f x.2)                                       *)
 (*         monotonous A f := {in A &, {mono f : x y / x <= y}} \/             *)
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
 (* ```                                                                        *)
@@ -370,6 +371,9 @@ Proof. by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.
 
 Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
 
+Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) :=
+  (f x.1, f x.2).
+
 Section order_min.
 Variables (d : Order.disp_t) (T : orderType d).
 

theories/function_spaces.v

@@ -9,17 +9,28 @@ Require Import reals signed all_topology separation_axioms.
 (* # The topology of functions spaces                                         *)
 (*                                                                            *)
 (* Function spaces have no canonical topology. We develop the theory of       *)
-(* several general-purpose function space topologies here. Contextually,      *)
-(* there is often a natural choice, though. So we provide modules to assign   *)
-(* topologies to arrow types locally.                                         *)
+(* several general-purpose function space topologies here.                    *)
+(*                                                                            *)
+(* ## Topologies on `U -> V`                                                  *)
+(* There is no canonical topology on `U->V` in this library. Mathematically,  *)
+(* the right topology usually depends on context. We provide 3 general        *)
+(* options in this file which work for various amounts of structures on the   *)
+(* domain and codomain.                                                       *)
 (*                                                                            *)
 (* Topologies we consider are:                                                *)
 (* - Topology of pointwise convergence                                        *)
-(* - Topology of uniform convergence                                          *)
-(* - Topology of uniform convergence on subspaces                             *)
+(*   - requires only a topology on V                                          *)
+(* - Topology of uniform convergence: Only uniform on V                       *)
+(*   - requires only a uniformity on V                                        *)
+(* - Topology of uniform convergence on subspaces: Only uniform on V          *)
+(*   - requires only a uniformity on V                                        *)
 (* - The compact-open topology                                                *)
+(*   - requires a topology on U and V                                         *)
+(*                                                                            *)
+(* Note that the compact-open and uniform topology agree when U has a         *)
+(* topology and V is uniform and compact by `compact_open_fam_compactP`.      *)
 (*                                                                            *)
-(* Available modules to assign a topology to `->`:                            *)
+(* To locally asign a topology to `->`, import one of the following modules   *)
 (* - ArrowAsProduct assigns the product topology                              *)
 (* - ArrowAsUniformType assigns the uniform topology                          *)
 (* - ArrowAsCompactOpen assign the compact-open topology                      *)

theories/topology/bool_topology.v

@@ -6,7 +6,8 @@ Require Import order_topology compact.
 
 (**md**************************************************************************)
 (* # Topology for boolean numbers                                             *)
-(*                                                                            *)
+(*          pseudoMetric_bool == an alias for bool equipped with the trivial  *)
+(*                               pseudometric                                 *)
 (******************************************************************************)
 
 Import Order.TTheory GRing.Theory Num.Theory.

theories/topology/compact.v

@@ -22,6 +22,11 @@ Require Import signed reals topology_mixin uniform_mixin pseudometric_mixin.
 (*                               for a finite number of indices in D          *)
 (*              cover_compact == set of compact sets w.r.t. the open          *)
 (*                               cover-based definition of compactness        *)
+(*          open_fam_of A D f == the family of f indexed by D restricted to A *)
+(*                               is a family of open sets                     *)
+(*        closed_fam_of A D f == the family of f indexed by D restricted to A *)
+(*                               is a family of closed sets                   *)
+(*                                                                            *)
 (* ```                                                                        *)
 (******************************************************************************)
 

theories/topology/matrix_topology.v

@@ -5,7 +5,10 @@ Require Import signed topology_mixin uniform_mixin pseudometric_mixin.
 
 (**md**************************************************************************)
 (* # Matrix topology                                                          *)
-(*                                                                            *)
+(* ```                                                                        *)
+(*                  mx_ent m n A == entourages for the m x n matricies        *)
+(*                 mx_ball m n A == balls for the m x n matricies             *)
+(* ```                                                                        *)
 (* Matrices `'M[T]_(m, n)` are endowed with the structures of:                *)
 (* - topology                                                                 *)
 (* - uniform space                                                            *)

theories/topology/pseudometric_mixin.v

@@ -25,8 +25,9 @@ Require Import signed reals topology_mixin uniform_mixin.
 (*                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         *)
+(*                   discrete_ent == entourages of the discrete uniformity    *)
 (*                                   topology                                 *)
+(*                  discrete_ball == singleton balls for the discrete metric  *)
 (*         discrete_topology_type == equip choice types with a discrete       *)
 (*                                   topology                                 *)
 (* ```                                                                        *)
@@ -57,6 +58,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 (* Making sure that [Program] does not automatically introduce *)
+#[local]
 Obligation Tactic := idtac.
 
 Local Open Scope classical_set_scope.

theories/topology/supremum_topology.v

@@ -9,8 +9,9 @@ Require Import topology_mixin uniform_mixin.
 (* ```                                                                        *)
 (*                  sup_topology Tc == supremum topology of the family of     *)
 (*                                     topologicalType structures Tc on T     *)
+(*                        sup_ent E == the entourages of the supremum         *)
 (* ```                                                                        *)
-(* `sup_ent` is equipped with the `Uniform` structure                         *)
+(* `sup_topology` is equipped with the `Uniform` structure                         *)
 (******************************************************************************)
 
 Set Implicit Arguments.

theories/topology/weak_topology.v

@@ -83,9 +83,6 @@ End Weak_Topology.
 HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) :=
   Pointed.on (weak_topology f).
 
-Definition map_pair {S U} (f : S -> U) (x : (S * S)) : (U * U) :=
-  (f x.1, f x.2).
-
 Section weak_uniform.
 Local Open Scope relation_scope.
 Variable (pS : choiceType) (U : uniformType) (f : pS -> U).