---

Step * of Lemma m-sup-property

∀[X:Type]
  ∀d:metric(X). ∀mtb:m-TB(X;d). ∀f:X ⟶ ℝ. ∀mc:UC(f:X ⟶ ℝ).
    ((∀x:X. ((f x) ≤ m-sup{i:l}(d;mtb;f;mc))) ∧ (∀e:ℝ. ((r0 < e) ⇒ (∃x:X. ((m-sup{i:l}(d;mtb;f;mc) - e) < (f x))))))
BY
{ (InstLemma `m-sup-property1` []
   THEN RepeatFor 5 (ParallelLast')
   THEN RepUR ``sup rset-member upper-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))) ∧ ((m-sup{i:l}(d;mtb;f;mc) - e) < x))))
7. ∀x:ℝ. ((∃x@0:X. (x = (f x@0))) ⇒ (x ≤ m-sup{i:l}(d;mtb;f;mc)))
⊢ ∀x:X. ((f x) ≤ m-sup{i:l}(d;mtb;f;mc))

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))) ⇒ (x ≤ m-sup{i:l}(d;mtb;f;mc)))
7. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((∃x@0:X. (x = (f x@0))) ∧ ((m-sup{i:l}(d;mtb;f;mc) - e) < x))))
8. e : ℝ
9. r0 < e
10. ∃x:ℝ. ((∃x@0:X. (x = (f x@0))) ∧ ((m-sup{i:l}(d;mtb;f;mc) - e) < x))
⊢ ∃x:X. ((m-sup{i:l}(d;mtb;f;mc) - e) < (f x))

---

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.  ((f  x)  \mleq{}  m-sup\{i:l\}(d;mtb;f;mc)))
        \mwedge{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:X.  ((m-sup\{i:l\}(d;mtb;f;mc)  -  e)  <  (f  x))))))


By

---

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

---

Home Index