Nuprl Lemma : rat2real-qsub
∀[a,b:ℚ]. (rat2real(a - b) = (rat2real(a) - rat2real(b)))
Proof
Definitions occuring in Statement :
rat2real: rat2real(q),
rsub: x - y,
req: x = y,
uall: ∀[x:A]. B[x],
qsub: r - s,
rationals: ℚ
Definitions unfolded in proof :
qsub: r - s,
rat2real: rat2real(q),
ifthenelse: if b then t else f fi ,
btrue: tt,
int-to-real: r(n),
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
req_int_terms: t1 ≡ t2,
false: False,
not: ¬A,
top: Top
Latex:
\mforall{}[a,b:\mBbbQ{}]. (rat2real(a - b) = (rat2real(a) - rat2real(b)))
Date html generated:
2020_05_20-AM-11_01_49
Last ObjectModification:
2019_12_09-AM-00_01_30
Theory : reals
Home
Index