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