Nuprl Definition : obtuse-angle

Obtuse(a;b;c) ==  ∀c':Point. (c'=b=c ⇒ ac > ac')



Definitions occuring in Statement :  geo-midpoint: a=m=b,  geo-gt: cd > ab,  geo-point: Point,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  geo-gt: cd > ab,  geo-midpoint: a=m=b,  implies: P ⇒ Q,  geo-point: Point,  all: ∀x:A. B[x]
FDL editor aliases :  obtuse-angle

Latex:
Obtuse(a;b;c)  ==    \mforall{}c':Point.  (c'=b=c  {}\mRightarrow{}  ac  >  ac')



Date html generated: 2018_05_22-AM-11_52_21
Last ObjectModification: 2018_03_28-PM-02_40_00

Theory : euclidean!plane!geometry


Home Index