---

Step * of Lemma singleton-orbit

∀[T:Type]. ∀[f:T ⟶ T]. ∀[o:T List].  (o ∈ {x:T| (f x) = x ∈ T}  List) supposing (orbit(T;f;o) and (||o|| = 1 ∈ ℤ))
BY
{ (Auto
   THEN (FLemma `orbit-closed` [-1] THENA Auto)
   THEN DVar `o'
   THEN All Reduce
   THEN Auto'
   THEN Try ((DVar `v' THEN Auto'))
   THEN MemTypeCD
   THEN Auto) }

1
.....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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[o:T  List].
    (o  \mmember{}  \{x:T|  (f  x)  =  x\}    List)  supposing  (orbit(T;f;o)  and  (||o||  =  1))


By

---

Latex:
(Auto
  THEN  (FLemma  `orbit-closed`  [-1]  THENA  Auto)
  THEN  DVar  `o'
  THEN  All  Reduce
  THEN  Auto'
  THEN  Try  ((DVar  `v'  THEN  Auto'))
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index