Nuprl Lemma : regularize-real
∀k:ℕ+. ∀x:ℝ. (regularize(k;x) = x ∈ ℝ)
Proof
Definitions occuring in Statement :
regularize: regularize(k;f),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
real: ℝ,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
nat_plus: ℕ+
Lemmas referenced :
regular-int-seq_wf,
real_wf,
nat_plus_wf,
regularize-regular,
real-regular
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
equalitySymmetry,
sqequalHypSubstitution,
setElimination,
thin,
rename,
dependent_set_memberEquality,
hypothesis,
introduction,
extract_by_obid,
isectElimination,
natural_numberEquality,
hypothesisEquality,
dependent_functionElimination,
functionExtensionality,
applyEquality
Latex:
\mforall{}k:\mBbbN{}\msupplus{}. \mforall{}x:\mBbbR{}. (regularize(k;x) = x)
Date html generated:
2017_10_03-AM-09_09_01
Last ObjectModification:
2017_09_20-PM-06_22_43
Theory : reals
Home
Index