---

Step * of Lemma implies-k-continuous

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
  (k-Monotone(T.F[T])
  ⇒ (∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i))
  ⇒ k-Continuous(T.F[T]))
BY
{ (Auto THEN BLemma `k-continuous-iff-all-k-1` THEN Auto) }

1
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)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    (k-Monotone(T.F[T])
    {}\mRightarrow{}  (\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))
    {}\mRightarrow{}  k-Continuous(T.F[T]))


By

---

Latex:
(Auto  THEN  BLemma  `k-continuous-iff-all-k-1`  THEN  Auto)

---

Home Index