Nuprl Definition : rpositive
rpositive(x) == ∃n:{ℕ+| 4 < x n}
Definitions occuring in Statement :
nat_plus: ℕ+,
less_than: a < b,
sq_exists: ∃x:{A| B[x]},
apply: f a,
natural_number: $n
Definitions occuring in definition :
sq_exists: ∃x:{A| B[x]},
nat_plus: ℕ+,
less_than: a < b,
natural_number: $n,
apply: f a
FDL editor aliases :
rpositive
rpositive
Latex:
rpositive(x) == \mexists{}n:\{\mBbbN{}\msupplus{}| 4 < x n\}
Date html generated:
2016_05_18-AM-07_00_26
Last ObjectModification:
2015_09_23-AM-09_01_07
Theory : reals
Home
Index