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 ((D THENA Auto)) THEN ExtWith [`a'] [⌜A[X 0] ⟶ B[X 0]⌝]⋅ THEN Auto) }

1
1. Type ⟶ Type
2. Type ⟶ Type
3. Continuous+(T.A[T])
4. Continuous(T.B[T])
5. : ℕ ⟶ Type
6. : ⋂n:ℕ(A[X n] ⟶ B[X n])
7. A[⋂n:ℕ(X n)]
⊢ 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