Nuprl Lemma : rabs_functionality_wrt_bdd-diff
∀x,y:ℕ+ ⟶ ℤ. (bdd-diff(x;y) ⇒ bdd-diff(|x|;|y|))
Proof
Definitions occuring in Statement :
rabs: |x|,
bdd-diff: bdd-diff(f;g),
nat_plus: ℕ+,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
rminus: -(x),
rmax: rmax(x;y),
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q
Latex:
\mforall{}x,y:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}. (bdd-diff(x;y) {}\mRightarrow{} bdd-diff(|x|;|y|))
Date html generated:
2020_05_20-AM-10_56_00
Last ObjectModification:
2020_03_20-AM-11_29_06
Theory : reals
Home
Index