---

Step * 1 of Lemma strong-continuity3-half-squash-surject


1. [B] : Type
2. g : ℕ ⟶ B
3. Surj(ℕ;B;g)
4. F : (ℕ ⟶ B) ⟶ ℕ
5. strong-continuity3(ℕ;λf.(F (g o f)))
⊢ strong-continuity3(B;F)
BY
{ (FLemma `strong-continuity3_functionality_surject` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  [B]  :  Type
2.  g  :  \mBbbN{}  {}\mrightarrow{}  B
3.  Surj(\mBbbN{};B;g)
4.  F  :  (\mBbbN{}  {}\mrightarrow{}  B)  {}\mrightarrow{}  \mBbbN{}
5.  strong-continuity3(\mBbbN{};\mlambda{}f.(F  (g  o  f)))
\mvdash{}  strong-continuity3(B;F)


By

---

Latex:
(FLemma  `strong-continuity3\_functionality\_surject`  [-1]  THEN  Auto)

---

Home Index