Nuprl Definition : pointwise-rleq
x[k] ≤ y[k] for k ∈ [n,m] == ∀k:ℤ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ y[k]))
Definitions occuring in Statement :
rleq: x ≤ y,
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int: ℤ
Definitions occuring in definition :
all: ∀x:A. B[x],
int: ℤ,
implies: P ⇒ Q,
le: A ≤ B,
rleq: x ≤ y
FDL editor aliases :
pointwise-rleq
pointwise-rleq
Latex:
x[k] \mleq{} y[k] for k \mmember{} [n,m] == \mforall{}k:\mBbbZ{}. ((n \mleq{} k) {}\mRightarrow{} (k \mleq{} m) {}\mRightarrow{} (x[k] \mleq{} y[k]))
Date html generated:
2016_05_18-AM-07_44_34
Last ObjectModification:
2015_09_23-AM-09_02_46
Theory : reals
Home
Index