---

Step * 1 1 2 1 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
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
⊢ (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r (⋂n:ℕ
                                                                      F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
BY
{ (Assert ∀n:ℕ
            ((⋂m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
               ⊆r F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ]) BY
         ((D 0 THENA Auto)
          THEN (InstHyp [⌜j - 1⌝;⌜λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ⌝] 4⋅ THENA Auto)
          THEN (D -1 With ⌜λn.(X n (j - 1))⌝  THENA Auto)
          THEN Reduce -1
          THEN NthHypEq (-1)
          THEN RepeatFor 3 (EqCDA)
          THEN RepeatFor 2 (AutoSplit)
          THEN HypSubst' (-1) 0
          THEN Auto)) }

1
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 : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
11. ∀n:ℕ
      ((⋂m:ℕ. F[λi.if (i =z j - 1) then X m (j - 1) if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r F[λi.if i <z j
                                                                                                              then ⋂n:ℕ
                                                                                                                     (X 
                                                                                                                      n 
                                                                                                                      i)
                                                                                                              else X n i
                                                                                                              fi ])
⊢ (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r (⋂n:ℕ
                                                                      F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])

---

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
7.  j  :  \mBbbZ{}
8.  0  <  j
9.  (\mcap{}n:\mBbbN{}.  F[X  n])  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  F[\mlambda{}i.if  i  <z  j  -  1  then  \mcap{}n:\mBbbN{}.  (X  n  i)  else  X  n  i  fi  ])
10.  j  \mleq{}  k
\mvdash{}  (\mcap{}n:\mBbbN{}.  F[\mlambda{}i.if  i  <z  j  -  1  then  \mcap{}n:\mBbbN{}.  (X  n  i)  else  X  n  i  fi  ])  \msubseteq{}r  (\mcap{}n:\mBbbN{}
                                                                                                                                            F[\mlambda{}i.if  i  <z  j
                                                                                                                                                      then  \mcap{}n:\mBbbN{}.  (X  n  i)
                                                                                                                                                      else  X  n  i
                                                                                                                                                      fi  ])


By

---

Latex:
(Assert  \mforall{}n:\mBbbN{}
                    ((\mcap{}m:\mBbbN{}
                            F[\mlambda{}i.if  (i  =\msubz{}  j  -  1)  then  X  m  (j  -  1)
                                      if  i  <z  j  -  1  then  \mcap{}n:\mBbbN{}.  (X  n  i)
                                      else  X  n  i
                                      fi  ])  \msubseteq{}r  F[\mlambda{}i.if  i  <z  j  then  \mcap{}n:\mBbbN{}.  (X  n  i)  else  X  n  i  fi  ])  BY
              ((D  0  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}j  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  i  <z  j  -  1  then  \mcap{}n:\mBbbN{}.  (X  n  i)  else  X  n  i  fi  \mkleeneclose{}]  4\mcdot{}  THENA  Auto)
                THEN  (D  -1  With  \mkleeneopen{}\mlambda{}n.(X  n  (j  -  1))\mkleeneclose{}    THENA  Auto)
                THEN  Reduce  -1
                THEN  NthHypEq  (-1)
                THEN  RepeatFor  3  (EqCDA)
                THEN  RepeatFor  2  (AutoSplit)
                THEN  HypSubst'  (-1)  0
                THEN  Auto))

---

Home Index