Nuprl Lemma : nsub_finite
∀n:ℕ. finite(ℕn)
Proof
Definitions occuring in Statement :
finite: finite(T),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
natural_number: $n
Definitions unfolded in proof :
finite: finite(T),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
uimplies: b supposing a
Lemmas referenced :
equipollent_weakening_ext-eq,
int_seg_wf,
ext-eq_weakening,
equipollent_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
dependent_pairFormation,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
setElimination,
rename,
hypothesis,
because_Cache,
independent_isectElimination
Latex:
\mforall{}n:\mBbbN{}. finite(\mBbbN{}n)
Date html generated:
2016_10_21-AM-11_00_18
Last ObjectModification:
2016_08_06-PM-02_34_19
Theory : equipollence!!cardinality!
Home
Index