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. Type
2. T ⟶ T
3. 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