Nuprl Definition : real-proj
ℙ^n == {b:ℝ^n + 1| ∃k:ℕn + 1. b k ≠ r0}
Definitions occuring in Statement :
real-vec: ℝ^n,
rneq: x ≠ y,
int-to-real: r(n),
int_seg: {i..j-},
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
real-vec: ℝ^n,
exists: ∃x:A. B[x],
int_seg: {i..j-},
add: n + m,
rneq: x ≠ y,
apply: f a,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
real-proj
Latex:
\mBbbP{}\^{}n == \{b:\mBbbR{}\^{}n + 1| \mexists{}k:\mBbbN{}n + 1. b k \mneq{} r0\}
Date html generated:
2017_10_05-AM-00_16_54
Last ObjectModification:
2017_06_17-AM-10_06_56
Theory : inner!product!spaces
Home
Index