Step * of Lemma flip_bijection

k:ℕ. ∀i,j:ℕk.  Bij(ℕk;ℕk;(i, j))
BY
((Unfold `biject` THEN Unfolds ``inject surject`` 0) THEN Auto) }

1
1. : ℕ
2. : ℕk
3. : ℕk
4. a1 : ℕk
5. a2 : ℕk
6. ((i, j) a1) ((i, j) a2) ∈ ℕk
⊢ a1 a2 ∈ ℕk

2
1. : ℕ
2. : ℕk
3. : ℕk
4. ∀a1,a2:ℕk.  ((((i, j) a1) ((i, j) a2) ∈ ℕk)  (a1 a2 ∈ ℕk))
5. : ℕ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