Finite dimensional real normed spaces are proper metric spaces

DOI10.2478/FORMA-2021-0017zbMath1494.68302OpenAlexW4285325843MaRDI QIDQ2171521

Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama

Publication date: 9 September 2022

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2021-0017

zbMATH Keywords

L1-normlinear isometrynormed spacestopological spacemaximum normproper metric spacereal vector space

Mathematics Subject Classification ID

Convergence and divergence of series and sequences (40A05) Linear transformations, semilinear transformations (15A04) Compactness in topological linear spaces; angelic spaces, etc. (46A50) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Differentiable Functions on Normed Linear Spaces
• Mizar: State-of-the-art and Beyond

This page was built for publication: Finite dimensional real normed spaces are proper metric spaces