Nuprl Lemma : rat_term_to_real_wf
∀[t:rat_term()]. ∀[f:ℤ ⟶ ℝ]. (rat_term_to_real(f;t) ∈ P:ℙ × ℝ supposing P)
Proof
Definitions occuring in Statement :
rat_term_to_real: rat_term_to_real(f;t),
rat_term: rat_term(),
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
function: x:A ⟶ B[x],
product: x:A × B[x],
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rat_term_to_real: rat_term_to_real(f;t),
prop: ℙ,
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
and: P ∧ Q,
subtype_rel: A ⊆r B,
cand: A c∧ B,
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2]
Lemmas referenced :
rat_term_ind_wf_simple,
real_wf,
true_wf,
int-to-real_wf,
istype-true,
radd_wf,
uimplies_subtype,
rsub_wf,
rmul_wf,
rneq_wf,
rdiv_wf,
rminus_wf,
istype-int,
rat_term_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
closedConclusion,
productEquality,
universeEquality,
isectEquality,
cumulativity,
hypothesisEquality,
hypothesis,
lambdaEquality_alt,
dependent_pairEquality_alt,
isect_memberEquality_alt,
isectIsType,
universeIsType,
because_Cache,
applyEquality,
productElimination,
independent_isectElimination,
productIsType,
inhabitedIsType,
natural_numberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
functionIsType,
isectIsTypeImplies
Latex:
\mforall{}[t:rat\_term()]. \mforall{}[f:\mBbbZ{} {}\mrightarrow{} \mBbbR{}]. (rat\_term\_to\_real(f;t) \mmember{} P:\mBbbP{} \mtimes{} \mBbbR{} supposing P)
Date html generated:
2019_10_29-AM-09_40_32
Last ObjectModification:
2019_04_01-AM-00_13_39
Theory : reals
Home
Index