Step
*
of Lemma
flip_bijection
∀k:ℕ. ∀i,j:ℕk.  Bij(ℕk;ℕk;(i, j))
BY
{ ((Unfold `biject` 0 THEN Unfolds ``inject surject`` 0) THEN Auto) }
1
1. k : ℕ
2. i : ℕk
3. j : ℕk
4. a1 : ℕk
5. a2 : ℕk
6. ((i, j) a1) = ((i, j) a2) ∈ ℕk
⊢ a1 = a2 ∈ ℕk
2
1. k : ℕ
2. i : ℕk
3. j : ℕk
4. ∀a1,a2:ℕk.  ((((i, j) a1) = ((i, j) a2) ∈ ℕk) 
⇒ (a1 = a2 ∈ ℕk))
5. b : ℕk
⊢ ∃a:ℕk. (((i, j) a) = b ∈ ℕk)
Latex:
Latex:
\mforall{}k:\mBbbN{}.  \mforall{}i,j:\mBbbN{}k.    Bij(\mBbbN{}k;\mBbbN{}k;(i,  j))
By
Latex:
((Unfold  `biject`  0  THEN  Unfolds  ``inject  surject``  0)  THEN  Auto)
Home
Index