Nuprl Definition : rat-sub-cube

rat-sub-cube(k;a;b) ==  ∀i:ℕk. rat-sub-interval(a i;b i)



Definitions occuring in Statement :  rat-sub-interval: rat-sub-interval(I;J),  int_seg: {i..j-},  all: ∀x:A. B[x],  apply: f a,  natural_number: $n
Definitions occuring in definition :  all: ∀x:A. B[x],  int_seg: {i..j-},  natural_number: $n,  rat-sub-interval: rat-sub-interval(I;J),  apply: f a
FDL editor aliases :  rat-sub-cube

Latex:
rat-sub-cube(k;a;b)  ==    \mforall{}i:\mBbbN{}k.  rat-sub-interval(a  i;b  i)



Date html generated: 2020_05_20-AM-09_17_37
Last ObjectModification: 2019_11_14-PM-08_03_21

Theory : rationals


Home Index