---

Step * of Lemma fun-connected-step

∀[T:Type]. ∀f:T ⟶ T. ∀x:T.  (Dec((f x) = x ∈ T) ⇒ f x is f*(x))
BY
{ xxx(Auto THEN UnfoldTopAb 0⋅ THEN D -1)xxx }

1
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. (f x) = x ∈ T
⊢ ∃L:T List. f x=f*(x) via L

2
1. [T] : Type
2. f : T ⟶ T
3. x : T
4. ¬((f x) = x ∈ T)
⊢ ∃L:T List. f x=f*(x) via L

---

Latex:

---

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


By

---

Latex:
xxx(Auto  THEN  UnfoldTopAb  0\mcdot{}  THEN  D  -1)xxx

---

Home Index