---

Step * of Lemma face-of-half-cube

∀k:ℕ. ∀a,b,c:ℚCube(k).  (b ≤ c ⇒ (↑is-half-cube(k;a;b)) ⇒ (∃!d:ℚCube(k). ((↑is-half-cube(k;d;c)) ∧ a ≤ d)))
BY
{ (Auto
   THEN (All (RWO "assert-is-half-cube assert-inhabited-rat-cube") THENA Auto)
   THEN All (RepUR ``rat-cube-face``)) }

1
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. ∀i:ℕk. b i ≤ c i
6. ∀i:ℕk. (↑is-half-interval(a i;b i))
⊢ ∃!d:ℚCube(k). ((↑is-half-cube(k;d;c)) ∧ (∀i:ℕk. a i ≤ d i))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}a,b,c:\mBbbQ{}Cube(k).
    (b  \mleq{}  c  {}\mRightarrow{}  (\muparrow{}is-half-cube(k;a;b))  {}\mRightarrow{}  (\mexists{}!d:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;d;c))  \mwedge{}  a  \mleq{}  d)))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "assert-is-half-cube  assert-inhabited-rat-cube")  THENA  Auto)
  THEN  All  (RepUR  ``rat-cube-face``))

---

Home Index