Nuprl Lemma : real-fun_wf
∀[a,b:ℝ]. ∀[f:[a, b] ⟶ℝ]. (real-fun(f;a;b) ∈ ℙ)
Proof
Definitions occuring in Statement :
real-fun: real-fun(f;a;b),
rfun: I ⟶ℝ,
rccint: [l, u],
real: ℝ,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
real-fun: real-fun(f;a;b),
all: ∀x:A. B[x],
top: Top,
prop: ℙ,
and: P ∧ Q,
implies: P ⇒ Q,
rfun: I ⟶ℝ
Lemmas referenced :
member_rccint_lemma,
istype-void,
real_wf,
rleq_wf,
req_wf,
rfun_wf,
rccint_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality_alt,
voidElimination,
hypothesis,
functionEquality,
setEquality,
productEquality,
isectElimination,
hypothesisEquality,
setElimination,
rename,
applyEquality,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
universeIsType,
isectIsTypeImplies,
inhabitedIsType
Latex:
\mforall{}[a,b:\mBbbR{}]. \mforall{}[f:[a, b] {}\mrightarrow{}\mBbbR{}]. (real-fun(f;a;b) \mmember{} \mBbbP{})
Date html generated:
2019_10_30-AM-07_14_37
Last ObjectModification:
2019_10_09-PM-03_41_14
Theory : reals
Home
Index