---

Step * of Lemma strong-continuity3_functionality

∀[T,S:Type].  ∀e:T ~ S. ∀F:(ℕ ⟶ S) ⟶ ℕ.  (strong-continuity3(T;λf.(F ((fst(e)) o f))) ⇒ strong-continuity3(S;F))
BY
{ ((Auto THEN D 3 THEN D 4) THEN InstLemma `strong-continuity3_functionality_surject` [⌜T⌝;⌜S⌝;⌜f⌝;⌜F⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}e:T  \msim{}  S.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}.
        (strong-continuity3(T;\mlambda{}f.(F  ((fst(e))  o  f)))  {}\mRightarrow{}  strong-continuity3(S;F))


By

---

Latex:
((Auto  THEN  D  3  THEN  D  4)
  THEN  InstLemma  `strong-continuity3\_functionality\_surject`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index