Nuprl Lemma : continuous-add-ext
∀[I:Interval]. ∀[f,g:I ⟶ℝ].
  (f[x] continuous for x ∈ I 
⇒ g[x] continuous for x ∈ I 
⇒ 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: a + b
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s]
, 
implies: P 
⇒ 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