Module mathcomp.analysis.normedtype_theory.tvs

# Topological vector spaces This file introduces locally convex topological vector spaces. ``` NbhsNmodule == HB class, join of Nbhs and Nmodule NbhsZmodule == HB class, join of Nbhs and Zmodule NbhsLmodule K == HB class, join of Nbhs and Lmodule over K K is a numDomainType. PreTopologicalNmodule == HB class, join of Topological and Nmodule TopologicalNmodule == HB class, PreTopologicalNmodule with a continuous addition PreTopologicalZmodule == HB class, join of Topological and Zmodule topologicalZmodType == topological abelian group TopologicalZmodule == HB class, join of TopologicalNmodule and Zmodule with a continuous opposite operator preTopologicalLmodType K == topological space and Lmodule over K K is a numDomainType The HB class is PreTopologicalLmodule. topologicalLmodType K == topologicalNmodule and Lmodule over K with a continuous scaling operation The HB class is TopologicalLmodule. PreUniformNmodule == HB class, join of Uniform and Nmodule UniformNmodule == HB class, join of Uniform and Nmodule with a uniformly continuous addition PreUniformZmodule == HB class, join of Uniform and Zmodule UniformZmodule == HB class, join of UniformNmodule and Zmodule with uniformly continuous opposite operator PreUniformLmodule K == HB class, join of Uniform and Lmodule over K K is a numDomainType. UniformLmodule K == HB class, join of UniformNmodule and Lmodule with a uniformly continuous scaling operation K is a numFieldType. tvsType R == interface type for a locally convex tvs on a numDomain R A tvs is constructed over a uniform space. The HB class is Tvs. PreTopologicalLmod_isTvs == factory allowing the construction of a tvs from an Lmodule which is also a topological space ``` HB instances: - The type R^o (R : numFieldType) is endowed with the structure of Tvs. - The product of two Tvs is endowed with the structure of Tvs.