Nuprl Definition : real-cube-sep
c1 # c2 == ∃i:ℕk. (((c1+ i) < (c2- i)) ∨ ((c2+ i) < (c1- i)))
Definitions occuring in Statement :
cube-lower: c-,
cube-upper: c+,
rless: x < y,
int_seg: {i..j-},
exists: ∃x:A. B[x],
or: P ∨ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
or: P ∨ Q,
rless: x < y,
cube-upper: c+,
apply: f a,
cube-lower: c-
FDL editor aliases :
real-cube-sep
Latex:
c1 \# c2 == \mexists{}i:\mBbbN{}k. (((c1+ i) < (c2- i)) \mvee{} ((c2+ i) < (c1- i)))
Date html generated:
2019_10_30-AM-11_31_23
Last ObjectModification:
2019_09_27-PM-01_27_55
Theory : real!vectors
Home
Index