Step * 1 1 of Lemma cyclic-map-transitive

.....assertion..... 
1. : ℕ
2. : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. ∀x,y:ℕn.  ∃n@0:ℕ((f^n@0 x) y ∈ ℕn)
5. : ℕn
6. : ℕn
7. : ℕ
8. (f^k x) y ∈ ℕn
⊢ ∃m:ℕ1. (0 < m ∧ ((f^m x) x ∈ ℕn))
BY
xxx(RepeatFor (Thin  (-1)) THEN Thin (-2))xxx }

1
1. : ℕ
2. : ℕn ⟶ ℕn
3. Inj(ℕn;ℕn;f)
4. : ℕn
⊢ ∃m:ℕ1. (0 < m ∧ ((f^m x) x ∈ ℕn))


Latex:


Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
3.  Inj(\mBbbN{}n;\mBbbN{}n;f)
4.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((f\^{}n@0  x)  =  y)
5.  x  :  \mBbbN{}n
6.  y  :  \mBbbN{}n
7.  k  :  \mBbbN{}
8.  (f\^{}k  x)  =  y
\mvdash{}  \mexists{}m:\mBbbN{}n  +  1.  (0  <  m  \mwedge{}  ((f\^{}m  x)  =  x))


By


Latex:
xxx(RepeatFor  3  (Thin    (-1))  THEN  Thin  (-2))xxx




Home Index