---

Step * 2 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)))
⊢ λf.inf{F (λa.(f a++z)) | z ∈ I} ∈ {F:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ| 
                                     ∀f,g:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} .
                                       ((∀x:I^n. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 
BY
{ (Assert ∀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)))} ) BY
         (RepeatFor 2 (Intro)
          THEN MemTypeCD
          THEN Auto
          THEN Reduce 0
          THEN DVar `f'
          THEN Unhide
          THEN Auto
          THEN BackThruSomeHyp
          THEN RWO "req-vec-extend" 0
          THEN Auto
          THEN RelRST
          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)))} )
⊢ λf.inf{F (λa.(f a++z)) | z ∈ I} ∈ {F:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ| 
                                     ∀f,g:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} .
                                       ((∀x:I^n. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 

---

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)))
\mvdash{}  \mlambda{}f.inf\{F  (\mlambda{}a.(f  a++z))  |  z  \mmember{}  I\}  \mmember{}  \{F:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}|  \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\} 
                                                                          {}\mrightarrow{}  \mBbbR{}| 
                                                                          \mforall{}f,g:\{f:I\^{}n  {}\mrightarrow{}  \mBbbR{}| 
                                                                                      \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  ((f  a)  =  (f  b)))\}  .
                                                                              ((\mforall{}x:I\^{}n.  ((f  x)  =  (g  x)))  {}\mRightarrow{}  ((F  f)  =  (F  g)))\} 


By

---

Latex:
(Assert  \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)))\}  )  \000CBY
              (RepeatFor  2  (Intro)
                THEN  MemTypeCD
                THEN  Auto
                THEN  Reduce  0
                THEN  DVar  `f'
                THEN  Unhide
                THEN  Auto
                THEN  BackThruSomeHyp
                THEN  RWO  "req-vec-extend"  0
                THEN  Auto
                THEN  RelRST
                THEN  Auto))

---

Home Index