Nuprl Lemma : r-bound_wf
∀[x:ℝ]. (r-bound(x) ∈ ℕ+)
Proof
Definitions occuring in Statement :
r-bound: r-bound(x),
real: ℝ,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
top: Top,
implies: P ⇒ Q,
prop: ℙ,
exists: ∃x:A. B[x],
so_apply: x[s],
nat_plus: ℕ+,
so_lambda: λ2x.t[x],
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
r-bound: r-bound(x),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
equal_wf,
pi1_wf_top,
int-to-real_wf,
rabs_wf,
rleq_wf,
nat_plus_wf,
exists_wf,
real_wf,
subtype_rel_self,
integer-bound
Rules used in proof :
axiomEquality,
independent_functionElimination,
dependent_functionElimination,
equalitySymmetry,
equalityTransitivity,
voidEquality,
voidElimination,
isect_memberEquality,
independent_pairEquality,
productElimination,
lambdaFormation,
rename,
setElimination,
hypothesisEquality,
lambdaEquality,
functionEquality,
isectElimination,
sqequalHypSubstitution,
hypothesis,
extract_by_obid,
instantiate,
thin,
applyEquality,
sqequalRule,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x:\mBbbR{}]. (r-bound(x) \mmember{} \mBbbN{}\msupplus{})
Date html generated:
2018_05_22-PM-01_50_31
Last ObjectModification:
2018_05_21-AM-00_09_03
Theory : reals
Home
Index