Nuprl Definition : qlog-type
qlog-type(q;e) == {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e}
Definitions occuring in Statement :
qexp: r ↑ n,
qle: r ≤ s,
qless: r < s,
nat_plus: ℕ+,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
nat_plus: ℕ+,
and: P ∧ Q,
implies: P ⇒ Q,
qle: r ≤ s,
subtract: n - m,
natural_number: $n,
qless: r < s,
qexp: r ↑ n
FDL editor aliases :
qlog-type
Latex:
qlog-type(q;e) == \{n:\mBbbN{}\msupplus{}| ((e \mleq{} 1) {}\mRightarrow{} (e \mleq{} q \muparrow{} n - 1)) \mwedge{} q \muparrow{} n < e\}
Date html generated:
2016_05_15-PM-11_15_22
Last ObjectModification:
2015_09_23-AM-08_28_06
Theory : rationals
Home
Index