Step
*
2
2
1
1
of Lemma
infn-property
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. [%1] : 0 < n
4. ∀f:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} . ∀e:{e:ℝ| r0 < e} .
∃x:I^n - 1. ((f x) ≤ ((infn(n - 1;I) f) + e))
5. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))}
6. e : {e:ℝ| r0 < e}
7. ∀z:{x:ℝ| x ∈ I} . (λa.(f a++z) ∈ {f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} )
8. ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))
9. ∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ ((infn(n - 1;I) (λa.(f a++x))) = (infn(n - 1;I) (λa.(f a++y)))))
10. inf(infn(n - 1;I) (λa.(f a++x))(x∈I)) = inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I}
⊢ ∃x:I^n. ((f x) ≤ (inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} + e))
BY
{ (D -1
THEN (InstHyp [⌜(e/r(2))⌝] (-1)⋅ THENA (Auto THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
THEN ExRepD
THEN RepUR ``rset-member rrange`` -2
THEN ExRepD
THEN RenameVar `z' (-4)
THEN (InstHyp [⌜z⌝] 7⋅ THENA Auto)
THEN (InstHyp [⌜λa.(f a++z)⌝;⌜(e/r(2))⌝] 4⋅ THENA (Auto THEN MemTypeCD THEN Auto THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
THEN ExRepD
THEN Reduce -1) }
1
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. [%1] : 0 < n
4. ∀f:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} . ∀e:{e:ℝ| r0 < e} .
∃x:I^n - 1. ((f x) ≤ ((infn(n - 1;I) f) + e))
5. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))}
6. e : {e:ℝ| r0 < e}
7. ∀z:{x:ℝ| x ∈ I} . (λa.(f a++z) ∈ {f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} )
8. ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))
9. ∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ ((infn(n - 1;I) (λa.(f a++x))) = (infn(n - 1;I) (λa.(f a++y)))))
10. lower-bound(infn(n - 1;I) (λa.(f a++x))(x∈I);inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I})
11. ∀e:ℝ
((r0 < e)
⇒ (∃x:ℝ. ((x ∈ infn(n - 1;I) (λa.(f a++x))(x∈I)) ∧ (x < (inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I} + e)))))
12. x : ℝ
13. z : ℝ
14. z ∈ I
15. (infn(n - 1;I) (λa.(f a++z))) = x
16. x < (inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I} + (e/r(2)))
17. λa.(f a++z) ∈ {f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))}
18. x1 : I^n - 1
19. (f x1++z) ≤ ((infn(n - 1;I) (λa.(f a++z))) + (e/r(2)))
⊢ ∃x:I^n. ((f x) ≤ (inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} + e))
Latex:
Latex:
1. I : \{I:Interval| icompact(I)\}
2. n : \mBbbZ{}
3. [\%1] : 0 < n
4. \mforall{}f:\{f:I\^{}n - 1 {}\mrightarrow{} \mBbbR{}| \mforall{}a,b:I\^{}n - 1. (req-vec(n - 1;a;b) {}\mRightarrow{} ((f a) = (f b)))\} . \mforall{}e:\{e:\mBbbR{}| r0 < e\} .
\mexists{}x:I\^{}n - 1. ((f x) \mleq{} ((infn(n - 1;I) f) + e))
5. f : \{f:I\^{}n {}\mrightarrow{} \mBbbR{}| \mforall{}a,b:I\^{}n. (req-vec(n;a;b) {}\mRightarrow{} ((f a) = (f b)))\}
6. e : \{e:\mBbbR{}| r0 < e\}
7. \mforall{}z:\{x:\mBbbR{}| x \mmember{} I\}
(\mlambda{}a.(f a++z) \mmember{} \{f:I\^{}n - 1 {}\mrightarrow{} \mBbbR{}| \mforall{}a,b:I\^{}n - 1. (req-vec(n - 1;a;b) {}\mRightarrow{} ((f a) = (f b)))\} )
8. \mforall{}a,b:I\^{}n. (req-vec(n;a;b) {}\mRightarrow{} ((f a) = (f b)))
9. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . ((x = y) {}\mRightarrow{} ((infn(n - 1;I) (\mlambda{}a.(f a++x))) = (infn(n - 1;I) (\mlambda{}a.(f a++y)))))
10. inf(infn(n - 1;I) (\mlambda{}a.(f a++x))(x\mmember{}I)) = inf\{infn(n - 1;I) (\mlambda{}a.(f a++x)) | x \mmember{} I\}
\mvdash{} \mexists{}x:I\^{}n. ((f x) \mleq{} (inf\{infn(n - 1;I) (\mlambda{}a.(f a++z)) | z \mmember{} I\} + e))
By
Latex:
(D -1
THEN (InstHyp [\mkleeneopen{}(e/r(2))\mkleeneclose{}] (-1)\mcdot{} THENA (Auto THEN nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN ExRepD
THEN RepUR ``rset-member rrange`` -2
THEN ExRepD
THEN RenameVar `z' (-4)
THEN (InstHyp [\mkleeneopen{}z\mkleeneclose{}] 7\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}\mlambda{}a.(f a++z)\mkleeneclose{};\mkleeneopen{}(e/r(2))\mkleeneclose{}] 4\mcdot{}
THENA (Auto THEN MemTypeCD THEN Auto THEN nRMul \mkleeneopen{}r(2)\mkleeneclose{} 0\mcdot{} THEN Auto)
)
THEN ExRepD
THEN Reduce -1)
Home
Index