Nuprl Lemma : continuous-add-ext

[I:Interval]. ∀[f,g:I ⟶ℝ].
  (f[x] continuous for x ∈  g[x] continuous for x ∈  f[x] g[x] continuous for x ∈ I)


Proof




Definitions occuring in Statement :  continuous: f[x] continuous for x ∈ I rfun: I ⟶ℝ interval: Interval radd: b uall: [x:A]. B[x] so_apply: x[s] implies:  Q
Definitions unfolded in proof :  continuous-add member: t ∈ T
Lemmas referenced :  continuous-add
Rules used in proof :  equalitySymmetry equalityTransitivity sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}[I:Interval].  \mforall{}[f,g:I  {}\mrightarrow{}\mBbbR{}].
    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  f[x]  +  g[x]  continuous  for  x  \mmember{}  I)



Date html generated: 2018_05_22-PM-02_17_32
Last ObjectModification: 2018_05_21-AM-00_32_24

Theory : reals


Home Index