---

Step * of Lemma separable-kernel-iff

No Annotations
∀rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ ⟶ ℝ.
  (trans-kernel-fun(rv;e;f)
  ⇒ (separable-kernel(rv;e;f)
     ⇐⇒ ∃phi:ℝ ⟶ ℝ
          ∃psi:{h:Point(rv)| h ⋅ e = r0}  ⟶ {r:ℝ| r0 < r} 
           ((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((phi t) * (psi h))))
           ∧ ((phi r0) = r0)
           ∧ ((psi 0) = r1)
           ∧ (∀t,s:ℝ.  ((t < s) ⇒ ((phi t) < (phi s))))
           ∧ (∀t:ℝ. ∃s:ℝ. ((phi s) = t))
           ∧ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  (psi h1 ≠ psi h2 ⇒ h1 # h2))
           ∧ (∀t,s:ℝ.  (phi t ≠ phi s ⇒ t ≠ s)))))
BY
{ (InstLemma `separable-kernel-properties` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN ((Unfold `separable-kernel` 0 THEN RepeatFor 2 (ParallelLast) THEN Auto)
   ORELSE ((D -1 THEN ExRepD) THEN InstHyp [⌜phi⌝;⌜psi⌝] 5⋅ THEN Auto)
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}e:Point(rv).  \mforall{}f:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}.
    (trans-kernel-fun(rv;e;f)
    {}\mRightarrow{}  (separable-kernel(rv;e;f)
          \mLeftarrow{}{}\mRightarrow{}  \mexists{}phi:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}
                    \mexists{}psi:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \{r:\mBbbR{}|  r0  <  r\} 
                      ((\mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    ((f  h  t)  =  ((phi  t)  *  (psi  h))))
                      \mwedge{}  ((phi  r0)  =  r0)
                      \mwedge{}  ((psi  0)  =  r1)
                      \mwedge{}  (\mforall{}t,s:\mBbbR{}.    ((t  <  s)  {}\mRightarrow{}  ((phi  t)  <  (phi  s))))
                      \mwedge{}  (\mforall{}t:\mBbbR{}.  \mexists{}s:\mBbbR{}.  ((phi  s)  =  t))
                      \mwedge{}  (\mforall{}h1,h2:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .    (psi  h1  \mneq{}  psi  h2  {}\mRightarrow{}  h1  \#  h2))
                      \mwedge{}  (\mforall{}t,s:\mBbbR{}.    (phi  t  \mneq{}  phi  s  {}\mRightarrow{}  t  \mneq{}  s)))))


By

---

Latex:
(InstLemma  `separable-kernel-properties`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  ((Unfold  `separable-kernel`  0  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto)
  ORELSE  ((D  -1  THEN  ExRepD)  THEN  InstHyp  [\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{}]  5\mcdot{}  THEN  Auto)
  ))

---

Home Index