---

Step * of Lemma fun-connected-iff-fun_exp

∀[T:Type]. ∀f:T ⟶ T. ((∀x:T. Dec((f x) = x ∈ T)) ⇒ (∀x,y:T.  (x is f*(y) ⇐⇒ ∃n:ℕ. (x = (f^n y) ∈ T))))
BY
{ xxxAutoxxx }

1
1. [T] : Type
2. f : T ⟶ T
3. ∀x:T. Dec((f x) = x ∈ T)
4. x : T
5. y : T
6. x is f*(y)
⊢ ∃n:ℕ. (x = (f^n y) ∈ T)

2
1. [T] : Type
2. f : T ⟶ T
3. ∀x:T. Dec((f x) = x ∈ T)
4. x : T
5. y : T
6. ∃n:ℕ. (x = (f^n y) ∈ T)
⊢ x is f*(y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  ((\mforall{}x:T.  Dec((f  x)  =  x))  {}\mRightarrow{}  (\mforall{}x,y:T.    (x  is  f*(y)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (x  =  (f\^{}n  y)))))


By

---

Latex:
xxxAutoxxx

---

Home Index