Transformation tools for real linear spaces

DOI10.2478/FORMA-2022-0008MaRDI QIDQ6489404zbMATH OpenFDO

Authors Kazuhisa Nakasho

Publication date 22 April 2024

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

zbMATH Keywords

real normed spacereal vector spacereal Euclidean spacereal linear space

Mathematics Subject Classification ID

Summability and bases in topological vector spaces (46A35) Formalization of mathematics in connection with theorem provers (68V20) Other ``topological linear spaces (convergence spaces, ranked spaces, spaces with a metric taking values in an ordered structure more general than (mathbb{R}), etc.) (46A19)

Recommendations

• Real vector space and related notions
• Lattice vector spaces and linear transformations
• scientific article; zbMATH DE number 7267081
• Isomorphisms from the space of multilinear operators

Cites work

• scientific article; zbMATH DE number 3678487 (Why is no real title available?)
• scientific article; zbMATH DE number 1199721 (Why is no real title available?)
• Cartesian products of family of real linear spaces
• Mizar: state-of-the-art and beyond
• Partial differentiation, differentiation and continuity on \(n\)-dimensional real normed linear spaces
• The role of the Mizar mathematical library for interactive proof development in Mizar

This page was built for publication: Transformation tools for real linear spaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6489404)