---

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


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)))])
BY
{ ((D 0 THENA Auto)
   THEN (D -2 With ⌜λr.(F interval-retraction(u;v;r))⌝  THENA Auto)
   THEN Reduce -1
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜λn.interval-retraction(u;v;G n)⌝  THENA Auto)
   THEN Reduce -1) }

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

2
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)))])

---

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.  \mforall{}F:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  interval-retraction(u;v;x)  =  y\}  .
          (\mexists{}n:\mBbbN{}\msupplus{}  [F  interval-retraction(u;v;x)  =  F  (G  n)])
\mvdash{}  \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  interval-retraction(u;v;interval-retraction(u;v;x))  =  F  z  \mwedge{}  (z  =  (G  n)))])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}r.(F  interval-retraction(u;v;r))\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}n.interval-retraction(u;v;G  n)\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1)

---

Home Index