Nuprl Lemma : ext-finite-nat-seq_wf
∀[f:finite-nat-seq()]. ∀[x:ℕ]. (ext-finite-nat-seq(f;x) ∈ ℕ ⟶ ℕ)
Proof
Definitions occuring in Statement :
ext-finite-nat-seq: ext-finite-nat-seq(f;x),
finite-nat-seq: finite-nat-seq(),
nat: ℕ,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ext-finite-nat-seq: ext-finite-nat-seq(f;x),
finite-nat-seq: finite-nat-seq(),
nat: ℕ,
less_than: a < b,
and: P ∧ Q,
less_than': less_than'(a;b),
true: True,
squash: ↓T,
top: Top,
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ,
int_seg: {i..j-},
lelt: i ≤ j < k
Lemmas referenced :
top_wf,
less_than_wf,
int_seg_wf,
lelt_wf,
nat_wf,
finite-nat-seq_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
lambdaEquality,
setElimination,
rename,
because_Cache,
hypothesis,
hypothesisEquality,
lessCases,
independent_pairFormation,
isectElimination,
baseClosed,
natural_numberEquality,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
axiomSqEquality,
extract_by_obid,
isect_memberEquality,
voidElimination,
voidEquality,
lambdaFormation,
imageElimination,
independent_functionElimination,
applyEquality,
functionExtensionality,
dependent_set_memberEquality,
axiomEquality
Latex:
\mforall{}[f:finite-nat-seq()]. \mforall{}[x:\mBbbN{}]. (ext-finite-nat-seq(f;x) \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbN{})
Date html generated:
2019_06_20-PM-03_04_21
Last ObjectModification:
2018_08_20-PM-09_41_02
Theory : continuity
Home
Index