Nuprl Definition : real-cube
real-cube(k) == ℝ^k × ℝ^k
Wellformedness Lemmas :
real-cube_wf
Definitions occuring in Statement :
real-vec: ℝ^n,
product: x:A × B[x]
Definitions occuring in definition :
product: x:A × B[x],
real-vec: ℝ^n
FDL editor aliases :
real-cube
Latex:
real-cube(k) == \mBbbR{}\^{}k \mtimes{} \mBbbR{}\^{}k
Date html generated:
2019_10_30-AM-11_30_56
Last ObjectModification:
2019_09_27-PM-00_41_49
Theory : real!vectors
Home
Index