---

Step * of Lemma same-half-cube-of-compatible

∀k:ℕ. ∀a,b,c:ℚCube(k).
  ((↑Inhabited(c)) ⇒ (↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;c;b)) ⇒ Compatible(a;b) ⇒ (a = b ∈ ℚCube(k)))
BY
{ (Auto
   THEN (D -1 THENA (InstLemma `inhabited-intersection-half-cubes` [⌜k⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜c⌝]⋅ THEN Auto))
   THEN D -1
   THEN (All (RWO "assert-is-half-cube assert-inhabited-rat-cube") THENA Auto)
   THEN All (RepUR ``rat-cube-face rat-cube-intersection``)
   THEN Unfold `rational-cube` 0
   THEN (FunExt THENA Auto)
   THEN RenameVar `i' (-1)
   THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Auto) THEN Thin h THEN MoveToConcl (-1)) ) }

1
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. i : ℕk
⊢ (↑Inhabited(c i))
⇒ (↑is-half-interval(c i;a i))
⇒ (↑is-half-interval(c i;b i))
⇒ a i ⋂ b i ≤ a i
⇒ a i ⋂ b i ≤ b i
⇒ ((a i) = (b i) ∈ ℚInterval)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}a,b,c:\mBbbQ{}Cube(k).
    ((\muparrow{}Inhabited(c))
    {}\mRightarrow{}  (\muparrow{}is-half-cube(k;c;a))
    {}\mRightarrow{}  (\muparrow{}is-half-cube(k;c;b))
    {}\mRightarrow{}  Compatible(a;b)
    {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(Auto
  THEN  (D  -1  THENA  (InstLemma  `inhabited-intersection-half-cubes`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  (All  (RWO  "assert-is-half-cube  assert-inhabited-rat-cube")  THENA  Auto)
  THEN  All  (RepUR  ``rat-cube-face  rat-cube-intersection``)
  THEN  Unfold  `rational-cube`  0
  THEN  (FunExt  THENA  Auto)
  THEN  RenameVar  `i'  (-1)
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  Thin  h  THEN  MoveToConcl  (-1))  )

---

Home Index