fixes #1456 (#1466)

* fixes #1456 * fixes #1454
math-comp · Feb 8, 2025 · b1efe9b · b1efe9b
1 parent 94bcff4
commit b1efe9b
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 9 deletions.
diff --git a/theories/charge.v b/theories/charge.v
@@ -50,7 +50,6 @@ From mathcomp Require Import lebesgue_integral.
 (*                                                                            *)
 (* ## Theory                                                                  *)
 (* ```                                                                        *)
-
 (*         nu.-positive_set P == P is a positive set with nu a charge         *)
 (*         nu.-negative_set N == N is a negative set with nu a charge         *)
 (* hahn_decomposition nu P N == the full set can be decomposed in P and N,    *)

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -2,9 +2,9 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
-From mathcomp Require Import boolp classical_sets functions.
-From mathcomp Require Import cardinality fsbigop signed reals ereal topology.
-From mathcomp Require Import tvs normedtype sequences real_interval esum measure.
+From mathcomp Require Import boolp classical_sets functions cardinality.
+From mathcomp Require Import fsbigop signed reals ereal topology tvs.
+From mathcomp Require Import normedtype sequences real_interval esum measure.
 From mathcomp Require Import lebesgue_measure numfun realfun function_spaces.
 
 (**md**************************************************************************)

diff --git a/theories/topology_theory/matrix_topology.v b/theories/topology_theory/matrix_topology.v
@@ -66,8 +66,7 @@ Variables (m n : nat) (T : uniformType).
 
 Implicit Types A : set ('M[T]_(m, n) * 'M[T]_(m, n)).
 
-Definition mx_ent :=
-  filter_from
+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)]).

diff --git a/theories/topology_theory/product_topology.v b/theories/topology_theory/product_topology.v
@@ -49,8 +49,6 @@ HB.instance Definition _ := Nbhs_isNbhsTopological.Build (T * U)%type
 
 End Prod_Topology.
 
-(** Topology on matrices *)
-
 Lemma fst_open {U V : topologicalType} (A : set (U * V)) :
   open A -> open (fst @` A).
 Proof.

diff --git a/theories/topology_theory/supremum_topology.v b/theories/topology_theory/supremum_topology.v
@@ -11,7 +11,7 @@ From mathcomp Require Import topology_structure uniform_structure.
 (*                                     topologicalType structures Tc on T     *)
 (*                        sup_ent E == the entourages of the supremum         *)
 (* ```                                                                        *)
-(* `sup_topology` is equipped with the `Uniform` structure                         *)
+(* `sup_topology` is equipped with the `Uniform` structure                    *)
 (******************************************************************************)
 
 Set Implicit Arguments.