Nuprl Definition : rat-cube-third
rat-cube-third(k;p;c) == in-rat-cube(k;p;c) ⇒ (∀i:ℕk. rat-interval-third(p i;c i))
Definitions occuring in Statement :
rat-interval-third: rat-interval-third(p;I),
in-rat-cube: in-rat-cube(k;p;c),
int_seg: {i..j-},
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
natural_number: $n
Definitions occuring in definition :
apply: f a,
rat-interval-third: rat-interval-third(p;I),
natural_number: $n,
int_seg: {i..j-},
all: ∀x:A. B[x],
in-rat-cube: in-rat-cube(k;p;c),
implies: P ⇒ Q
FDL editor aliases :
rat-cube-third
Latex:
rat-cube-third(k;p;c) == in-rat-cube(k;p;c) {}\mRightarrow{} (\mforall{}i:\mBbbN{}k. rat-interval-third(p i;c i))
Date html generated:
2019_11_04-PM-04_43_21
Last ObjectModification:
2019_11_04-PM-02_09_35
Theory : real!vectors
Home
Index