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