---

Step * 1 of Lemma strong-continuous-function


1. F : Type ⟶ Type
2. A : Type
3. Continuous+(T.F[T])
4. X : ℕ ⟶ Type
⊢ (⋂n:ℕ. (A ⟶ F[X n])) ⊆r (A ⟶ F[⋂n:ℕ. (X n)])
BY
{ ((D 0 THEN Auto) THEN ExtWith [`a'] [⌜A ⟶ F[X 0]⌝]⋅ THEN Auto) }

1
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)]

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  A  :  Type
3.  Continuous+(T.F[T])
4.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
\mvdash{}  (\mcap{}n:\mBbbN{}.  (A  {}\mrightarrow{}  F[X  n]))  \msubseteq{}r  (A  {}\mrightarrow{}  F[\mcap{}n:\mBbbN{}.  (X  n)])


By

---

Latex:
((D  0  THEN  Auto)  THEN  ExtWith  [`a']  [\mkleeneopen{}A  {}\mrightarrow{}  F[X  0]\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index