---

Step * of Lemma weak-continuity-principle-interval

No Annotations
∀u,v:ℝ. ∀x:{x:ℝ| x ∈ [u, v]} .
  ∃x':{x':ℝ| x' = x} 
   ∀F:{x:ℝ| x ∈ [u, v]}  ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| (x = y ∈ (ℕ+n ⟶ ℤ)) ∧ (y ∈ [u, v])} .
     ∃z:{x:ℝ| x ∈ [u, v]} . (∃n:ℕ+ [(F x' = F z ∧ (z = (G n)))])
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert x ∈ [u, v] BY
               Auto)
   THEN Reduce -1
   THEN (InstLemma `weak-continuity-principle-real` [⌜interval-retraction(u;v;x)⌝]⋅ THENA Auto)
   THEN (D 0 With ⌜interval-retraction(u;v;interval-retraction(u;v;x))⌝  THENA Auto)) }

1
1. u : ℝ
2. v : ℝ
3. x : {x:ℝ| x ∈ [u, v]} 
4. (u ≤ x) ∧ (x ≤ v)
5. ∀F:ℝ ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| interval-retraction(u;v;x) = y ∈ (ℕ+n ⟶ ℤ)} .
     (∃n:ℕ+ [F interval-retraction(u;v;x) = F (G n)])
⊢ ∀F:{x:ℝ| x ∈ [u, v]}  ⟶ 𝔹. ∀G:n:ℕ+ ⟶ {y:ℝ| (x = y ∈ (ℕ+n ⟶ ℤ)) ∧ (y ∈ [u, v])} .
    ∃z:{x:ℝ| x ∈ [u, v]} . (∃n:ℕ+ [(F interval-retraction(u;v;interval-retraction(u;v;x)) = F z ∧ (z = (G n)))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}u,v:\mBbbR{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .
    \mexists{}x':\{x':\mBbbR{}|  x'  =  x\} 
      \mforall{}F:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbB{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  (x  =  y)  \mwedge{}  (y  \mmember{}  [u,  v])\}  .
          \mexists{}z:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (\mexists{}n:\mBbbN{}\msupplus{}  [(F  x'  =  F  z  \mwedge{}  (z  =  (G  n)))])


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  x  \mmember{}  [u,  v]  BY
                          Auto)
  THEN  Reduce  -1
  THEN  (InstLemma  `weak-continuity-principle-real`  [\mkleeneopen{}interval-retraction(u;v;x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}interval-retraction(u;v;interval-retraction(u;v;x))\mkleeneclose{}    THENA  Auto))

---

Home Index