---

Step * of Lemma in-rat-half-cube

∀k:ℕ. ∀c,h:ℚCube(k).  ((↑is-half-cube(k;h;c)) ⇒ (∀x:ℝ^k. (in-rat-cube(k;x;h) ⇒ in-rat-cube(k;x;c))))
BY
{ (Auto
   THEN (RWO  "assert-is-half-cube" (-3) THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 4 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜x i⌝;⌜h i⌝;⌜c i⌝]⋅
   THEN All Thin
   THEN D -2
   THEN D -1
   THEN RepUR ``is-half-interval`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN D 8
   THEN Auto
   THEN RationalElim ⌜v3⌝⋅
   THEN RationalElim ⌜v4⌝⋅) }

1
1. v6 : ℚ
2. v5 : ℚ
3. v : ℝ
4. rat2real(qavg(v5;v6)) ≤ v
5. v ≤ rat2real(v6)
⊢ rat2real(v5) ≤ v

2
1. v5 : ℚ
2. v6 : ℚ
3. v : ℝ
4. rat2real(v5) ≤ v
5. v ≤ rat2real(qavg(v5;v6))
6. rat2real(v5) ≤ v
⊢ v ≤ rat2real(v6)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,h:\mBbbQ{}Cube(k).
    ((\muparrow{}is-half-cube(k;h;c))  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}\^{}k.  (in-rat-cube(k;x;h)  {}\mRightarrow{}  in-rat-cube(k;x;c))))


By

---

Latex:
(Auto
  THEN  (RWO    "assert-is-half-cube"  (-3)  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}x  i\mkleeneclose{};\mkleeneopen{}h  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -2
  THEN  D  -1
  THEN  RepUR  ``is-half-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  D  8
  THEN  Auto
  THEN  RationalElim  \mkleeneopen{}v3\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v4\mkleeneclose{}\mcdot{})

---

Home Index