Step
*
1
2
of Lemma
injection-is-surjection
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
5. ¬(n = 0 ∈ ℤ)
⊢ Surj(ℕn;ℕn;f)
BY
{ ((Assert n ≤ (n - 1) BY (BLemma `injection_le` THEN Auto))⋅ THEN Auto') }
1
.....aux.....
1. n : ℕ
2. f : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ∃i:ℕn. ∀a:ℕn. (¬((f a) = i ∈ ℕn))
5. ¬(n = 0 ∈ ℤ)
⊢ ∃f:ℕn ⟶ ℕn - 1. Inj(ℕn;ℕn - 1;f)
Latex:
Latex:
1. n : \mBbbN{}
2. f : \mBbbN{}n {}\mrightarrow{} \mBbbN{}n
3. Inj(\mBbbN{}n;\mBbbN{}n;f)
4. \mexists{}i:\mBbbN{}n. \mforall{}a:\mBbbN{}n. (\mneg{}((f a) = i))
5. \mneg{}(n = 0)
\mvdash{} Surj(\mBbbN{}n;\mBbbN{}n;f)
By
Latex:
((Assert n \mleq{} (n - 1) BY (BLemma `injection\_le` THEN Auto))\mcdot{} THEN Auto')
Home
Index