---

Step * 2 1 of Lemma strong-continuous-function

.....wf..... 
1. F : Type ⟶ Type
2. A : Type
3. Continuous+(T.F[T])
4. X : ℕ ⟶ Type
5. n : ℕ
6. A@i
7. x : F (⋂n:ℕ. (X n))@i
⊢ x ∈ F (X n)
BY
{ (SubsumeC ⌜⋂n:ℕ. (F (X n))⌝⋅ THEN Try (Complete (Auto)))⋅ }

1
1. F : Type ⟶ Type
2. A : Type
3. Continuous+(T.F[T])
4. X : ℕ ⟶ Type
5. n : ℕ
6. A@i
7. x : F (⋂n:ℕ. (X n))@i
⊢ x ∈ ⋂n:ℕ. (F (X n))

---

Latex:

---

Latex:
.....wf..... 
1.  F  :  Type  {}\mrightarrow{}  Type
2.  A  :  Type
3.  Continuous+(T.F[T])
4.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
5.  n  :  \mBbbN{}
6.  A@i
7.  x  :  F  (\mcap{}n:\mBbbN{}.  (X  n))@i
\mvdash{}  x  \mmember{}  F  (X  n)


By

---

Latex:
(SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  (F  (X  n))\mkleeneclose{}\mcdot{}  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index