---

Step * 1 1 of Lemma closed-interval-connected


1. u : ℝ
2. v : ℝ
3. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
4. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
7. a : {x:ℝ| x ∈ [u, v]} 
8. A[a]
9. b : {x:ℝ| x ∈ [u, v]} 
10. B[b]
11. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
12. u ≤ v
13. (∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((A interval-retraction(u;v;y)) ⇒ (A interval-retraction(u;v;x))))
⇒ (∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((B interval-retraction(u;v;y)) ⇒ (B interval-retraction(u;v;x))))
⇒ (∃a:ℝ. (A interval-retraction(u;v;a)))
⇒ (∃b:ℝ. (B interval-retraction(u;v;b)))
⇒ (∀r:ℝ. ((A interval-retraction(u;v;r)) ∨ (B interval-retraction(u;v;r))))
⇒ (∃r:ℝ. ((A interval-retraction(u;v;r)) ∧ (B interval-retraction(u;v;r))))
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])
BY
{ ((D -1
    THENA (Auto
           THEN InstHyp [⌜interval-retraction(u;v;x)⌝;⌜interval-retraction(u;v;y)⌝] 5⋅
           THEN Try (Complete (Auto))
           THEN MemTypeCD
           THEN Auto
           THEN BLemma `interval-retraction_functionality`
           THEN Auto)
    )
   THEN (D -1
         THENA (Auto
                THEN InstHyp [⌜interval-retraction(u;v;x)⌝;⌜interval-retraction(u;v;y)⌝] 6⋅
                THEN Try (Complete (Auto))
                THEN MemTypeCD
                THEN Auto
                THEN BLemma `interval-retraction_functionality`
                THEN Auto)
         )
   ) }

1
1. u : ℝ
2. v : ℝ
3. [A] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
4. [B] : {x:ℝ| x ∈ [u, v]}  ⟶ ℙ
5. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (A[y] ⇒ A[x])
6. ∀x:{x:ℝ| x ∈ [u, v]} . ∀y:{y:{x:ℝ| x ∈ [u, v]} | x = y} .  (B[y] ⇒ B[x])
7. a : {x:ℝ| x ∈ [u, v]} 
8. A[a]
9. b : {x:ℝ| x ∈ [u, v]} 
10. B[b]
11. ∀r:{x:ℝ| x ∈ [u, v]} . (A[r] ∨ B[r])
12. u ≤ v
13. (∃a:ℝ. (A interval-retraction(u;v;a)))
⇒ (∃b:ℝ. (B interval-retraction(u;v;b)))
⇒ (∀r:ℝ. ((A interval-retraction(u;v;r)) ∨ (B interval-retraction(u;v;r))))
⇒ (∃r:ℝ. ((A interval-retraction(u;v;r)) ∧ (B interval-retraction(u;v;r))))
⊢ ∃r:{x:ℝ| x ∈ [u, v]} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
4.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}    {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
6.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
7.  a  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
8.  A[a]
9.  b  :  \{x:\mBbbR{}|  x  \mmember{}  [u,  v]\} 
10.  B[b]
11.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mvee{}  B[r])
12.  u  \mleq{}  v
13.  (\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    ((A  interval-retraction(u;v;y))  {}\mRightarrow{}  (A  interval-retraction(u;v;x))))
{}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    ((B  interval-retraction(u;v;y))  {}\mRightarrow{}  (B  interval-retraction(u;v;x))))
{}\mRightarrow{}  (\mexists{}a:\mBbbR{}.  (A  interval-retraction(u;v;a)))
{}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  (B  interval-retraction(u;v;b)))
{}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  ((A  interval-retraction(u;v;r))  \mvee{}  (B  interval-retraction(u;v;r))))
{}\mRightarrow{}  (\mexists{}r:\mBbbR{}.  ((A  interval-retraction(u;v;r))  \mwedge{}  (B  interval-retraction(u;v;r))))
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  [u,  v]\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((D  -1
    THENA  (Auto
                  THEN  InstHyp  [\mkleeneopen{}interval-retraction(u;v;x)\mkleeneclose{};\mkleeneopen{}interval-retraction(u;v;y)\mkleeneclose{}]  5\mcdot{}
                  THEN  Try  (Complete  (Auto))
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  BLemma  `interval-retraction\_functionality`
                  THEN  Auto)
    )
  THEN  (D  -1
              THENA  (Auto
                            THEN  InstHyp  [\mkleeneopen{}interval-retraction(u;v;x)\mkleeneclose{};\mkleeneopen{}interval-retraction(u;v;y)\mkleeneclose{}]  6\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  BLemma  `interval-retraction\_functionality`
                            THEN  Auto)
              )
  )

---

Home Index