---

Step * 1 1 of Lemma continuous-function


1. A : Type ⟶ Type
2. B : Type ⟶ Type
3. Continuous+(T.A[T])
4. Continuous(T.B[T])
5. X : ℕ ⟶ Type
6. x : ⋂n:ℕ. (A[X n] ⟶ B[X n])
7. a : A[⋂n:ℕ. (X n)]
⊢ x a ∈ ⋂n:ℕ. B[X n]
BY
{ MemTypeCD }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
MemTypeCD

---

Home Index