Nuprl Definition : ip-gt
cd > ab == ↓∃w:Point. (c_w_d ∧ cw=ab ∧ w # d)
Definitions occuring in Statement :
ip-between: a_b_c,
ip-congruent: ab=cd,
ss-sep: x # y,
ss-point: Point,
exists: ∃x:A. B[x],
squash: ↓T,
and: P ∧ Q
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
ss-point: Point,
ip-between: a_b_c,
and: P ∧ Q,
ip-congruent: ab=cd,
ss-sep: x # y
FDL editor aliases :
ip-gt
Latex:
cd > ab == \mdownarrow{}\mexists{}w:Point. (c\_w\_d \mwedge{} cw=ab \mwedge{} w \# d)
Date html generated:
2017_10_05-AM-00_02_23
Last ObjectModification:
2017_03_19-PM-02_53_22
Theory : inner!product!spaces
Home
Index