---

Step * of Lemma between-fun-connected

∀[T:Type]. ∀f:T ⟶ T. (retraction(T;f) ⇒ (∀y,x:T.  (y is f*(x) ⇒ f x is f*(y) ⇒ ((y = x ∈ T) ∨ (y = (f x) ∈ T)))))
BY
{ (xxxRepeatFor 3 ((D 0 THENA Auto))xxx THEN BLemma `fun-connected-induction` THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(xxxRepeatFor  3  ((D  0  THENA  Auto))xxx  THEN  BLemma  `fun-connected-induction`  THEN  Auto)

---

Home Index