---

Step * 2 1 of Lemma fix_property

.....truecase..... 
1. [T] : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. h : T ⟶ ℕ
6. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
7. n : ℤ
8. [%4] : 0 < n
9. ∀x:T. (h x < n - 1 ⇒ (((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)))
10. x : T
11. h x < n
12. ((f x) = x ∈ T) ∨ h (f x) < h x
13. x = (f x) ∈ T
⊢ ((f x) = x ∈ T) ∧ x is f*(x)
BY
{ EAuto 1 }

---

Latex:

---

Latex:
.....truecase..... 
1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  retraction(T;f)
5.  h  :  T  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x)
7.  n  :  \mBbbZ{}
8.  [\%4]  :  0  <  n
9.  \mforall{}x:T.  (h  x  <  n  -  1  {}\mRightarrow{}  (((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x)))
10.  x  :  T
11.  h  x  <  n
12.  ((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x
13.  x  =  (f  x)
\mvdash{}  ((f  x)  =  x)  \mwedge{}  x  is  f*(x)


By

---

Latex:
EAuto  1

---

Home Index