---

Step * of Lemma ss-mem-basic-and

No Annotations
∀[X:SeparationSpace]. ∀u,v:ss-basic(X). ∀x:Point(X).  uiff(x ∈ ss-basic-and(u;v);x ∈ u ∧ x ∈ v)
BY
{ (Auto THEN (Unhide THENA Auto) THEN All (RepUR ``ss-mem-basic ss-basic l_all ss-basic-and``)) }

1
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:ℕ||u||. let f,r = u[i] in f(x) < r

2
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

3
1. X : SeparationSpace
2. u : (Point(X ⟶ ℝ) × ℝ) List
3. v : (Point(X ⟶ ℝ) × ℝ) List
4. x : 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 = u @ v[i] in f(x) < r

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}u,v:ss-basic(X).  \mforall{}x:Point(X).    uiff(x  \mmember{}  ss-basic-and(u;v);x  \mmember{}  u  \mwedge{}  x  \mmember{}  v)


By

---

Latex:
(Auto  THEN  (Unhide  THENA  Auto)  THEN  All  (RepUR  ``ss-mem-basic  ss-basic  l\_all  ss-basic-and``))

---

Home Index