---

Step * of Lemma injection-is-surjection

∀n:ℕ. ∀f:ℕn ⟶ ℕn.  Surj(ℕn;ℕn;f) supposing Inj(ℕn;ℕn;f)
BY
{ (Auto THEN (Decide ∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn)) THENA Auto)) }

1
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
⊢ Surj(ℕn;ℕn;f)

2
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ¬(∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn)))
⊢ Surj(ℕn;ℕn;f)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.    Surj(\mBbbN{}n;\mBbbN{}n;f)  supposing  Inj(\mBbbN{}n;\mBbbN{}n;f)


By

---

Latex:
(Auto  THEN  (Decide  \mexists{}i:\mBbbN{}n.  \mforall{}a:\mBbbN{}n.  (\mneg{}((f  a)  =  i))  THENA  Auto))

---

Home Index