---

Step * of Lemma strong-continuous-function

∀[F:Type ⟶ Type]. ∀[A:Type].  Continuous+(T.A ⟶ F[T]) supposing Continuous+(T.F[T])
BY
{ (Auto THEN RepeatFor 2 ((D 0 THEN Auto))) }

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

2
1. F : Type ⟶ Type
2. A : Type
3. Continuous+(T.F[T])
4. X : ℕ ⟶ Type
⊢ (A ⟶ F[⋂n:ℕ. (X n)]) ⊆r (⋂n:ℕ. (A ⟶ F[X n]))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THEN  Auto)))

---

Home Index