[isabelle] Dependent types and existence of n-dimensional space.
Dear Isabelle Users
I know that dependent types do not exist in Isabelle. But there should be some alternative way to express any (simple) mathematical fact, should not it? I really need the following lemma.
Lemma. Fix natural number n. Then there exist a n-dimensional real vector space R^n
This fact is absolutely obvious, and it is crucial for my formalization.
In Isabelle, for, say, n=100, I can easily obtain 100-dimensional space by writing
have “CARD(100)=100” by auto
from this obtain A where “A = (UNIV :: (real^100) set)” and “dim A = 100” by (simp add: dim_univ)
But I need this for general n. I can write
fix n :: nat
assume “CARD('m :: finite)=n”
from this obtain A where “A = (UNIV :: (real^'m) set)” and “dim A = n” by (simp add: dim_univ)
But now I need to obtain a n-dimensional universe without additional assumptions. Can somebody help me?
P. S. I hope this is possible. Otherwise how we can hope to formalize significant part of mathematics if we cannot prove such a simple fact?
This archive was generated by a fusion of
Pipermail (Mailman edition) and