Nuprl Definition : r2-line
r2-line == a:ℝ^2 × b:ℝ^2 × a ≠ b
Definitions occuring in Statement :
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
product: x:A × B[x]
FDL editor aliases :
r2-line
Latex:
r2-line == a:\mBbbR{}\^{}2 \mtimes{} b:\mBbbR{}\^{}2 \mtimes{} a \mneq{} b
Date html generated:
2018_07_29-AM-09_46_53
Last ObjectModification:
2018_07_02-PM-03_51_54
Theory : reals!model!euclidean!geometry
Home
Index