---

Step * of Lemma separable-kernel-properties

No Annotations
∀rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ ⟶ ℝ.
  (trans-kernel-fun(rv;e;f)
  ⇒ (∀g:ℝ ⟶ ℝ. ∀k:{h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ.
        ((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((g t) * (k h))))
        ⇒ (∃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
{ (((Auto THEN D 4) THEN (D 0 With ⌜λt.((g t) * (k 0))⌝  THENA Auto)) THEN Reduce 0) }

1
1. rv : InnerProductSpace
2. e : Point(rv)
3. f : {h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ ⟶ ℝ
4. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ.  (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2))
5. (∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0))
∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ.  ((t1 < t2) ⇒ ((f h t1) < (f h t2))))
∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ.  ∃t:ℝ. ((f h t) = r))
6. g : ℝ ⟶ ℝ
7. k : {h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ
8. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((g t) * (k h)))
⊢ ∃psi:{h:Point(rv)| h ⋅ e = r0}  ⟶ {r:ℝ| r0 < r} 
   ((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = (((g t) * (k 0)) * (psi h))))
   ∧ (((g r0) * (k 0)) = r0)
   ∧ ((psi 0) = r1)
   ∧ (∀t,s:ℝ.  ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0)))))
   ∧ (∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t))
   ∧ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  (psi h1 ≠ psi h2 ⇒ h1 # h2))
   ∧ (∀t,s:ℝ.  ((g t) * (k 0) ≠ (g s) * (k 0) ⇒ t ≠ s)))

---

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{}  (\mforall{}g:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}k:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}.
                ((\mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    ((f  h  t)  =  ((g  t)  *  (k  h))))
                {}\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:
(((Auto  THEN  D  4)  THEN  (D  0  With  \mkleeneopen{}\mlambda{}t.((g  t)  *  (k  0))\mkleeneclose{}    THENA  Auto))  THEN  Reduce  0)

---

Home Index