Nuprl Definition : rn-ss
sepℝ^n == Point=ℝ^n #=λx,y. x ≠ y cotrans=TERMOF{real-vec-sep-cases-alt:o, 1:l} n
Definitions occuring in Statement :
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-ss: Error :mk-ss,
real-vec: ℝ^n,
lambda: λx.A[x],
real-vec-sep: a ≠ b,
apply: f a,
real-vec-sep-cases-alt
TermOfs occuring in Definition :
real-vec-sep-cases-alt
FDL editor aliases :
rn-ss
Latex:
sep\mBbbR{}\^{}n == Point=\mBbbR{}\^{}n \#=\mlambda{}x,y. x \mneq{} y cotrans=TERMOF\{real-vec-sep-cases-alt:o, 1:l\} n
Date html generated:
2020_05_20-PM-01_10_46
Last ObjectModification:
2019_12_10-AM-00_31_11
Theory : inner!product!spaces
Home
Index