---

Step * of Lemma nat2inf-injection

Inj(ℕ;ℕ∞;λn.n∞)
BY
{ ((D 0 THEN Auto) THEN Reduce (-1) THEN BLemma `nat2inf-one-one`  THEN Auto) }

---

Latex:

---

Latex:
Inj(\mBbbN{};\mBbbN{}\minfty{};\mlambda{}n.n\minfty{})


By

---

Latex:
((D  0  THEN  Auto)  THEN  Reduce  (-1)  THEN  BLemma  `nat2inf-one-one`    THEN  Auto)

---

Home Index