---

Step * of Lemma strong-continuity2_functionality_surject

∀[T,S:Type].
  ∀g:T ⟶ S. (Surj(T;S;g) ⇒ (∀F:(ℕ ⟶ S) ⟶ ℕ. (strong-continuity2(T;λf.(F (g o f))) ⇒ strong-continuity2(S;F))))
BY
{ (Auto
   THEN (All (RWO "strong-continuity2-iff-3") THENA Auto)
   THEN FLemma `strong-continuity3_functionality_surject` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}g:T  {}\mrightarrow{}  S
        (Surj(T;S;g)
        {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}.  (strong-continuity2(T;\mlambda{}f.(F  (g  o  f)))  {}\mRightarrow{}  strong-continuity2(S;F))))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "strong-continuity2-iff-3")  THENA  Auto)
  THEN  FLemma  `strong-continuity3\_functionality\_surject`  [-1]
  THEN  Auto)

---

Home Index