Nuprl Lemma : rleq-limit

[x,y:ℕ ⟶ ℝ]. ∀[a,b:ℝ].  (a ≤ b) supposing ((∀n:ℕ(x[n] ≤ y[n])) and lim n→∞.y[n] and lim n→∞.x[n] a)


Definitions occuring in Statement :  converges-to: lim n→∞.x[n] y rleq: x ≤ y real: nat: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q rleq: x ≤ y rnonneg: rnonneg(x) le: A ≤ B and: P ∧ Q prop: uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y guard: {T} req_int_terms: t1 ≡ t2 false: False not: ¬A top: Top rsub: y

\mforall{}[x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[a,b:\mBbbR{}].
    (a  \mleq{}  b)  supposing  ((\mforall{}n:\mBbbN{}.  (x[n]  \mleq{}  y[n]))  and  lim  n\mrightarrow{}\minfty{}.y[n]  =  b  and  lim  n\mrightarrow{}\minfty{}.x[n]  =  a)

Date html generated: 2020_05_20-AM-11_16_05
Last ObjectModification: 2020_01_02-PM-02_11_36

Theory : reals

Home Index