Nuprl Definition : in-real-cube
p ∈ c == ∀i:ℕk. (((c- i) ≤ (p i)) ∧ ((p i) ≤ (c+ i)))
Definitions occuring in Statement :
cube-lower: c-,
cube-upper: c+,
rleq: x ≤ y,
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
and: P ∧ Q,
cube-lower: c-,
rleq: x ≤ y,
apply: f a,
cube-upper: c+
FDL editor aliases :
in-real-cube
Latex:
p \mmember{} c == \mforall{}i:\mBbbN{}k. (((c- i) \mleq{} (p i)) \mwedge{} ((p i) \mleq{} (c+ i)))
Date html generated:
2019_10_30-AM-11_31_17
Last ObjectModification:
2019_09_27-PM-01_26_41
Theory : real!vectors
Home
Index