---

Step * 1 1 of Lemma strong-continuous-function


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index