---

Step * 2 of Lemma ss-mem-basic-and


1. X : SeparationSpace
2. u : (Point(X ⟶ ℝ) × ℝ) List
3. v : (Point(X ⟶ ℝ) × ℝ) List
4. x : Point(X)
5. ∀i:ℕ||u @ v||. let f,r = u @ v[i] in f(x) < r
⊢ ∀i:ℕ||v||. let f,r = v[i] in f(x) < r
BY
{ ((D 0 THENA Auto) THEN (D -2 With ⌜||u|| + i⌝  THENA Auto)) }

1
1. X : SeparationSpace
2. u : (Point(X ⟶ ℝ) × ℝ) List
3. v : (Point(X ⟶ ℝ) × ℝ) List
4. x : Point(X)
5. i : ℕ||v||
6. let f,r = u @ v[||u|| + i] 
   in f(x) < r
⊢ let f,r = v[i] 
  in f(x) < r

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  u  :  (Point(X  {}\mrightarrow{}  \mBbbR{})  \mtimes{}  \mBbbR{})  List
3.  v  :  (Point(X  {}\mrightarrow{}  \mBbbR{})  \mtimes{}  \mBbbR{})  List
4.  x  :  Point(X)
5.  \mforall{}i:\mBbbN{}||u  @  v||.  let  f,r  =  u  @  v[i]  in  f(x)  <  r
\mvdash{}  \mforall{}i:\mBbbN{}||v||.  let  f,r  =  v[i]  in  f(x)  <  r


By

---

Latex:
((D  0  THENA  Auto)  THEN  (D  -2  With  \mkleeneopen{}||u||  +  i\mkleeneclose{}    THENA  Auto))

---

Home Index