Nuprl Definition : r2-line-sep
r2-line-sep(l;m) ==  ∃p:ℝ^2. ((|pfst(l)fst(snd(l))| = r0) ∧ |pfst(m)fst(snd(m))| ≠ r0)
Definitions occuring in Statement : 
r2-det: |pqr|
, 
real-vec: ℝ^n
, 
rneq: x ≠ y
, 
req: x = y
, 
int-to-real: r(n)
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
exists: ∃x:A. B[x]
, 
and: P ∧ Q
, 
natural_number: $n
Definitions occuring in definition : 
natural_number: $n
, 
int-to-real: r(n)
, 
pi2: snd(t)
, 
pi1: fst(t)
, 
r2-det: |pqr|
, 
rneq: x ≠ y
, 
req: x = y
, 
and: P ∧ Q
, 
real-vec: ℝ^n
, 
exists: ∃x:A. B[x]
FDL editor aliases : 
r2-line-sep
Latex:
r2-line-sep(l;m)  ==    \mexists{}p:\mBbbR{}\^{}2.  ((|pfst(l)fst(snd(l))|  =  r0)  \mwedge{}  |pfst(m)fst(snd(m))|  \mneq{}  r0)
Date html generated:
2018_07_29-AM-09_46_57
Last ObjectModification:
2018_07_02-PM-04_02_51
Theory : reals!model!euclidean!geometry
Home
Index