---

Step * 1 2 of Lemma weak-continuity-principle-interval


1. u : ℝ
2. v : ℝ
3. x : {x:ℝ| x ∈ [u, v]} 
4. (u ≤ x) ∧ (x ≤ v)
5. F : {x:ℝ| x ∈ [u, v]}  ⟶ 𝔹
6. G : n:ℕ+ ⟶ {y:ℝ| (x = y ∈ (ℕ+n ⟶ ℤ)) ∧ (y ∈ [u, v])} 
7. ∃n:ℕ+ [F interval-retraction(u;v;interval-retraction(u;v;x)) 
         = F interval-retraction(u;v;interval-retraction(u;v;G n))]
⊢ ∃z:{x:ℝ| x ∈ [u, v]} . (∃n:ℕ+ [(F interval-retraction(u;v;interval-retraction(u;v;x)) = F z ∧ (z = (G n)))])
BY
{ (ExRepD
   THEN D 0 With ⌜interval-retraction(u;v;interval-retraction(u;v;G n))⌝ 
   THEN Auto
   THEN UseWitness ⌜n⌝⋅
   THEN DSetVars
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  x  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
4.  (u  \mleq{}  x)  \mwedge{}  (x  \mleq{}  v)
5.  F  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbB{}
6.  G  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  (x  =  y)  \mwedge{}  (y  \mmember{}  [u,  v])\} 
7.  \mexists{}n:\mBbbN{}\msupplus{}  [F  interval-retraction(u;v;interval-retraction(u;v;x)) 
                  =  F  interval-retraction(u;v;interval-retraction(u;v;G  n))]
\mvdash{}  \mexists{}z:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
      (\mexists{}n:\mBbbN{}\msupplus{}  [(F  interval-retraction(u;v;interval-retraction(u;v;x))  =  F  z  \mwedge{}  (z  =  (G  n)))])


By

---

Latex:
(ExRepD
  THEN  D  0  With  \mkleeneopen{}interval-retraction(u;v;interval-retraction(u;v;G  n))\mkleeneclose{} 
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  DSetVars
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index