---

Step * 1 3 of Lemma infn_functionality

.....wf..... 
1. ∀n1:ℕ
     (∀I:{I:Interval| icompact(I)} . ∀f,g:I^n1 ⟶ ℝ.
        ((∀x,y:I^n1.  (req-vec(n1;x;y) ⇒ ((f x) = (f y))))
        ⇒ (∀x:I^n1. ((f x) = (g x)))
        ⇒ ((infn(n1;I) f) = (infn(n1;I) g))) ∈ ℙ)
2. n : ℤ
3. 0 < n
⊢ istype(∀I:{I:Interval| icompact(I)} . ∀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))))
BY
{ ((D 1 With ⌜n - 1⌝  THENA Auto) THEN At ⌜ℙ⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  \mforall{}n1:\mBbbN{}
          (\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f,g:I\^{}n1  {}\mrightarrow{}  \mBbbR{}.
                ((\mforall{}x,y:I\^{}n1.    (req-vec(n1;x;y)  {}\mRightarrow{}  ((f  x)  =  (f  y))))
                {}\mRightarrow{}  (\mforall{}x:I\^{}n1.  ((f  x)  =  (g  x)))
                {}\mRightarrow{}  ((infn(n1;I)  f)  =  (infn(n1;I)  g)))  \mmember{}  \mBbbP{})
2.  n  :  \mBbbZ{}
3.  0  <  n
\mvdash{}  istype(\mforall{}I:\{I:Interval|  icompact(I)\}  .  \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))))


By

---

Latex:
((D  1  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)  THEN  At  \mkleeneopen{}\mBbbP{}\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index