---

Step * of Lemma compatible-half-cubes

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

1
.....assertion..... 
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. (↑Inhabited(a ⋂ b)) ⇒ (a ⋂ b ≤ a ∧ a ⋂ b ≤ b)
9. ∀i:ℕk. (↑Inhabited(c i ⋂ d i))
⊢ ↑Inhabited(a ⋂ b)

2
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. (↑Inhabited(a ⋂ b)) ⇒ (a ⋂ b ≤ a ∧ a ⋂ b ≤ b)
9. ∀i:ℕk. (↑Inhabited(c i ⋂ d i))
10. ↑Inhabited(a ⋂ b)
⊢ c ⋂ d ≤ c ∧ c ⋂ d ≤ d

---

Latex:

---

Latex:
No  Annotations
\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{}  Compatible(a;b)  {}\mRightarrow{}  Compatible(c;d))


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  (RWO  "assert-is-half-cube"  0  THENA  Auto)
  THEN  Auto
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "assert-inhabited-rat-cube"  (-1)  THENA  Auto)
  THEN  RepUR  ``rat-cube-intersection``  -1
  THEN  Assert  \mkleeneopen{}\muparrow{}Inhabited(a  \mcap{}  b)\mkleeneclose{}\mcdot{})

---

Home Index