Step
*
1
1
2
1
of Lemma
implies-k-1-continuous
.....assertion.....
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
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
⊢ (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r (⋂n:ℕ
F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
BY
{ (Decide ⌜j ≤ k⌝⋅ THENA Auto) }
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
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. j ≤ k
⊢ (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r (⋂n:ℕ
F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
2
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
7. j : ℤ
8. 0 < j
9. (⋂n:ℕ. F[X n]) ⊆r (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ])
10. ¬(j ≤ k)
⊢ (⋂n:ℕ. F[λi.if i <z j - 1 then ⋂n:ℕ. (X n i) else X n i fi ]) ⊆r (⋂n:ℕ
F[λi.if i <z j then ⋂n:ℕ. (X n i) else X n i fi ])
Latex:
Latex:
.....assertion.....
1. k : \mBbbN{}
2. F : (\mBbbN{}k {}\mrightarrow{} Type) {}\mrightarrow{} Type
3. \mforall{}[A,B:\mBbbN{}k {}\mrightarrow{} Type]. F[A] \msubseteq{}r F[B] supposing A \msubseteq{} B
4. \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 ])
5. X : \mBbbN{} {}\mrightarrow{} \mBbbN{}k {}\mrightarrow{} Type
6. \mforall{}n:\mBbbN{}. X (n + 1) \msubseteq{} X n
7. j : \mBbbZ{}
8. 0 < j
9. (\mcap{}n:\mBbbN{}. F[X n]) \msubseteq{}r (\mcap{}n:\mBbbN{}. F[\mlambda{}i.if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ])
\mvdash{} (\mcap{}n:\mBbbN{}. F[\mlambda{}i.if i <z j - 1 then \mcap{}n:\mBbbN{}. (X n i) else X n i fi ]) \msubseteq{}r (\mcap{}n:\mBbbN{}
F[\mlambda{}i.if i <z j
then \mcap{}n:\mBbbN{}. (X n i)
else X n i
fi ])
By
Latex:
(Decide \mkleeneopen{}j \mleq{} k\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index