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:  Q apply: a natural_number: $n
Definitions occuring in definition :  apply: 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:  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