Nuprl Lemma : rabs-difference-lower-bound
∀x,y,z:ℝ. (z < |x - y| ⇐⇒ ((z + y) < x) ∨ ((z + x) < y))
Proof
Definitions occuring in Statement :
rless: x < y,
rabs: |x|,
rsub: x - y,
radd: a + b,
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
or: P ∨ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
or: P ∨ Q,
prop: ℙ,
rev_implies: P ⇐ Q,
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
false: False,
not: ¬A
Latex:
\mforall{}x,y,z:\mBbbR{}. (z < |x - y| \mLeftarrow{}{}\mRightarrow{} ((z + y) < x) \mvee{} ((z + x) < y))
Date html generated:
2020_05_20-AM-11_02_24
Last ObjectModification:
2019_11_06-PM-05_03_59
Theory : reals
Home
Index