---

Step * 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 ∈ B[⋂n:ℕ. (X n)]
BY
{ (SubsumeC ⌜⋂n:ℕ. B[X n]⌝⋅ THEN Try (Complete (Auto)))⋅ }

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)]
⊢ x a ∈ ⋂n:ℕ. B[X n]

---

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{}  B[\mcap{}n:\mBbbN{}.  (X  n)]


By

---

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

---

Home Index