---

Step * of Lemma retraction-fixedpoint

∀[T:Type]. ∀f:T ⟶ T. (retraction(T;f) ⇒ (∀x:T. ∃y:T. (((f y) = y ∈ T) ∧ y is f*(x))))
BY
{ xxx(Unfold `retraction` 0
      THEN (Auto THEN ExRepD)
      THEN MoveToConcl (-1)
      THEN Assert ⌜∀n:ℕ. ∀x:T.  (h x < n ⇒ (∃y:T. (((f y) = y ∈ T) ∧ y is f*(x))))⌝⋅
      THEN Try (((D 0 THENA Auto) THEN InstHyp [⌜(h x) + 1⌝;⌜x⌝] (-2)⋅ THEN Auto'))
      THEN InductionOnNat
      THEN Auto')xxx }

1
1. [T] : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. n : ℤ
6. [%2] : 0 < n
7. ∀x:T. (h x < n - 1 ⇒ (∃y:T. (((f y) = y ∈ T) ∧ y is f*(x))))
8. x : T
9. h x < n
⊢ ∃y:T. (((f y) = y ∈ T) ∧ y is f*(x))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  (retraction(T;f)  {}\mRightarrow{}  (\mforall{}x:T.  \mexists{}y:T.  (((f  y)  =  y)  \mwedge{}  y  is  f*(x))))


By

---

Latex:
xxx(Unfold  `retraction`  0
        THEN  (Auto  THEN  ExRepD)
        THEN  MoveToConcl  (-1)
        THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:T.    (h  x  <  n  {}\mRightarrow{}  (\mexists{}y:T.  (((f  y)  =  y)  \mwedge{}  y  is  f*(x))))\mkleeneclose{}\mcdot{}
        THEN  Try  (((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}(h  x)  +  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto'))
        THEN  InductionOnNat
        THEN  Auto')xxx

---

Home Index