---

Step * 2 of Lemma strong-continuous-function


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]))
BY
{ (BLemma `subtype_rel_isect` THEN Auto) }

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

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  A  :  Type
3.  Continuous+(T.F[T])
4.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
\mvdash{}  (A  {}\mrightarrow{}  F[\mcap{}n:\mBbbN{}.  (X  n)])  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  (A  {}\mrightarrow{}  F[X  n]))


By

---

Latex:
(BLemma  `subtype\_rel\_isect`  THEN  Auto)

---

Home Index