Nuprl Definition : geo-non-parallel

geo-non-parallel(g;l;L) ==  ↓∀a:Line. ((a = L ∈ (l,m:Line//l || m)) ⇒ (∃p:Point. (p I l ∧ p I a)))


Definitions occuring in Statement :  geo-Aparallel: l || m,  geo-incident: p I L,  geo-line: Line,  geo-point: Point,  quotient: x,y:A//B[x; y],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  squash: ↓T,  implies: P ⇒ Q,  and: P ∧ Q,  equal: s = t ∈ T
Definitions occuring in definition :  geo-incident: p I L,  and: P ∧ Q,  geo-point: Point,  exists: ∃x:A. B[x],  geo-Aparallel: l || m,  geo-line: Line,  quotient: x,y:A//B[x; y],  equal: s = t ∈ T,  implies: P ⇒ Q,  all: ∀x:A. B[x],  squash: ↓T
FDL editor aliases :  geo-non-parallel
Latex:
geo-non-parallel(g;l;L)  ==    \mdownarrow{}\mforall{}a:Line.  ((a  =  L)  {}\mRightarrow{}  (\mexists{}p:Point.  (p  I  l  \mwedge{}  p  I  a)))


Date html generated: 2018_05_22-PM-01_11_49
Last ObjectModification: 2018_03_23-PM-02_10_38

Theory : euclidean!plane!geometry


Home Index