Nuprl Definition : eu-bisect-line
eu-bisect-line(e;a;b) == (¬(a = b ∈ Point)) ∧ (∃d:Point. (ad=db ∧ a_d_b))
Definitions occuring in Statement :
eu-between-eq: a_b_c,
eu-congruent: ab=cd,
eu-point: Point,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
eu-between-eq: a_b_c,
eu-congruent: ab=cd,
and: P ∧ Q,
eu-point: Point,
exists: ∃x:A. B[x],
equal: s = t ∈ T,
not: ¬A
FDL editor aliases :
eu-bisect-line
Latex:
eu-bisect-line(e;a;b) == (\mneg{}(a = b)) \mwedge{} (\mexists{}d:Point. (ad=db \mwedge{} a\_d\_b))
Date html generated:
2016_06_16-PM-01_31_24
Last ObjectModification:
2016_06_08-PM-02_53_58
Theory : euclidean!geometry
Home
Index