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