Nuprl Lemma : converges-to_functionality2
∀x1,x2:ℕ ⟶ ℝ. ∀y1,y2:ℝ. (lim n→∞.x1[n] = y1 ⇒ lim n→∞.x2[n] = y2) supposing ((y1 = y2) and (∀n:ℕ. (x1[n] = x2[n])))
Proof
Definitions occuring in Statement :
converges-to: lim n→∞.x[n] = y,
req: x = y,
real: ℝ,
nat: ℕ,
uimplies: b supposing a,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
guard: {T}
Lemmas referenced :
converges-to_functionality
Rules used in proof :
cut,
lemma_by_obid,
sqequalHypSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}x1,x2:\mBbbN{} {}\mrightarrow{} \mBbbR{}. \mforall{}y1,y2:\mBbbR{}.
(lim n\mrightarrow{}\minfty{}.x1[n] = y1 {}\mRightarrow{} lim n\mrightarrow{}\minfty{}.x2[n] = y2) supposing ((y1 = y2) and (\mforall{}n:\mBbbN{}. (x1[n] = x2[n])))
Date html generated:
2016_05_18-AM-07_35_48
Last ObjectModification:
2015_12_28-AM-00_56_36
Theory : reals
Home
Index