---

Step * of Lemma fun-connected-to-same

∀[T:Type]
  ∀f:T ⟶ T
    (retraction(T;f)
    ⇒ (∀x,y:T.  Dec(x = y ∈ T))
    ⇒ (∀x,z:T.  (x is f*(z) ⇒ (∀y:T. (y is f*(z) ⇒ (x is f*(y) ∨ y is f*(x)))))))
BY
{ (xxxRepeatFor 4 ((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. ∀x,y:T.  Dec(x = y ∈ T)
5. x : T
6. z : T
7. z1 : T
8. x = (f z) ∈ T
9. ¬(x = z ∈ T)
10. z is f*(z1)
11. ∀y@0:T. (y@0 is f*(z1) ⇒ (z is f*(y@0) ∨ y@0 is f*(z)))
12. y : T
13. y is f*(z1)
⊢ x is f*(y) ∨ y is f*(x)

---

Latex:

---

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


By

---

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

---

Home Index