Nuprl Lemma : continuous-rnexp

I:Interval. ∀n:ℕ.  x^n continuous for x ∈ I


Proof




Definitions occuring in Statement :  continuous: f[x] continuous for x ∈ I interval: Interval rnexp: x^k1 nat: all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] label: ...$L... t rfun: I ⟶ℝ nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False and: P ∧ Q prop: so_apply: x[s] rnexp: x^k1 ifthenelse: if then else fi  eq_int: (i =z j) btrue: tt int-to-real: r(n) rfun-eq: rfun-eq(I;f;g) r-ap: f(x) nat_plus: + uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q)

Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}.    x\^{}n  continuous  for  x  \mmember{}  I



Date html generated: 2020_05_20-PM-00_24_03
Last ObjectModification: 2020_01_02-PM-01_57_39

Theory : reals


Home Index