---

Step * of Lemma implies-k-1-continuous

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ Type].
  ((∀[A,B:ℕk ⟶ Type].  F[A] ⊆r F[B] supposing A ⊆ B)
  ⇒ (∀j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ]))
  ⇒ k-1-continuous{i:l}(k;T.F[T]))
BY
{ (Auto THEN (D 0 THEN Auto) THEN Unfold `k-intersection` 0) }

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
⊢ (⋂n:ℕ. F[X n]) ⊆r F[λi.⋂n:ℕ. (X n i)]

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  Type].
    ((\mforall{}[A,B:\mBbbN{}k  {}\mrightarrow{}  Type].    F[A]  \msubseteq{}r  F[B]  supposing  A  \msubseteq{}  B)
    {}\mRightarrow{}  (\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  ]))
    {}\mRightarrow{}  k-1-continuous\{i:l\}(k;T.F[T]))


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  Unfold  `k-intersection`  0)

---

Home Index