The structure pseudometric_normedZmodType is morally a topologicalNmodule but topologicalNmodule is defined later in tvs.v (which imports pseudometric_normed_zmodule.v).
We think that it should be defined at the beginning of pseudometric_normed_zmodule.v and that pseudometric_normedZmodType should be defined using topologicalNmodule.
This would avoid the duplication of lemmas such as cvgD/fun_cvgD.
See
The structure
pseudometric_normedZmodTypeis morally atopologicalNmodulebuttopologicalNmoduleis defined later intvs.v(which importspseudometric_normed_zmodule.v).We think that it should be defined at the beginning of
pseudometric_normed_zmodule.vand thatpseudometric_normedZmodTypeshould be defined usingtopologicalNmodule.This would avoid the duplication of lemmas such as
cvgD/fun_cvgD.See
analysis/theories/normedtype_theory/tvs.v
Line 117 in 6bc95eb