---

Step * of Lemma sq_stable__ss-mem-basic

No Annotations
∀[X:SeparationSpace]. ∀B:ss-basic(X). ∀x:Point(X).  SqStable(x ∈ B)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (Unfold `ss-mem-basic` 0 THEN Auto)
   THEN UseWitness ⌜λi.let f,r = B[i] 
                       in rlessw(f x;r)⌝⋅
   THEN Unfold `l_all` 0
   THEN Unfold `ss-basic` 2
   THEN Auto) }

1
1. X : SeparationSpace
2. B : (Point(X ⟶ ℝ) × ℝ) List@i
3. x : Point(X)@i
4. x ∈ B
5. i : ℕ||B||@i
6. f : Point(X ⟶ ℝ)
7. r : ℝ
8. B[i] = <f, r> ∈ (Point(X ⟶ ℝ) × ℝ)
⊢ f ∈ Point(X) ⟶ Point(ℝ)

2
1. X : SeparationSpace
2. B : (Point(X ⟶ ℝ) × ℝ) List@i
3. x : Point(X)@i
4. x ∈ B
5. i : ℕ||B||@i
6. f : Point(X ⟶ ℝ)
7. r : ℝ
8. B[i] = <f, r> ∈ (Point(X ⟶ ℝ) × ℝ)
⊢ r ∈ {y:ℝ| (f x) < y} 

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:SeparationSpace].  \mforall{}B:ss-basic(X).  \mforall{}x:Point(X).    SqStable(x  \mmember{}  B)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (Unfold  `ss-mem-basic`  0  THEN  Auto)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}i.let  f,r  =  B[i] 
                                          in  rlessw(f  x;r)\mkleeneclose{}\mcdot{}
  THEN  Unfold  `l\_all`  0
  THEN  Unfold  `ss-basic`  2
  THEN  Auto)

---

Home Index