---

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

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].  (k-Continuous(T.F[T]) ⇐⇒ ∀i:ℕk. k-1-continuous{i:l}(k;T.F[T] i))
BY
{ (Auto THEN All (Unfolds  ``k-continuous k-1-continuous``)⋅) }

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

2
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. ∀i:ℕk. ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ((⋂n:ℕ. (F[X n] i)) ⊆r (F[⋂n. X n] i)))
⊢ ∀[X:ℕ ⟶ ℕk ⟶ Type]. ((∀n:ℕ. X (n + 1) ⊆ X n) ⇒ ⋂n. F[X n] ⊆ F[⋂n. X n])

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    (k-Continuous(T.F[T])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}k.  k-1-continuous\{i:l\}(k;T.F[T]  i))


By

---

Latex:
(Auto  THEN  All  (Unfolds    ``k-continuous  k-1-continuous``)\mcdot{})

---

Home Index