---

Step * 1 of Lemma separable-kernel-properties


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)))
BY
{ (Assert ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0 BY
         (Auto
          THEN (InstHyp [⌜h⌝;⌜r0⌝;⌜r1⌝] 6⋅ THENA Auto)
          THEN (RWO "-3" (-1) THENA Auto)
          THEN (Assert r0 < (((g r1) - g r0) * (k h)) BY
                      Auto)
          THEN (RWO  "rmul-is-positive" (-1) THENA Auto)
          THEN D -1
          THEN Auto)) }

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)))
9. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
⊢ ∃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:

1.  rv  :  InnerProductSpace
2.  e  :  Point(rv)
3.  f  :  \{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
4.  \mforall{}h1,h2:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t1,t2:\mBbbR{}.    (f  h1  t1  \mneq{}  f  h2  t2  {}\mRightarrow{}  (h1  \#  h2  \mvee{}  t1  \mneq{}  t2))
5.  (\mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  ((f  h  r0)  =  r0))
\mwedge{}  (\mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t1,t2:\mBbbR{}.    ((t1  <  t2)  {}\mRightarrow{}  ((f  h  t1)  <  (f  h  t2))))
\mwedge{}  (\mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}r:\mBbbR{}.    \mexists{}t:\mBbbR{}.  ((f  h  t)  =  r))
6.  g  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
7.  k  :  \{h:Point(rv)|  h  \mcdot{}  e  =  r0\}    {}\mrightarrow{}  \mBbbR{}
8.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  \mforall{}t:\mBbbR{}.    ((f  h  t)  =  ((g  t)  *  (k  h)))
\mvdash{}  \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)  =  (((g  t)  *  (k  0))  *  (psi  h))))
      \mwedge{}  (((g  r0)  *  (k  0))  =  r0)
      \mwedge{}  ((psi  0)  =  r1)
      \mwedge{}  (\mforall{}t,s:\mBbbR{}.    ((t  <  s)  {}\mRightarrow{}  (((g  t)  *  (k  0))  <  ((g  s)  *  (k  0)))))
      \mwedge{}  (\mforall{}t:\mBbbR{}.  \mexists{}s:\mBbbR{}.  (((g  s)  *  (k  0))  =  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{}.    ((g  t)  *  (k  0)  \mneq{}  (g  s)  *  (k  0)  {}\mRightarrow{}  t  \mneq{}  s)))


By

---

Latex:
(Assert  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  k  h  \mneq{}  r0  BY
              (Auto
                THEN  (InstHyp  [\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
                THEN  (RWO  "-3"  (-1)  THENA  Auto)
                THEN  (Assert  r0  <  (((g  r1)  -  g  r0)  *  (k  h))  BY
                                        Auto)
                THEN  (RWO    "rmul-is-positive"  (-1)  THENA  Auto)
                THEN  D  -1
                THEN  Auto))

---

Home Index