Step
*
2
of Lemma
infn-rleq
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. 0 < n
4. ∀f:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b)
⇒ ((f a) = (f b)))} . ∀x:I^n - 1. ((infn(n - 1;I) f) ≤ (f x)\000C)
5. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b)
⇒ ((f a) = (f b)))}
6. x : I^n
⊢ (infn(n;I) f) ≤ (f x)
BY
{ Assert ⌜∀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)))} )⌝⋅ \000C}
1
.....assertion.....
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. 0 < n
4. ∀f:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b)
⇒ ((f a) = (f b)))} . ∀x:I^n - 1. ((infn(n - 1;I) f) ≤ (f x)\000C)
5. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b)
⇒ ((f a) = (f b)))}
6. x : I^n
⊢ ∀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)))} )
2
1. I : {I:Interval| icompact(I)}
2. n : ℤ
3. 0 < n
4. ∀f:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1. (req-vec(n - 1;a;b)
⇒ ((f a) = (f b)))} . ∀x:I^n - 1. ((infn(n - 1;I) f) ≤ (f x)\000C)
5. f : {f:I^n ⟶ ℝ| ∀a,b:I^n. (req-vec(n;a;b)
⇒ ((f a) = (f b)))}
6. x : I^n
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)))} )
⊢ (infn(n;I) f) ≤ (f x)
Latex:
Latex:
1. I : \{I:Interval| icompact(I)\}
2. n : \mBbbZ{}
3. 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{}x:I\^{}n - 1.
((infn(n - 1;I) f) \mleq{} (f x))
5. f : \{f:I\^{}n {}\mrightarrow{} \mBbbR{}| \mforall{}a,b:I\^{}n. (req-vec(n;a;b) {}\mRightarrow{} ((f a) = (f b)))\}
6. x : I\^{}n
\mvdash{} (infn(n;I) f) \mleq{} (f x)
By
Latex:
Assert \mkleeneopen{}\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)))\} )\mkleeneclose{}\000C\mcdot{}
Home
Index