Step
*
1
of Lemma
k-continuous-iff-all-k-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)))
BY
{ (ParallelOp -2 THEN ParallelLast THEN D -1 With ⌜i⌝ THEN Auto) }
Latex:
Latex:
1. k : \mBbbN{}
2. F : (\mBbbN{}k {}\mrightarrow{} Type) {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type
3. \mforall{}[X:\mBbbN{} {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type]. ((\mforall{}n:\mBbbN{}. X (n + 1) \msubseteq{} X n) {}\mRightarrow{} \mcap{}n. F[X n] \msubseteq{} F[\mcap{}n. X n])
4. i : \mBbbN{}k
\mvdash{} \mforall{}[X:\mBbbN{} {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type]. ((\mforall{}n:\mBbbN{}. X (n + 1) \msubseteq{} X n) {}\mRightarrow{} ((\mcap{}n:\mBbbN{}. (F[X n] i)) \msubseteq{}r (F[\mcap{}n. X n] i)))
By
Latex:
(ParallelOp -2 THEN ParallelLast THEN D -1 With \mkleeneopen{}i\mkleeneclose{} THEN Auto)
Home
Index