---

Step * of Lemma closures-meet-sq-ext

∀[P,Q:ℝ ⟶ ℙ].
  ((∃a:{a:ℝ| P a} . (∃b:ℝ [((Q b) ∧ (a ≤ b))]))
  ⇒ (∃c:{c:ℝ| (r0 ≤ c) ∧ (c < r1)} 
       ∀a:{a:ℝ| P a} . ∀b:{b:ℝ| (Q b) ∧ (a ≤ b)} .
         ∃a':{a':ℝ| P a'} . (∃b':{b':ℝ| (Q b') ∧ (a' ≤ b')}  [((a ≤ a') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))]))
  ⇒ (∃y:ℝ. (y ∈ closure(λz.(↓P z)) ∧ y ∈ closure(λz.(↓Q z)))))
BY
{ ... }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\{a:\mBbbR{}|  P  a\}  .  (\mexists{}b:\mBbbR{}  [((Q  b)  \mwedge{}  (a  \mleq{}  b))]))
    {}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  (r0  \mleq{}  c)  \mwedge{}  (c  <  r1)\} 
              \mforall{}a:\{a:\mBbbR{}|  P  a\}  .  \mforall{}b:\{b:\mBbbR{}|  (Q  b)  \mwedge{}  (a  \mleq{}  b)\}  .
                  \mexists{}a':\{a':\mBbbR{}|  P  a'\}  .  (\mexists{}b':\{b':\mBbbR{}|  (Q  b')  \mwedge{}  (a'  \mleq{}  b')\}    [((a  \mleq{}  a')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  ((b'  -  a')  \mleq{}  ((\000Cb  -  a)  *  c)))]))
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}P  z))  \mwedge{}  y  \mmember{}  closure(\mlambda{}z.(\mdownarrow{}Q  z)))))


By

---

Latex:
...

---

Home Index