---

Step * of Lemma nsub_finite'

∀n:ℕ. finite'(ℕn)
BY
{ TACTIC:(Unfold `finite\'` 0
          THEN Unfold `surject` 0
          THEN Auto
          THEN SupposeNot
          THEN (Assert ⌜n ≤ (n - 1)⌝⋅ THENL [(BackThruLemma `injection_le` THEN Auto); Auto'])) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. b : ℕn
5. ¬(∃a:ℕn. ((f a) = b ∈ ℕn))
⊢ ∃f:ℕn ⟶ ℕn - 1. Inj(ℕn;ℕn - 1;f)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  finite'(\mBbbN{}n)


By

---

Latex:
TACTIC:(Unfold  `finite\mbackslash{}'`  0
                THEN  Unfold  `surject`  0
                THEN  Auto
                THEN  SupposeNot
                THEN  (Assert  \mkleeneopen{}n  \mleq{}  (n  -  1)\mkleeneclose{}\mcdot{}  THENL  [(BackThruLemma  `injection\_le`  THEN  Auto);  Auto']))

---

Home Index