Nuprl Lemma : converges-to-rexp-ext
∀x:ℝ. lim n→∞.approx-rexp(x;n) = e^x
Proof
Definitions occuring in Statement :
approx-rexp: approx-rexp(x;n),
rexp: e^x,
converges-to: lim n→∞.x[n] = y,
real: ℝ,
all: ∀x:A. B[x]
Definitions unfolded in proof :
member: t ∈ T,
converges-to-rexp
Lemmas referenced :
converges-to-rexp
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}x:\mBbbR{}. lim n\mrightarrow{}\minfty{}.approx-rexp(x;n) = e\^{}x
Date html generated:
2019_10_31-AM-06_11_20
Last ObjectModification:
2019_04_03-AM-01_15_26
Theory : reals_2
Home
Index