Nuprl Lemma : nat2inf-injection
Inj(ℕ;ℕ∞;λn.n∞)
Proof
Definitions occuring in Statement :
nat2inf: n∞,
nat-inf: ℕ∞,
inject: Inj(A;B;f),
nat: ℕ,
lambda: λx.A[x]
Definitions unfolded in proof :
inject: Inj(A;B;f),
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
prop: ℙ
Lemmas referenced :
nat2inf-one-one,
equal_wf,
nat-inf_wf,
nat2inf_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalHypSubstitution,
sqequalRule,
lemma_by_obid,
isectElimination,
thin,
hypothesisEquality,
independent_functionElimination,
hypothesis
Latex:
Inj(\mBbbN{};\mBbbN{}\minfty{};\mlambda{}n.n\minfty{})
Date html generated:
2016_05_15-PM-01_46_54
Last ObjectModification:
2015_12_27-AM-00_09_41
Theory : basic
Home
Index