Nuprl Definition : rng-pp-primitives
rng-pp-primitives(r) == points={p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} lines={p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} plse\000Cp=λp,l. (¬((p . l) = 0 ∈ |r|))
Definitions occuring in Statement :
mk-pgeo-prim: mk-pgeo-prim,
int_seg: {i..j-},
not: ¬A,
set: {x:A| B[x]} ,
lambda: λx.A[x],
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
rng_zero: 0,
rng_car: |r|,
scalar-product: (a . b),
zero-vector: 0
Definitions occuring in definition :
mk-pgeo-prim: mk-pgeo-prim,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int_seg: {i..j-},
zero-vector: 0,
lambda: λx.A[x],
not: ¬A,
equal: s = t ∈ T,
rng_car: |r|,
scalar-product: (a . b),
natural_number: $n,
rng_zero: 0
FDL editor aliases :
rng-pp-primitives
Latex:
rng-pp-primitives(r) == points=\{p:\mBbbN{}3 {}\mrightarrow{} |r|| \mneg{}(p = 0)\} lines=\{p:\mBbbN{}3 {}\mrightarrow{} |r|| \mneg{}(p = 0)\} plsep=\mlambda{}p,l. \000C(\mneg{}((p . l) = 0))
Date html generated:
2018_05_22-PM-00_53_01
Last ObjectModification:
2017_12_20-PM-03_25_21
Theory : euclidean!plane!geometry
Home
Index