Nuprl Lemma : fastpi-converges-ext
lim n→∞.fastpi(n) = π/2(slower)
Proof
Definitions occuring in Statement :
fastpi: fastpi(n),
half-pi: π/2(slower),
converges-to: lim n→∞.x[n] = y
Definitions unfolded in proof :
member: t ∈ T,
fastpi-converges,
fastexp: i^n,
efficient-exp-ext
Lemmas referenced :
fastpi-converges,
efficient-exp-ext
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
lim n\mrightarrow{}\minfty{}.fastpi(n) = \mpi{}/2(slower)
Date html generated:
2016_10_26-PM-00_22_47
Last ObjectModification:
2016_09_12-PM-05_42_32
Theory : reals_2
Home
Index