---

Step * 1 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)))
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)))
BY
{ ((InstHyp [⌜0⌝] (-1)⋅ THENA Auto)
   THEN (D 0 With ⌜λh.(k h/k 0)⌝  THEN Auto)
   THEN Reduce 0
   THEN Auto
   THEN nRNorm 0
   THEN Auto
   THEN Try ((RWO  "10<" 0 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)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ.  ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ.  ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:Point(rv). (h ⋅ e = r0 ∈ Type)
14. h : Point(rv)
15. h ⋅ e = r0
⊢ (k h/k 0) ∈ {r:ℝ| r0 < r} 

2
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)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ.  ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ.  ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = (((g t) * (k 0)) * ((λh.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((λh.(k h/k 0)) 0) = r1
16. ∀t,s:ℝ.  ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0))))
17. ∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t)
18. h1 : {h:Point(rv)| h ⋅ e = r0} 
19. h2 : {h:Point(rv)| h ⋅ e = r0} 
20. (λh.(k h/k 0)) h1 ≠ (λh.(k h/k 0)) h2
⊢ h1 # h2

3
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)
6. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ.  ((t1 < t2) ⇒ ((f h t1) < (f h t2)))
7. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ.  ∃t:ℝ. ((f h t) = r)
8. g : ℝ ⟶ ℝ
9. k : {h:Point(rv)| h ⋅ e = r0}  ⟶ ℝ
10. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = ((g t) * (k h)))
11. ∀h:{h:Point(rv)| h ⋅ e = r0} . k h ≠ r0
12. k 0 ≠ r0
13. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ.  ((f h t) = (((g t) * (k 0)) * ((λh.(k h/k 0)) h)))
14. ((g r0) * (k 0)) = r0
15. ((λh.(k h/k 0)) 0) = r1
16. ∀t,s:ℝ.  ((t < s) ⇒ (((g t) * (k 0)) < ((g s) * (k 0))))
17. ∀t:ℝ. ∃s:ℝ. (((g s) * (k 0)) = t)
18. ∀h1,h2:{h:Point(rv)| h ⋅ e = r0} .  ((λh.(k h/k 0)) h1 ≠ (λh.(k h/k 0)) h2 ⇒ h1 # h2)
19. t : ℝ
20. s : ℝ
21. (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)))
9.  \mforall{}h:\{h:Point(rv)|  h  \mcdot{}  e  =  r0\}  .  k  h  \mneq{}  r0
\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:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}h.(k  h/k  0)\mkleeneclose{}    THEN  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto
  THEN  Try  ((RWO    "10<"  0  THEN  Auto)))

---

Home Index