---

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

∀[B:Type]. ((∃g:ℕ ⟶ B. Surj(ℕ;B;g)) ⇒ (∀F:(ℕ ⟶ B) ⟶ ℕ. ⇃(strong-continuity3(B;F))))
BY
{ ((Auto THEN ExRepD)
   THEN (Assert ⇃(strong-continuity3(ℕ;λf.(F (g o f)))) BY
               (BLemma `strong-continuity3-half-squash` THEN Auto))
   THEN (UnHalfSquash THENA Auto)
   THEN UnHalfSquashConcl
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[B:Type].  ((\mexists{}g:\mBbbN{}  {}\mrightarrow{}  B.  Surj(\mBbbN{};B;g))  {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  B)  {}\mrightarrow{}  \mBbbN{}.  \00D9(strong-continuity3(B;F))))


By

---

Latex:
((Auto  THEN  ExRepD)
  THEN  (Assert  \00D9(strong-continuity3(\mBbbN{};\mlambda{}f.(F  (g  o  f))))  BY
                          (BLemma  `strong-continuity3-half-squash`  THEN  Auto))
  THEN  (UnHalfSquash  THENA  Auto)
  THEN  UnHalfSquashConcl
  THEN  Auto)

---

Home Index