---

Step * of Lemma strong-continuity2-half-squash-surject-biject

∀[T,S,U:Type].
  ((U ⊆r ℕ)
  ⇒ (∃r:ℕ ⟶ U. ∀x:U. ((r x) = x ∈ U))
  ⇒ (∃g:ℕ ⟶ T. Surj(ℕ;T;g))
  ⇒ (∃h:S ⟶ U. Bij(S;U;h))
  ⇒ (∀F:(ℕ ⟶ T) ⟶ S
        ⇃(∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
           ∀f:ℕ ⟶ T
             ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f))))))
BY
{ TACTIC:((Auto THEN ExRepD)
          THEN (Assert ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) BY
                      (Auto
                       THEN (Assert ⇃(strong-continuity2(ℕ;λf.(F1 (g o f)))) BY
                                   (BLemma `strong-continuity2-half-squash` THEN Auto))
                       THEN (UnHalfSquash THENA Auto)
                       THEN UnHalfSquashConcl
                       THEN Auto
                       THEN FLemma `strong-continuity2_functionality_surject` [-1]
                       THEN Auto))
          THEN (D -1 With ⌜h o F⌝  THENA Auto)
          THEN (UnHalfSquash THENA Auto)
          THEN UnHalfSquashConcl
          THEN Auto) }

1
1. [T] : Type
2. [S] : Type
3. [U] : Type
4. U ⊆r ℕ
5. r : ℕ ⟶ U@i
6. ∀x:U. ((r x) = x ∈ U)
7. g : ℕ ⟶ T@i
8. Surj(ℕ;T;g)
9. h : S ⟶ U@i
10. Bij(S;U;h)
11. F : (ℕ ⟶ T) ⟶ S@i
12. strong-continuity2(T;h o F)
⊢ ∃M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (S?)
   ∀f:ℕ ⟶ T. ((∃n:ℕ. ((M n f) = (inl (F f)) ∈ (S?))) ∧ (∀n:ℕ. (M n f) = (inl (F f)) ∈ (S?) supposing ↑isl(M n f)))

---

Latex:

---

Latex:
\mforall{}[T,S,U:Type].
    ((U  \msubseteq{}r  \mBbbN{})
    {}\mRightarrow{}  (\mexists{}r:\mBbbN{}  {}\mrightarrow{}  U.  \mforall{}x:U.  ((r  x)  =  x))
    {}\mRightarrow{}  (\mexists{}g:\mBbbN{}  {}\mrightarrow{}  T.  Surj(\mBbbN{};T;g))
    {}\mRightarrow{}  (\mexists{}h:S  {}\mrightarrow{}  U.  Bij(S;U;h))
    {}\mRightarrow{}  (\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  S
                \00D9(\mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (S?)
                      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
                          ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (inl  (F  f))))
                          \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (inl  (F  f))  supposing  \muparrow{}isl(M  n  f))))))


By

---

Latex:
TACTIC:((Auto  THEN  ExRepD)
                THEN  (Assert  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(strong-continuity2(T;F))  BY
                                        (Auto
                                          THEN  (Assert  \00D9(strong-continuity2(\mBbbN{};\mlambda{}f.(F1  (g  o  f))))  BY
                                                                  (BLemma  `strong-continuity2-half-squash`  THEN  Auto))
                                          THEN  (UnHalfSquash  THENA  Auto)
                                          THEN  UnHalfSquashConcl
                                          THEN  Auto
                                          THEN  FLemma  `strong-continuity2\_functionality\_surject`  [-1]
                                          THEN  Auto))
                THEN  (D  -1  With  \mkleeneopen{}h  o  F\mkleeneclose{}    THENA  Auto)
                THEN  (UnHalfSquash  THENA  Auto)
                THEN  UnHalfSquashConcl
                THEN  Auto)

---

Home Index