---

Step * 1 of Lemma strong-continuity3_functionality_surject


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 ∈ ℕ))))
BY
{ ((InstHyp [⌜j o f⌝] (-4)⋅ THENA Auto) THEN Reduce -1 THEN ParallelLast THEN Auto) }

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
11. n : ℕ
12. (M n (j o f)) = (inl (F (g o (j o f)))) ∈ (ℕ?)
13. ∀m:ℕ. ((↑isl(M m (j o f))) ⇒ (m = n ∈ ℕ))
⊢ (M n (j o f)) = (inl (F f)) ∈ (ℕ?)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [S]  :  Type
3.  g  :  T  {}\mrightarrow{}  S
4.  Surj(T;S;g)
5.  F  :  (\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}?)
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}.  (((M  n  f)  =  (inl  (F  (g  o  f))))  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n))))
8.  j  :  S  {}\mrightarrow{}  T
9.  \mforall{}x:S.  ((g  (j  x))  =  x)
10.  f  :  \mBbbN{}  {}\mrightarrow{}  S
\mvdash{}  \mexists{}n:\mBbbN{}.  (((M  n  (j  o  f))  =  (inl  (F  f)))  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  (j  o  f)))  {}\mRightarrow{}  (m  =  n))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}j  o  f\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  Reduce  -1  THEN  ParallelLast  THEN  Auto)

---

Home Index