---

Step * 1 of Lemma fix_property


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. x : T
8. h x < 0
⊢ ((f f**(x)) = f**(x) ∈ T) ∧ f**(x) is f*(x)
BY
{ Auto'⋅ }

---

Latex:

---

Latex:

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.  x  :  T
8.  h  x  <  0
\mvdash{}  ((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x)


By

---

Latex:
Auto'\mcdot{}

---

Home Index