Nuprl Definition : geo-perp-in
ab ⊥x cd == Colinear(a;b;x) ∧ Colinear(c;d;x) ∧ (∀u,v:Point. (Colinear(a;b;u) ⇒ Colinear(c;d;v) ⇒ Ruxv))
Definitions occuring in Statement :
right-angle: Rabc,
geo-colinear: Colinear(a;b;c),
geo-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],
geo-point: Point,
implies: P ⇒ Q,
geo-colinear: Colinear(a;b;c),
right-angle: Rabc
FDL editor aliases :
geo-perp-in
geo-perp-in
Latex:
ab \mbot{}x 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{} Ruxv))
Date html generated:
2017_10_02-PM-06_42_26
Last ObjectModification:
2017_08_05-PM-04_48_34
Theory : euclidean!plane!geometry
Home
Index