Nuprl Definition : eu-perpendicular
Per(a;b;c) == ∃c':Point. (c=b=c' ∧ ac=ac')
Definitions occuring in Statement :
eu-midpoint: a=m=b,
eu-congruent: ab=cd,
eu-point: Point,
exists: ∃x:A. B[x],
and: P ∧ Q
Definitions occuring in definition :
exists: ∃x:A. B[x],
eu-point: Point,
and: P ∧ Q,
eu-midpoint: a=m=b,
eu-congruent: ab=cd
FDL editor aliases :
eu-per
Latex:
Per(a;b;c) == \mexists{}c':Point. (c=b=c' \mwedge{} ac=ac')
Date html generated:
2016_05_18-AM-06_42_26
Last ObjectModification:
2015_09_23-AM-09_00_28
Theory : euclidean!geometry
Home
Index