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


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


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


By


Latex:
(D  -1  THEN  (D  0  THENA  Auto)  THEN  (RWO  "select-append"  0  THENA  Auto)  THEN  AutoSplit)




Home Index