---

Step * 2 2 1 of Lemma half-cube-dimension


1. k : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
4. h : ℚCube(k)
5. ∀i:ℕk. (↑is-half-interval(h i;c i))
6. ∀i:ℕk. (dim(h i) = dim(c i) ∈ ℤ)
⊢ ∀i:ℕk. (↑Inhabited(h i))
BY
{ (ParallelOp 3
   THEN (Assert ↑is-half-interval(h i;c i) BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜h i⌝;⌜c i⌝]⋅
   THEN D -4
   THEN D -2
   THEN RepUR ``inhabited-rat-interval is-half-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN All Thin
   THEN Auto
   THEN RepeatFor 2 (D -1)
   THEN (RWO  "-1 -2" 0 THENA Auto)
   THEN Unfold `qavg` 0
   THEN QMul ⌜2⌝ 0⋅) }

1
1. v2 : ℚ
2. v3 : ℚ
3. v4 : ℚ
4. v5 : ℚ
5. v4 ≤ v5
6. v2 = v4 ∈ ℚ
7. v3 = qavg(v4;v5) ∈ ℚ
⊢ (2 * v4) ≤ (v4 + v5)

2
1. v2 : ℚ
2. v3 : ℚ
3. v4 : ℚ
4. v5 : ℚ
5. v4 ≤ v5
6. v2 = qavg(v4;v5) ∈ ℚ
7. v3 = v5 ∈ ℚ
⊢ (v4 + v5) ≤ (2 * v5)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \mforall{}i:\mBbbN{}k.  (\muparrow{}Inhabited(c  i))
4.  h  :  \mBbbQ{}Cube(k)
5.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(h  i;c  i))
6.  \mforall{}i:\mBbbN{}k.  (dim(h  i)  =  dim(c  i))
\mvdash{}  \mforall{}i:\mBbbN{}k.  (\muparrow{}Inhabited(h  i))


By

---

Latex:
(ParallelOp  3
  THEN  (Assert  \muparrow{}is-half-interval(h  i;c  i)  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}h  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  D  -4
  THEN  D  -2
  THEN  RepUR  ``inhabited-rat-interval  is-half-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO    "-1  -2"  0  THENA  Auto)
  THEN  Unfold  `qavg`  0
  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  0\mcdot{})

---

Home Index