---

Step * 1 of Lemma implies-k-continuous


1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. k-Monotone(T.F[T])
4. ∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i)
5. i : ℕk
⊢ k-1-continuous{i:l}(k;T.F[T] i)
BY
{ (D -2 With ⌜i⌝  THEN EAuto 1) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
3.  k-Monotone(T.F[T])
4.  \mforall{}i,j:\mBbbN{}k.  \mforall{}Z:\mBbbN{}k  {}\mrightarrow{}  Type.    Continuous(X.F[\mlambda{}i.if  (i  =\msubz{}  j)  then  X  else  Z  i  fi  ]  i)
5.  i  :  \mBbbN{}k
\mvdash{}  k-1-continuous\{i:l\}(k;T.F[T]  i)


By

---

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

---

Home Index