---

Step * of Lemma simple-partition-exists

∀a,b:ℝ.
  ((a ≤ b)
  ⇒ (∀e:ℝ
        ((r0 < e)
        ⇒ (∃M:ℕ+
             ∃g:ℕM + 1 ⟶ {x:ℝ| x ∈ [a, b]} 
              (((g 0) = a ∈ ℝ) ∧ ((g M) = b ∈ ℝ) ∧ (∀i:ℕM. (((g i) ≤ (g (i + 1))) ∧ (((g (i + 1)) - g i) ≤ e))))))))
BY
{ (Auto
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN (InstLemma `partition-exists` [⌜[a, b]⌝;⌜e⌝]⋅ THENA Auto)
   THEN D -1
   THEN (InstConcl [⌜||full-partition([a, b];p)|| - 1⌝]⋅ THENA (Auto THEN RepUR ``full-partition`` 0 THEN Auto'))) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. e : ℝ
5. r0 < e
6. icompact([a, b])
7. p : partition([a, b])
8. partition-mesh([a, b];p) ≤ e
⊢ ∃g:ℕ(||full-partition([a, b];p)|| - 1) + 1 ⟶ {x:ℝ| x ∈ [a, b]} 
   (((g 0) = a ∈ ℝ)
   ∧ ((g (||full-partition([a, b];p)|| - 1)) = b ∈ ℝ)
   ∧ (∀i:ℕ||full-partition([a, b];p)|| - 1. (((g i) ≤ (g (i + 1))) ∧ (((g (i + 1)) - g i) ≤ e))))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    ((a  \mleq{}  b)
    {}\mRightarrow{}  (\mforall{}e:\mBbbR{}
                ((r0  <  e)
                {}\mRightarrow{}  (\mexists{}M:\mBbbN{}\msupplus{}
                          \mexists{}g:\mBbbN{}M  +  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  [a,  b]\} 
                            (((g  0)  =  a)
                            \mwedge{}  ((g  M)  =  b)
                            \mwedge{}  (\mforall{}i:\mBbbN{}M.  (((g  i)  \mleq{}  (g  (i  +  1)))  \mwedge{}  (((g  (i  +  1))  -  g  i)  \mleq{}  e))))))))


By

---

Latex:
(Auto
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  (InstLemma  `partition-exists`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (InstConcl  [\mkleeneopen{}||full-partition([a,  b];p)||  -  1\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``full-partition``  0  THEN  Auto')
              ))

---

Home Index