---

Step * of Lemma infn_wf

No Annotations
∀[I:{I:Interval| icompact(I)} ]
  ∀n:ℕ
    (infn(n;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
{ (Unfold `infn` 0 THEN InductionOnNat THEN Reduce 0) }

1
1. I : {I:Interval| icompact(I)} 
2. n : ℤ
⊢ λf.(f ⋅) ∈ {F:{f:I^0 ⟶ ℝ| ∀a,b:I^0.  (req-vec(0;a;b) ⇒ ((f a) = (f b)))}  ⟶ ℝ| 
              ∀f,g:{f:I^0 ⟶ ℝ| ∀a,b:I^0.  (req-vec(0;a;b) ⇒ ((f a) = (f b)))} .
                ((∀x:I^0. ((f x) = (g x))) ⇒ ((F f) = (F g)))} 

2
.....upcase..... 
1. I : {I:Interval| icompact(I)} 
2. n : ℤ
3. 0 < n
4. primrec(n - 1;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I}) ∈ {F:{f:I^n - 1 ⟶ ℝ| 
                                                                ∀a,b:I^n - 1.  (req-vec(n - 1;a;b) ⇒ ((f a) = (f b)))} 
                                                             ⟶ ℝ| 
                                                             ∀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)))} 
⊢ primrec(n;λf.(f ⋅);λi,r,f. inf{r (λa.(f a++z)) | z ∈ I}) ∈ {F:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b\000C)))} 
                                                        ⟶ ℝ| 
                                                        ∀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:
No  Annotations
\mforall{}[I:\{I:Interval|  icompact(I)\}  ]
    \mforall{}n:\mBbbN{}
        (infn(n;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:
(Unfold  `infn`  0  THEN  InductionOnNat  THEN  Reduce  0)

---

Home Index