Nuprl Definition : eu-perp-in
Perp-in(x; ab; cd) ==
Colinear(a;b;x) ∧ Colinear(c;d;x) ∧ (∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Per(u;x;v)))
Definitions occuring in Statement :
eu-perpendicular: Per(a;b;c),
eu-colinear: Colinear(a;b;c),
eu-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
eu-point: Point,
implies: P ⇒ Q,
eu-colinear: Colinear(a;b;c),
eu-perpendicular: Per(a;b;c)
FDL editor aliases :
eu-perp-in
Latex:
Perp-in(x; ab; cd) ==
Colinear(a;b;x)
\mwedge{} Colinear(c;d;x)
\mwedge{} (\mforall{}u,v:Point. (Colinear(a;b;u) {}\mRightarrow{} Colinear(c;d;v) {}\mRightarrow{} Per(u;x;v)))
Date html generated:
2016_05_18-AM-06_43_14
Last ObjectModification:
2015_12_25-PM-04_13_09
Theory : euclidean!geometry
Home
Index