---

Step * of Lemma decidable__fun-connected

∀[T:Type]. ∀f:T ⟶ T. (retraction(T;f) ⇒ (∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀x,y:T.  Dec(x is f*(y))))
BY
{ RepeatFor 4 (xxx(D 0 THENA Auto)xxx) }

1
1. [T] : Type
2. f : T ⟶ T
3. retraction(T;f)
4. ∀x,y:T.  Dec(x = y ∈ T)
⊢ ∀x,y:T.  Dec(x is f*(y))

---

Latex:

---

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


By

---

Latex:
RepeatFor  4  (xxx(D  0  THENA  Auto)xxx)

---

Home Index