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