Nuprl Lemma : rational-lower-approx-as-rat2real

x:ℝ. ∀n:ℕ+.  ∃q:ℚ((below within 1/n) rat2real(q))


Proof




Definitions occuring in Statement :  rational-lower-approx: (below within 1/n) rat2real: rat2real(q) req: y real: nat_plus: + all: x:A. B[x] exists: x:A. B[x] rationals:
Definitions unfolded in proof :  all: x:A. B[x] rational-lower-approx: (below within 1/n) has-value: (a)↓ uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nat_plus: + real: decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: subtype_rel: A ⊆B int_nzero: -o nequal: a ≠ b ∈  rneq: x ≠ y guard: {T} iff: ⇐⇒ Q rev_implies:  Q rat2real: rat2real(q) ifthenelse: if then else fi  btrue: tt uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    \mexists{}q:\mBbbQ{}.  ((below  x  within  1/n)  =  rat2real(q))



Date html generated: 2020_05_20-AM-11_03_53
Last ObjectModification: 2019_11_21-AM-11_06_03

Theory : reals


Home Index