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


1. SeparationSpace
2. (Point(X ⟶ ℝ) × ℝList
3. (Point(X ⟶ ℝ) × ℝList
4. Point(X)
5. : ℕ||v||
6. let f,r v[||u|| i] 
   in f(x) < r
⊢ let f,r v[i] 
  in f(x) < r
BY
(RWO "select_append_back" (-1) THEN Auto) }


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.  i  :  \mBbbN{}||v||
6.  let  f,r  =  u  @  v[||u||  +  i] 
      in  f(x)  <  r
\mvdash{}  let  f,r  =  v[i] 
    in  f(x)  <  r


By


Latex:
(RWO  "select\_append\_back"  (-1)  THEN  Auto)




Home Index