---

Step * of Lemma fun_exp-fixedpoint

∀[T:Type]. ∀[f:T ⟶ T]. ∀[x:T].  ∀[n:ℕ]. ((f^n x) = x ∈ T) supposing (f x) = x ∈ T
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto) }

1
.....upcase..... 
1. T : Type
2. f : T ⟶ T
3. x : T
4. (f x) = x ∈ T
5. n : ℤ
6. 0 < n
7. (f^n - 1 x) = x ∈ T
⊢ (f^n x) = x ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[x:T].    \mforall{}[n:\mBbbN{}].  ((f\^{}n  x)  =  x)  supposing  (f  x)  =  x


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto)

---

Home Index