---

Step * 1 of Lemma k-continuous-iff-all-k-1


1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ⋂n. F[X n] ⊆ F[⋂n. X n])
4. i : ℕk
⊢ ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ((⋂n:ℕ. (F[X n] i)) ⊆r (F[⋂n. X n] i)))
BY
{ (ParallelOp -2 THEN ParallelLast THEN D -1 With ⌜i⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
3.  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].  ((\mforall{}n:\mBbbN{}.  X  (n  +  1)  \msubseteq{}  X  n)  {}\mRightarrow{}  \mcap{}n.  F[X  n]  \msubseteq{}  F[\mcap{}n.  X  n])
4.  i  :  \mBbbN{}k
\mvdash{}  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].  ((\mforall{}n:\mBbbN{}.  X  (n  +  1)  \msubseteq{}  X  n)  {}\mRightarrow{}  ((\mcap{}n:\mBbbN{}.  (F[X  n]  i))  \msubseteq{}r  (F[\mcap{}n.  X  n]  i)))


By

---

Latex:
(ParallelOp  -2  THEN  ParallelLast  THEN  D  -1  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)

---

Home Index