---

Step * 1 1 of Lemma singleton-orbit


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
BY
{ (Thin (-1) THEN (InstHyp [⌜1⌝] (-1)⋅ THENA Auto) THEN Reduce (-1) THEN RWO "member_singleton" (-1) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  (-1)
  THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RWO  "member\_singleton"  (-1)
  THEN  Auto)

---

Home Index