---

Step * of Lemma inhabited-intersection-half-cubes

∀k:ℕ. ∀a,b,c,d:ℚCube(k).
  ((↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;d;b)) ⇒ (↑Inhabited(c ⋂ d)) ⇒ (↑Inhabited(a ⋂ b)))
BY
{ (RepeatFor 5 (Intro)
   THEN (RWO "assert-is-half-cube" 0 THENA Auto)
   THEN Auto
   THEN (RWO "assert-inhabited-rat-cube" (-1) THENA Auto)
   THEN RepUR ``rat-cube-intersection`` -1) }

1
1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. d : ℚCube(k)
6. ∀i:ℕk. (↑is-half-interval(c i;a i))
7. ∀i:ℕk. (↑is-half-interval(d i;b i))
8. ∀i:ℕk. (↑Inhabited(c i ⋂ d i))
⊢ ↑Inhabited(a ⋂ b)

---

Latex:

---

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


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (RWO  "assert-is-half-cube"  0  THENA  Auto)
  THEN  Auto
  THEN  (RWO  "assert-inhabited-rat-cube"  (-1)  THENA  Auto)
  THEN  RepUR  ``rat-cube-intersection``  -1)

---

Home Index