---

Step * of Lemma strong-continuity3_functionality_surject

∀[T,S:Type].
  ∀g:T ⟶ S. (Surj(T;S;g) ⇒ (∀F:(ℕ ⟶ S) ⟶ ℕ. (strong-continuity3(T;λf.(F (g o f))) ⇒ strong-continuity3(S;F))))
BY
{ (Auto
   THEN D -1
   THEN Reduce -1
   THEN (FLemma `surject-inverse` [4] THENA Auto)
   THEN D -1
   THEN RenameVar `j' (-2)
   THEN D 0 With ⌜λn,f. (M n (j o f))⌝ 
   THEN Auto
   THEN Reduce 0) }

1
1. [T] : Type
2. [S] : Type
3. g : T ⟶ S
4. Surj(T;S;g)
5. F : (ℕ ⟶ S) ⟶ ℕ
6. M : n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ?)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (((M n f) = (inl (F (g o f))) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
8. j : S ⟶ T
9. ∀x:S. ((g (j x)) = x ∈ S)
10. f : ℕ ⟶ S
⊢ ∃n:ℕ. (((M n (j o f)) = (inl (F f)) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m (j o f))) ⇒ (m = n ∈ ℕ))))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  Reduce  -1
  THEN  (FLemma  `surject-inverse`  [4]  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `j'  (-2)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}n,f.  (M  n  (j  o  f))\mkleeneclose{} 
  THEN  Auto
  THEN  Reduce  0)

---

Home Index