Nuprl Definition : rpositive2

rpositive2(x) ==  ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))


Definitions occuring in Statement :  nat_plus: ℕ+,  le: A ≤ B,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  apply: f a,  multiply: n * m
Definitions occuring in definition :  exists: ∃x:A. B[x],  all: ∀x:A. B[x],  nat_plus: ℕ+,  implies: P ⇒ Q,  le: A ≤ B,  multiply: n * m,  apply: f a
FDL editor aliases :  rpositive2
Latex:
rpositive2(x)  ==    \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  (x  m))))


Date html generated: 2016_05_18-AM-07_00_32
Last ObjectModification: 2015_09_23-AM-09_01_08

Theory : reals


Home Index