---

Step * of Lemma m-inf-property

∀[X:Type]
  ∀d:metric(X). ∀mtb:m-TB(X;d). ∀f:X ⟶ ℝ. ∀mc:UC(f:X ⟶ ℝ).
    ((∀x:X. (m-inf{i:l}(d;mtb;f;mc) ≤ (f x))) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:X. ((f x) < (m-inf{i:l}(d;mtb;f;mc) + e))))))
BY
{ (InstLemma `m-inf-property1` []
   THEN RepeatFor 5 (ParallelLast')
   THEN RepUR ``inf rset-member lower-bound`` -1
   THEN ParallelLast
   THEN Try (RepeatFor 2 (ParallelLast))) }

1
1. [X] : Type
2. d : metric(X)
3. mtb : m-TB(X;d)
4. f : X ⟶ ℝ
5. mc : UC(f:X ⟶ ℝ)
6. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((∃x@0:X. (x = (f x@0))) ∧ (x < (m-inf{i:l}(d;mtb;f;mc) + e)))))
7. ∀x:ℝ. ((∃x@0:X. (x = (f x@0))) ⇒ (m-inf{i:l}(d;mtb;f;mc) ≤ x))
⊢ ∀x:X. (m-inf{i:l}(d;mtb;f;mc) ≤ (f x))

2
1. [X] : Type
2. d : metric(X)
3. mtb : m-TB(X;d)
4. f : X ⟶ ℝ
5. mc : UC(f:X ⟶ ℝ)
6. ∀x:ℝ. ((∃x@0:X. (x = (f x@0))) ⇒ (m-inf{i:l}(d;mtb;f;mc) ≤ x))
7. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((∃x@0:X. (x = (f x@0))) ∧ (x < (m-inf{i:l}(d;mtb;f;mc) + e)))))
8. e : ℝ
9. r0 < e
10. ∃x:ℝ. ((∃x@0:X. (x = (f x@0))) ∧ (x < (m-inf{i:l}(d;mtb;f;mc) + e)))
⊢ ∃x:X. ((f x) < (m-inf{i:l}(d;mtb;f;mc) + e))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}mtb:m-TB(X;d).  \mforall{}f:X  {}\mrightarrow{}  \mBbbR{}.  \mforall{}mc:UC(f:X  {}\mrightarrow{}  \mBbbR{}).
        ((\mforall{}x:X.  (m-inf\{i:l\}(d;mtb;f;mc)  \mleq{}  (f  x)))
        \mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((f  x)  <  (m-inf\{i:l\}(d;mtb;f;mc)  +  e))))))


By

---

Latex:
(InstLemma  `m-inf-property1`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  RepUR  ``inf  rset-member  lower-bound``  -1
  THEN  ParallelLast
  THEN  Try  (RepeatFor  2  (ParallelLast)))

---

Home Index