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