---

Step * 1 of Lemma singleton-orbit

.....set predicate..... 
1. T : Type
2. f : T ⟶ T
3. u : T
4. (||[]|| + 1) = 1 ∈ ℤ
5. orbit(T;f;[u])
6. (∀a∈[u].∀n:ℕ. (f^n a ∈ [u]))
⊢ (f u) = u ∈ T
BY
{ (RWO "l_all_cons" (-1) THEN Auto) }

1
1. T : Type
2. f : T ⟶ T
3. u : T
4. (||[]|| + 1) = 1 ∈ ℤ
5. orbit(T;f;[u])
6. ∀n:ℕ. (f^n u ∈ [u])
7. (∀a∈[].∀n:ℕ. (f^n a ∈ [u]))
⊢ (f u) = u ∈ T

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  u  :  T
4.  (||[]||  +  1)  =  1
5.  orbit(T;f;[u])
6.  (\mforall{}a\mmember{}[u].\mforall{}n:\mBbbN{}.  (f\^{}n  a  \mmember{}  [u]))
\mvdash{}  (f  u)  =  u


By

---

Latex:
(RWO  "l\_all\_cons"  (-1)  THEN  Auto)

---

Home Index