Nuprl Definition : in-rat-cube
in-rat-cube(k;p;c) == ∀i:ℕk. ((rat2real(fst((c i))) ≤ (p i)) ∧ ((p i) ≤ rat2real(snd((c i)))))
Definitions occuring in Statement :
rat2real: rat2real(q),
rleq: x ≤ y,
int_seg: {i..j-},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
apply: f a,
pi2: snd(t),
rat2real: rat2real(q),
rleq: x ≤ y,
pi1: fst(t),
and: P ∧ Q,
natural_number: $n,
int_seg: {i..j-},
all: ∀x:A. B[x]
FDL editor aliases :
in-rat-cube
Latex:
in-rat-cube(k;p;c) == \mforall{}i:\mBbbN{}k. ((rat2real(fst((c i))) \mleq{} (p i)) \mwedge{} ((p i) \mleq{} rat2real(snd((c i)))))
Date html generated:
2019_10_30-AM-10_12_45
Last ObjectModification:
2019_10_26-AM-11_47_58
Theory : real!vectors
Home
Index