---

Step * of Lemma fun-connected-fixedpoint

∀[T:Type]. ∀[f:T ⟶ T]. ∀[x,y:T].  (x = y ∈ T) supposing (((f y) = y ∈ T) and x is f*(y))
BY
{ xxx(Auto THEN RepeatFor 4 (MoveToConcl (-1)) THEN BLemma `fun-connected-induction`⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].  \mforall{}[x,y:T].    (x  =  y)  supposing  (((f  y)  =  y)  and  x  is  f*(y))


By

---

Latex:
xxx(Auto  THEN  RepeatFor  4  (MoveToConcl  (-1))  THEN  BLemma  `fun-connected-induction`\mcdot{}  THEN  Auto)xxx

---

Home Index