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