Nuprl Lemma : rsqrt_wf
∀[x:{x:ℝ| r0 ≤ x} ]. (rsqrt(x) ∈ {r:ℝ| (r0 ≤ r) ∧ ((r * r) = x)} )
Proof
Definitions occuring in Statement :
rsqrt: rsqrt(x),
rleq: x ≤ y,
req: x = y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rsqrt: rsqrt(x),
int_upper: {i...},
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
false: False,
subtype_rel: A ⊆r B
Latex:
\mforall{}[x:\{x:\mBbbR{}| r0 \mleq{} x\} ]. (rsqrt(x) \mmember{} \{r:\mBbbR{}| (r0 \mleq{} r) \mwedge{} ((r * r) = x)\} )
Date html generated:
2020_05_20-PM-00_31_44
Last ObjectModification:
2019_12_14-PM-03_09_09
Theory : reals
Home
Index