Nuprl Definition : geo-intersect
L \/ M ==
∃l,m:Line
((l = L ∈ LINE)
∧ (m = M ∈ LINE)
∧ (∃a,b:{c:Point| c I l} . (a leftof fst(m)fst(snd(m)) ∧ b leftof fst(snd(m))fst(m))))
Definitions occuring in Statement :
geo-incident: p I L
,
geoline: LINE
,
geo-line: Line
,
geo-left: a leftof bc
,
geo-point: Point
,
pi1: fst(t)
,
pi2: snd(t)
,
exists: ∃x:A. B[x]
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
equal: s = t ∈ T
Definitions occuring in definition :
pi1: fst(t)
,
pi2: snd(t)
,
geo-left: a leftof bc
,
and: P ∧ Q
,
geo-incident: p I L
,
geo-point: Point
,
set: {x:A| B[x]}
,
exists: ∃x:A. B[x]
,
geoline: LINE
,
equal: s = t ∈ T
,
geo-line: Line
FDL editor aliases :
geo-intersect
Latex:
L \mbackslash{}/ M ==
\mexists{}l,m:Line
((l = L)
\mwedge{} (m = M)
\mwedge{} (\mexists{}a,b:\{c:Point| c I l\} . (a leftof fst(m)fst(snd(m)) \mwedge{} b leftof fst(snd(m))fst(m))))
Date html generated:
2018_05_22-PM-01_05_01
Last ObjectModification:
2018_05_10-PM-04_43_41
Theory : euclidean!plane!geometry
Home
Index