Isolate normed structures from topological structures

AUTHORS.md

@@ -7,9 +7,9 @@
 - Pierre-Yves Strub, École polytechnique
 
 # Acknowledgments
-- `hierarchy.v` is a reimplementation of file `Hierarchy.v` from the
-  library Coquelicot by Sylvie Boldo, Catherine Lelay, and Guillaume
-  Melquiond (http://coquelicot.saclay.inria.fr/)
+- `topology.v` and `normedtype.v` contain a reimplementation of file
+  `Hierarchy.v` from the library Coquelicot by Sylvie Boldo, Catherine Lelay,
+  and Guillaume Melquiond (http://coquelicot.saclay.inria.fr/)
 - our proof of Zorn's Lemma in `set.v` is a reimplementation of the one by
   Daniel Schepler (https://github.com/coq-contribs/zorns-lemma); we also took
   inspiration from his work on topology

FILES.md

@@ -5,7 +5,7 @@
 - `posnum.v`
 - `classical_set.v`
 - `topology.v`
-- `hierarchy.v`
+- `normedtype.v`
 - `landau.v`
 - `derive.v`
 - `README.md`

_CoqProject

@@ -10,7 +10,7 @@ classical_sets.v
 Rstruct.v
 Rbar.v
 topology.v
-hierarchy.v
+normedtype.v
 forms.v
 derive.v
 summability.v

derive.v

@@ -3,7 +3,7 @@ Require Import Reals.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
 From mathcomp Require Import ssralg ssrnum fintype bigop matrix interval.
 Require Import boolp reals Rstruct Rbar.
-Require Import classical_sets posnum topology hierarchy landau forms.
+Require Import classical_sets posnum topology normedtype landau forms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -1307,7 +1307,7 @@ have {imf_ltsup} imf_ltsup : forall t, t \in `[a, b] -> f t < sup imf.
   apply/eqP; rewrite eqr_le supleft sup_upper_bound => //.
   by rewrite !inE; apply/asboolP/imageP.
 have invf_cont : {in `[a, b], continuous (fun t => 1 / (sup imf - f t))}.
-  move=> t tab; apply: lim_inv.
+  move=> t tab; apply: (@lim_inv _ [filter of t]).
     by rewrite neqr_lt subr_gt0 orbC imf_ltsup.
   by apply: lim_add; [apply: continuous_cst|apply: lim_opp; apply:fcont].
 have [M imVfltM] : bounded ((fun t => 1 / (sup imf - f t)) @`

landau.v

@@ -3,7 +3,7 @@ Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum.
 Require Import boolp reals Rstruct Rbar.
-Require Import classical_sets posnum topology hierarchy.
+Require Import classical_sets posnum topology normedtype.
 
 (******************************************************************************)
 (*              BACHMANN-LANDAU NOTATIONS : BIG AND LITTLE O                  *)

misc/uniform_bigO.v

@@ -3,7 +3,7 @@ Require Import Reals.
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop ssralg ssrnum.
 Require Import boolp reals Rstruct Rbar.
-Require Import classical_sets posnum topology hierarchy landau.
+Require Import classical_sets posnum topology normedtype landau.
 
 Set Implicit Arguments.
 Unset Strict Implicit.