Nuprl Definition : P_point-line-sep
P_point-line-sep(e;P;L) ==
(fst(snd(P)) \/ fst(L) ∨ fst(snd(snd(P))) \/ fst(L))
∧ (∀x:{x:Point| x I fst(snd(P)) ∧ x I fst(snd(snd(P)))} . x # fst(L))
Definitions occuring in Statement :
geo-plsep: p # l,
geo-intersect: L \/ M,
geo-incident: p I L,
geo-point: Point,
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions occuring in definition :
or: P ∨ Q,
geo-intersect: L \/ M,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
geo-point: Point,
and: P ∧ Q,
geo-incident: p I L,
pi2: snd(t),
geo-plsep: p # l,
pi1: fst(t)
FDL editor aliases :
P_point-line-sep
Latex:
P\_point-line-sep(e;P;L) ==
(fst(snd(P)) \mbackslash{}/ fst(L) \mvee{} fst(snd(snd(P))) \mbackslash{}/ fst(L))
\mwedge{} (\mforall{}x:\{x:Point| x I fst(snd(P)) \mwedge{} x I fst(snd(snd(P)))\} . x \# fst(L))
Date html generated:
2019_10_16-PM-03_00_32
Last ObjectModification:
2018_08_11-PM-09_59_06
Theory : euclidean!plane!geometry
Home
Index