GitHub - dominique-unruh/bounded-operators: Isabelle theory about bounded operators

Formalization of the space of complex bounded operators

Author: Jose Manuel Rodriguez Caballero, Dominique Unruh Licence: BSD 3-clause

Name		Name	Last commit message	Last commit date
Latest commit History 1,349 Commits
document		document
extra		extra
fake-session-dir		fake-session-dir
.gitattributes		.gitattributes
.gitignore		.gitignore
All.thy		All.thy
Cblinfun_Code.thy		Cblinfun_Code.thy
Cblinfun_Code_Examples.thy		Cblinfun_Code_Examples.thy
Cblinfun_Matrix.thy		Cblinfun_Matrix.thy
Complex_Bounded_Linear_Function.thy		Complex_Bounded_Linear_Function.thy
Complex_Bounded_Linear_Function0.thy		Complex_Bounded_Linear_Function0.thy
Complex_Euclidean_Space0.thy		Complex_Euclidean_Space0.thy
Complex_Inner_Product.thy		Complex_Inner_Product.thy
Complex_Inner_Product0.thy		Complex_Inner_Product0.thy
Complex_L2.thy		Complex_L2.thy
Complex_Vector_Spaces.thy		Complex_Vector_Spaces.thy
Complex_Vector_Spaces0.thy		Complex_Vector_Spaces0.thy
LICENSE		LICENSE
Makefile		Makefile
One_Dimensional_Spaces.thy		One_Dimensional_Spaces.thy
README.md		README.md
ROOT		ROOT
ROOT.AFP		ROOT.AFP
bounded-operators-afp.zip		bounded-operators-afp.zip
isabelle.sh		isabelle.sh
todo.txt		todo.txt

Provide feedback