Formalization of orthogonal decomposition for Hilbert spaces

DOI10.2478/FORMA-2022-0023MaRDI QIDQ6557227zbMATH OpenFDO

Authors Hiroyuki Okazaki

Publication date 18 June 2024

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported

Full work available at URL https://doi.org/10.2478/FORMA-2022-0023

zbMATH Keywords

Hilbert spaceorthogonal decompositiontopological space

Mathematics Subject Classification ID

Hilbert and pre-Hilbert spaces: geometry and topology (including spaces with semidefinite inner product) (46C05) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• The orthogonal projection and the Riesz representation theorem
• scientific article; zbMATH DE number 11256
• Orthogonally Complemented Subspaces in Banach Spaces
• scientific article; zbMATH DE number 1829736

Cites work

• scientific article; zbMATH DE number 3678487 (Why is no real title available?)
• scientific article; zbMATH DE number 3281211 (Why is no real title available?)
• Mizar: state-of-the-art and beyond
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(1)

• Formalization of orthogonal complements of normed spaces

This page was built for publication: Formalization of orthogonal decomposition for Hilbert spaces

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