---

Step * of Lemma continuous-function

∀[A,B:Type ⟶ Type].  (Continuous(T.A[T] ⟶ B[T])) supposing (Continuous(T.B[T]) and Continuous+(T.A[T]))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto)) THEN ExtWith [`a'] [⌜A[X 0] ⟶ B[X 0]⌝]⋅ THEN 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 ∈ B[⋂n:ℕ. (X n)]

---

Latex:

---

Latex:
\mforall{}[A,B:Type  {}\mrightarrow{}  Type].
    (Continuous(T.A[T]  {}\mrightarrow{}  B[T]))  supposing  (Continuous(T.B[T])  and  Continuous+(T.A[T]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ExtWith  [`a']  [\mkleeneopen{}A[X  0]  {}\mrightarrow{}  B[X  0]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index