---

Step * of Lemma closures-meet-sq

∀[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
{ ((Auto THEN ExRepD)
   THEN D 3
   THEN D 4
   THEN D 6
   THEN RenameVar `a0' 3
   THEN RenameVar `b0' 4
   THEN Assert ⌜∃s:ℕ ⟶ (a:{a:ℝ| P a}  × {b:ℝ| (Q b) ∧ (a ≤ b)} ) [(∀n:ℕ
                                                                 (((fst(s[n])) ≤ (fst(s[n + 1])))
                                                                 ∧ ((snd(s[n + 1])) ≤ (snd(s[n])))
                                                                 ∧ (((snd(s[n + 1])) - fst(s[n + 1])) ≤ (((snd(s[n])) 
                                                                   - fst(s[n]))
                                                                   * c))))]⌝⋅) }

1
.....assertion..... 
1. [P] : ℝ ⟶ ℙ
2. [Q] : ℝ ⟶ ℙ
3. a0 : {a:ℝ| P a} 
4. b0 : ℝ
5. [%4] : (Q b0) ∧ (a0 ≤ b0)
6. c : ℝ
7. [%5] : (r0 ≤ c) ∧ (c < r1)
8. ∀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)))])
⊢ ∃s:ℕ ⟶ (a:{a:ℝ| P a}  × {b:ℝ| (Q b) ∧ (a ≤ b)} ) [(∀n:ℕ
                                                   (((fst(s[n])) ≤ (fst(s[n + 1])))
                                                   ∧ ((snd(s[n + 1])) ≤ (snd(s[n])))
                                                   ∧ (((snd(s[n + 1])) - fst(s[n + 1])) ≤ (((snd(s[n])) - fst(s[n]))
                                                     * c))))]

2
1. [P] : ℝ ⟶ ℙ
2. [Q] : ℝ ⟶ ℙ
3. a0 : {a:ℝ| P a} 
4. b0 : ℝ
5. [%4] : (Q b0) ∧ (a0 ≤ b0)
6. c : ℝ
7. [%5] : (r0 ≤ c) ∧ (c < r1)
8. ∀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)))])
9. ∃s:ℕ ⟶ (a:{a:ℝ| P a}  × {b:ℝ| (Q b) ∧ (a ≤ b)} ) [(∀n:ℕ
                                                    (((fst(s[n])) ≤ (fst(s[n + 1])))
                                                    ∧ ((snd(s[n + 1])) ≤ (snd(s[n])))
                                                    ∧ (((snd(s[n + 1])) - fst(s[n + 1])) ≤ (((snd(s[n])) - fst(s[n]))
                                                      * c))))]
⊢ ∃y:ℝ. (y ∈ closure(λz.(↓P z)) ∧ y ∈ closure(λz.(↓Q z)))

---

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:
((Auto  THEN  ExRepD)
  THEN  D  3
  THEN  D  4
  THEN  D  6
  THEN  RenameVar  `a0'  3
  THEN  RenameVar  `b0'  4
  THEN  Assert  \mkleeneopen{}\mexists{}s:\mBbbN{}  {}\mrightarrow{}  (a:\{a:\mBbbR{}|  P  a\}    \mtimes{}  \{b:\mBbbR{}|  (Q  b)  \mwedge{}  (a  \mleq{}  b)\}  )  [(\mforall{}n:\mBbbN{}
                                                                                                                              (((fst(s[n]))  \mleq{}  (fst(s[n  +  1])))
                                                                                                                              \mwedge{}  ((snd(s[n  +  1]))  \mleq{}  (snd(s[n])))
                                                                                                                              \mwedge{}  (((snd(s[n  +  1]))  -  fst(s[n
                                                                                                                                  +  1]))  \mleq{}  (((snd(s[n]))  -  fst(s[n]))
                                                                                                                                  *  c))))]\mkleeneclose{}\mcdot{})

---

Home Index