---

Step * 1 of Lemma implies-k-1-continuous


1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type].  F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
⊢ (⋂n:ℕ. F[X n]) ⊆r F[λi.⋂n:ℕ. (X n i)]
BY
{ Assert ⌜∀j:ℕ. ((⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ]))⌝⋅ }

1
.....assertion..... 
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type].  F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
⊢ ∀j:ℕ. ((⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ]))

2
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ Type
3. ∀[A,B:ℕk ⟶ Type].  F[A] ⊆r F[B] supposing A ⊆ B
4. ∀j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ])
5. X : ℕ ⟶ ℕk ⟶ Type
6. ∀n:ℕ. X (n + 1) ⊆ X n
7. ∀j:ℕ. ((⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ]))
⊢ (⋂n:ℕ. F[X n]) ⊆r F[λi.⋂n:ℕ. (X n i)]

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  Type
3.  \mforall{}[A,B:\mBbbN{}k  {}\mrightarrow{}  Type].    F[A]  \msubseteq{}r  F[B]  supposing  A  \msubseteq{}  B
4.  \mforall{}j:\mBbbN{}k.  \mforall{}Z:\mBbbN{}k  {}\mrightarrow{}  Type.    Continuous(X.F[\mlambda{}i.if  (i  =\msubz{}  j)  then  X  else  Z  i  fi  ])
5.  X  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
6.  \mforall{}n:\mBbbN{}.  X  (n  +  1)  \msubseteq{}  X  n
\mvdash{}  (\mcap{}n:\mBbbN{}.  F[X  n])  \msubseteq{}r  F[\mlambda{}i.\mcap{}n:\mBbbN{}.  (X  n  i)]


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}j:\mBbbN{}.  ((\mcap{}n:\mBbbN{}.  F[X  n])  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  F[\mlambda{}i.if  i  <z  j  then  \mcap{}n:\mBbbN{}.  (X  n  i)  else  X  n  i  fi  ]))\mkleeneclose{}\mcdot{}

---

Home Index