---

Step * 1 of Lemma fix-connected


1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
⊢ ∀x,y:T.  (x is f*(y) ⇒ (f**(x) = f**(y) ∈ T))
BY
{ (BLemma `fun-connected-induction` THEN Auto)⋅ }

1
1. T : Type
2. eq : EqDecider(T)
3. f : T ⟶ T
4. retraction(T;f)
5. x : T
6. y : T
7. z : T
8. x = (f y) ∈ T
9. ¬(x = y ∈ T)
10. y is f*(z)
11. f**(y) = f**(z) ∈ T
⊢ f**(x) = f**(z) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  T  {}\mrightarrow{}  T
4.  retraction(T;f)
\mvdash{}  \mforall{}x,y:T.    (x  is  f*(y)  {}\mRightarrow{}  (f**(x)  =  f**(y)))


By

---

Latex:
(BLemma  `fun-connected-induction`  THEN  Auto)\mcdot{}

---

Home Index