Step
*
2
of Lemma
bijection_restriction
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Bij(ℕk;ℕk;f)
5. (f (k - 1)) = (k - 1) ∈ ℤ
6. f ∈ ℕk - 1 ⟶ ℕk - 1
7. f ∈ ℕk - 1 ⟶ ℕk - 1
⊢ Bij(ℕk - 1;ℕk - 1;f)
BY
{ RepeatFor 4 (ParallelOp (-4)) }
1
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Surj(ℕk;ℕk;f)
5. ∀a1,a2:ℕk.  (((f a1) = (f a2) ∈ ℕk) 
⇒ (a1 = a2 ∈ ℕk))
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. a1 : ℕk - 1
10. ∀a2:ℕk. (((f a1) = (f a2) ∈ ℕk) 
⇒ (a1 = a2 ∈ ℕk))
⊢ ∀a2:ℕk - 1. (((f a1) = (f a2) ∈ ℕk - 1) 
⇒ (a1 = a2 ∈ ℕk - 1))
2
1. k : ℕ
2. f : ℕk ⟶ ℕk
3. 0 < k
4. Inj(ℕk;ℕk;f)
5. ∀b:ℕk. ∃a:ℕk. ((f a) = b ∈ ℕk)
6. (f (k - 1)) = (k - 1) ∈ ℤ
7. f ∈ ℕk - 1 ⟶ ℕk - 1
8. f ∈ ℕk - 1 ⟶ ℕk - 1
9. b : ℕk - 1
10. ∃a:ℕk. ((f a) = b ∈ ℕk)
⊢ ∃a:ℕk - 1. ((f a) = b ∈ ℕk - 1)
Latex:
Latex:
1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k
3.  0  <  k
4.  Bij(\mBbbN{}k;\mBbbN{}k;f)
5.  (f  (k  -  1))  =  (k  -  1)
6.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
7.  f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1
\mvdash{}  Bij(\mBbbN{}k  -  1;\mBbbN{}k  -  1;f)
By
Latex:
RepeatFor  4  (ParallelOp  (-4))
Home
Index