Nuprl Definition : rv-ge
cd ≥ ab == ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ cd=uw))
Definitions occuring in Statement :
rv-between: a-b-c,
real-vec-sep: a ≠ b,
rv-congruent: ab=cd,
real-vec: ℝ^n,
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
rv-congruent: ab=cd,
and: P ∧ Q,
rv-between: a-b-c,
not: ¬A,
real-vec-sep: a ≠ b,
real-vec: ℝ^n,
exists: ∃x:A. B[x]
FDL editor aliases :
rv-ge
Latex:
cd \mgeq{} ab == \mneg{}\mneg{}(\mexists{}u,v,w:\mBbbR{}\^{}n. ((\mneg{}(u \mneq{} v \mwedge{} v \mneq{} w \mwedge{} (\mneg{}u-v-w))) \mwedge{} ab=uv \mwedge{} cd=uw))
Date html generated:
2016_10_28-AM-07_37_21
Last ObjectModification:
2016_10_27-PM-01_16_57
Theory : reals
Home
Index