---

Step * of Lemma cyclic-map-conjugate

∀[T:Type]. ∀[g,h:T ⟶ T].
  (∀[f:cyclic-map(T)]. (g o (f o h) ∈ cyclic-map(T))) supposing 
     ((∀a:T. ((g (h a)) = a ∈ T)) and 
     (∀b:T. ((h (g b)) = b ∈ T)))
BY
{ (Auto THEN D -1 THEN D -2 THEN MemTypeCD THEN Try ((D (-1) THEN Auto))) }

1
1. T : Type
2. g : T ⟶ T
3. h : T ⟶ T
4. ∀b:T. ((h (g b)) = b ∈ T)
5. ∀a:T. ((g (h a)) = a ∈ T)
6. f : T ⟶ T
7. Inj(T;T;f)
8. ∀x,y:T.  ∃n:ℕ. ((f^n x) = y ∈ T)
⊢ g o (f o h) ∈ T →⟶ T

2
.....set predicate..... 
1. T : Type
2. g : T ⟶ T
3. h : T ⟶ T
4. ∀b:T. ((h (g b)) = b ∈ T)
5. ∀a:T. ((g (h a)) = a ∈ T)
6. f : T ⟶ T
7. Inj(T;T;f)
8. ∀x,y:T.  ∃n:ℕ. ((f^n x) = y ∈ T)
⊢ ∀x,y:T.  ∃n:ℕ. ((g o (f o h)^n x) = y ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g,h:T  {}\mrightarrow{}  T].
    (\mforall{}[f:cyclic-map(T)].  (g  o  (f  o  h)  \mmember{}  cyclic-map(T)))  supposing 
          ((\mforall{}a:T.  ((g  (h  a))  =  a))  and 
          (\mforall{}b:T.  ((h  (g  b))  =  b)))


By

---

Latex:
(Auto  THEN  D  -1  THEN  D  -2  THEN  MemTypeCD  THEN  Try  ((D  (-1)  THEN  Auto)))

---

Home Index