Nuprl Lemma : expr_wf
∀[x:ℝ]. (expr(x) ∈ {y:ℝ| y = e^x} )
Proof
Definitions occuring in Statement :
expr: expr(x),
rexp: e^x,
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]}
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
converges-to-rexp-ext,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
expr: expr(x),
approx-rexp: approx-rexp(x;n),
real: ℝ,
nat_plus: ℕ+,
less_than: a < b,
squash: ↓T,
less_than': less_than'(a;b),
true: True,
and: P ∧ Q,
nequal: a ≠ b ∈ T ,
not: ¬A,
implies: P ⇒ Q,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
false: False,
has-value: (a)↓
Lemmas referenced :
converges-to-rexp-ext,
subtype_rel_self,
real_wf,
converges-to_wf,
approx-rexp_wf,
istype-nat,
rexp_wf,
req-from-converges,
istype-less_than,
subtype_base_sq,
int_subtype_base,
istype-int,
value-type-has-value,
int-value-type,
req_inversion,
req_wf,
converges-cauchy-witness,
cauchy-limit_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
applyEquality,
thin,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
sqequalHypSubstitution,
isectElimination,
functionEquality,
lambdaEquality_alt,
hypothesisEquality,
equalityTransitivity,
equalitySymmetry,
addEquality,
divideEquality,
setElimination,
rename,
because_Cache,
dependent_set_memberEquality_alt,
closedConclusion,
natural_numberEquality,
independent_pairFormation,
imageMemberEquality,
baseClosed,
lambdaFormation_alt,
cumulativity,
intEquality,
independent_isectElimination,
dependent_functionElimination,
independent_functionElimination,
voidElimination,
equalityIstype,
sqequalBase,
inhabitedIsType,
callbyvalueReduce,
axiomEquality,
universeIsType
Latex:
\mforall{}[x:\mBbbR{}]. (expr(x) \mmember{} \{y:\mBbbR{}| y = e\^{}x\} )
Date html generated:
2019_10_31-AM-06_11_34
Last ObjectModification:
2019_01_30-PM-02_43_54
Theory : reals_2
Home
Index