Nuprl Lemma : rabs-is-zero
∀x:ℝ. (|x| = r0 ⇐⇒ x = r0)
Proof
Definitions occuring in Statement :
rabs: |x|,
req: x = y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
prop: ℙ,
rev_implies: P ⇐ Q,
uimplies: b supposing a,
guard: {T},
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
squash: ↓T,
true: True,
subtype_rel: A ⊆r B
Latex:
\mforall{}x:\mBbbR{}. (|x| = r0 \mLeftarrow{}{}\mRightarrow{} x = r0)
Date html generated:
2020_05_20-AM-11_02_12
Last ObjectModification:
2019_12_14-PM-00_54_42
Theory : reals
Home
Index