Step
*
2
2
1
1
1
1
1
1
of Lemma
infn-rleq
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. 0 < n
4. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))}
5. x : I^n
6. ∀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)))} )
7. x (n - 1) ∈ {x:ℝ| x ∈ I}
8. (infn(n - 1;I) (λa.(f a++x (n - 1)))) ≤ (f x++x (n - 1))
9. ∀f,g:I^n ⟶ ℝ.
((∀x,y:I^n. (req-vec(n;x;y) ⇒ ((f x) = (f y))))
⇒ (∀x:I^n. ((f x) = (g x)))
⇒ (inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} = inf{infn(n - 1;I) (λa.(g a++z)) | z ∈ I}))
10. ∀f,g:I^n - 1 ⟶ ℝ.
((∀x,y:I^n - 1. (req-vec(n - 1;x;y) ⇒ ((f x) = (f y))))
⇒ (∀x:I^n - 1. ((f x) = (g x)))
⇒ ((infn(n - 1;I) f) = (infn(n - 1;I) g)))
11. ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))
12. inf(infn(n - 1;I) (λa.(f a++x))(x∈I)) = inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I}
⊢ inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} ≤ (f x)
BY
{ (Assert inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} ≤ (infn(n - 1;I) (λa.(f a++x (n - 1)))) BY
(D -1
THEN BackThruHyp' (-2)
THEN Auto
THEN RepUR ``rrange rset-member`` 0
THEN D 0 With ⌜x (n - 1)⌝
THEN Auto
THEN MemTypeHD 7
THEN Unhide
THEN Auto)) }
1
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. 0 < n
4. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))}
5. x : I^n
6. ∀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)))} )
7. x (n - 1) ∈ {x:ℝ| x ∈ I}
8. (infn(n - 1;I) (λa.(f a++x (n - 1)))) ≤ (f x++x (n - 1))
9. ∀f,g:I^n ⟶ ℝ.
((∀x,y:I^n. (req-vec(n;x;y) ⇒ ((f x) = (f y))))
⇒ (∀x:I^n. ((f x) = (g x)))
⇒ (inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} = inf{infn(n - 1;I) (λa.(g a++z)) | z ∈ I}))
10. ∀f,g:I^n - 1 ⟶ ℝ.
((∀x,y:I^n - 1. (req-vec(n - 1;x;y) ⇒ ((f x) = (f y))))
⇒ (∀x:I^n - 1. ((f x) = (g x)))
⇒ ((infn(n - 1;I) f) = (infn(n - 1;I) g)))
11. ∀a,b:I^n. (req-vec(n;a;b) ⇒ ((f a) = (f b)))
12. inf(infn(n - 1;I) (λa.(f a++x))(x∈I)) = inf{infn(n - 1;I) (λa.(f a++x)) | x ∈ I}
13. inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} ≤ (infn(n - 1;I) (λa.(f a++x (n - 1))))
⊢ inf{infn(n - 1;I) (λa.(f a++z)) | z ∈ I} ≤ (f x)
Latex:
Latex:
1. I : \{I:Interval| icompact(I)\}
2. n : \mBbbZ{}
3. 0 < n
4. f : \{f:I\^{}n {}\mrightarrow{} \mBbbR{}| \mforall{}a,b:I\^{}n. (req-vec(n;a;b) {}\mRightarrow{} ((f a) = (f b)))\}
5. x : I\^{}n
6. \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)))\} )
7. x (n - 1) \mmember{} \{x:\mBbbR{}| x \mmember{} I\}
8. (infn(n - 1;I) (\mlambda{}a.(f a++x (n - 1)))) \mleq{} (f x++x (n - 1))
9. \mforall{}f,g:I\^{}n {}\mrightarrow{} \mBbbR{}.
((\mforall{}x,y:I\^{}n. (req-vec(n;x;y) {}\mRightarrow{} ((f x) = (f y))))
{}\mRightarrow{} (\mforall{}x:I\^{}n. ((f x) = (g x)))
{}\mRightarrow{} (inf\{infn(n - 1;I) (\mlambda{}a.(f a++z)) | z \mmember{} I\} = inf\{infn(n - 1;I) (\mlambda{}a.(g a++z)) | z \mmember{} I\}))
10. \mforall{}f,g:I\^{}n - 1 {}\mrightarrow{} \mBbbR{}.
((\mforall{}x,y:I\^{}n - 1. (req-vec(n - 1;x;y) {}\mRightarrow{} ((f x) = (f y))))
{}\mRightarrow{} (\mforall{}x:I\^{}n - 1. ((f x) = (g x)))
{}\mRightarrow{} ((infn(n - 1;I) f) = (infn(n - 1;I) g)))
11. \mforall{}a,b:I\^{}n. (req-vec(n;a;b) {}\mRightarrow{} ((f a) = (f b)))
12. 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{} inf\{infn(n - 1;I) (\mlambda{}a.(f a++z)) | z \mmember{} I\} \mleq{} (f x)
By
Latex:
(Assert inf\{infn(n - 1;I) (\mlambda{}a.(f a++z)) | z \mmember{} I\} \mleq{} (infn(n - 1;I) (\mlambda{}a.(f a++x (n - 1)))) BY
(D -1
THEN BackThruHyp' (-2)
THEN Auto
THEN RepUR ``rrange rset-member`` 0
THEN D 0 With \mkleeneopen{}x (n - 1)\mkleeneclose{}
THEN Auto
THEN MemTypeHD 7
THEN Unhide
THEN Auto))
Home
Index