---

Step * 2 1 1 1 of Lemma infn_wf


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)))}  ⟶ ℝ
5. ∀f,g:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} .
     ((∀x:I^n - 1. ((f x) = (g x))) ⇒ ((F f) = (F g)))
6. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} . ∀z:{z:ℝ| z ∈ 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. λf.inf{F (λa.(f a++z)) | z ∈ I} ∈ {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ
8. f : {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
9. g : {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
10. ∀x:I^n. ((f x) = (g x))
⊢ inf{F (λa.(f a++z)) | z ∈ I} = inf{F (λa.(g a++z)) | z ∈ I}
BY
{ ((Assert ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b))) BY
          (DVar `f' THEN Unhide THEN Auto))
   THEN (Assert ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((g a) = (g b))) BY
               (DVar `g' THEN Unhide THEN Auto))
   ) }

1
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)))}  ⟶ ℝ
5. ∀f,g:{f:I^n - 1 ⟶ ℝ| ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} .
     ((∀x:I^n - 1. ((f x) = (g x))) ⇒ ((F f) = (F g)))
6. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} . ∀z:{z:ℝ| z ∈ 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. λf.inf{F (λa.(f a++z)) | z ∈ I} ∈ {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ
8. f : {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
9. g : {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
10. ∀x:I^n. ((f x) = (g x))
11. ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))
12. ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((g a) = (g b)))
⊢ inf{F (λa.(f a++z)) | z ∈ I} = inf{F (λa.(g a++z)) | z ∈ I}

---

Latex:

---

Latex:

1.  I  :  \{I:Interval|  icompact(I)\} 
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  F  :  \{f:I\^{}n  -  1  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n  -  1.    (req-vec(n  -  1;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\}    {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}f,g:\{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.  ((f  x)  =  (g  x)))  {}\mRightarrow{}  ((F  f)  =  (F  g)))
6.  \mforall{}f:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\}  .  \mforall{}z:\{z:\mBbbR{}|  z  \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.  \mlambda{}f.inf\{F  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\}  \mmember{}  \{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\}    {}\000C\mrightarrow{}  \mBbbR{}
8.  f  :  \{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\} 
9.  g  :  \{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\} 
10.  \mforall{}x:I\^{}n.  ((f  x)  =  (g  x))
\mvdash{}  inf\{F  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\}  =  inf\{F  (\mlambda{}a.(g  a++z))  |  z  \mmember{}  I\}


By

---

Latex:
((Assert  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))  BY
                (DVar  `f'  THEN  Unhide  THEN  Auto))
  THEN  (Assert  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((g  a)  =  (g  b)))  BY
                          (DVar  `g'  THEN  Unhide  THEN  Auto))
  )

---

Home Index