Nuprl Lemma : real-fun-implies-sfun-ext
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. real-sfun(f;a;b) supposing real-fun(f;a;b)
Proof
Definitions occuring in Statement :
real-sfun: real-sfun(f;a;b),
real-fun: real-fun(f;a;b),
rfun: I ⟶ℝ,
rccint: [l, u],
rleq: x ≤ y,
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
set: {x:A| B[x]}
Definitions unfolded in proof :
member: t ∈ T,
real-fun-implies-sfun,
real-weak-Markov,
rneq-if-rabs
Lemmas referenced :
real-fun-implies-sfun,
real-weak-Markov,
rneq-if-rabs
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[a:\mBbbR{}]. \mforall{}[b:\{b:\mBbbR{}| a \mleq{} b\} ]. \mforall{}[f:[a, b] {}\mrightarrow{}\mBbbR{}]. real-sfun(f;a;b) supposing real-fun(f;a;b)
Date html generated:
2017_01_09-AM-08_59_35
Last ObjectModification:
2016_11_21-PM-03_55_06
Theory : reals
Home
Index