Nuprl Definition : geo-not-parallel
geo-not-parallel(g;l;L) == ∀m:Line. ((m = L ∈ (l,m:Line//l || m)) ⇒ (¬l || m))
Definitions occuring in Statement :
geo-Aparallel: l || m,
geo-line: Line,
quotient: x,y:A//B[x; y],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
geo-Aparallel: l || m,
not: ¬A,
geo-line: Line,
quotient: x,y:A//B[x; y],
equal: s = t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
FDL editor aliases :
geo-not-parallel
Latex:
geo-not-parallel(g;l;L) == \mforall{}m:Line. ((m = L) {}\mRightarrow{} (\mneg{}l || m))
Date html generated:
2018_05_22-PM-01_12_11
Last ObjectModification:
2018_04_14-PM-01_38_25
Theory : euclidean!plane!geometry
Home
Index