Commit 99016d59 authored by Michael Kohlhase's avatar Michael Kohlhase

debug

parent c6be6b3e
\begin{mhmodnl}[creators=miko]{topvr-metrizable}{en}
\begin{definition}
We call a \trefiii[topological-vectorspace]{topological}{vector}{space} $\cV$
\defi{normable}, iff there is a \trefii[metric-space]{distance}{function} on the
\defi{metrizable}, iff there is a \trefii[metric-space]{distance}{function} on the
\trefii[topological-vectorspace]{base}{set} of $\cV$ that
\mtrefi[metric-induced-topology?induced-topology]{induces} the topology of $\cV$.
\end{definition}
......
\begin{modsig}[creators=miko]{topvr-metrizable}
\gimport[smglom/calculus]{metric-induced-topology}
\gimport{topological-vectorspace}
\symi{metrizable}
\symi{normable}
\symi{metrizable}
\end{modsig}
%%% Local Variables:
%%% mode: latex
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment