Nuprl Definition : geo-lt-angle
abc < xyz ==
(¬out(y xz)) ∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ y_p'_p ∧ (out(y xx') ∧ out(y zz')) ∧ (¬x_y_p) ∧ x'_p'_z' ∧ p' ≠ z'))
Definitions occuring in Statement :
geo-out: out(p ab),
geo-cong-angle: abc ≅a xyz,
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
geo-point: Point,
geo-cong-angle: abc ≅a xyz,
geo-out: out(p ab),
not: ¬A,
and: P ∧ Q,
geo-between: a_b_c,
geo-sep: a ≠ b
FDL editor aliases :
geo-lt-angle
Latex:
abc < xyz ==
(\mneg{}out(y xz))
\mwedge{} (\mexists{}p,p',x',z':Point
(abc \mcong{}\msuba{} xyp \mwedge{} y\_p'\_p \mwedge{} (out(y xx') \mwedge{} out(y zz')) \mwedge{} (\mneg{}x\_y\_p) \mwedge{} x'\_p'\_z' \mwedge{} p' \mneq{} z'))
Date html generated:
2019_10_16-PM-01_49_00
Last ObjectModification:
2019_08_30-PM-00_54_01
Theory : euclidean!plane!geometry
Home
Index