---

Step * 1 of Lemma in-compatible-cubes

.....assertion..... 
1. k : ℕ
2. c : ℚCube(k)
3. d : ℚCube(k)
4. Compatible(c;d)
5. p : ℝ^k
6. in-rat-cube(k;p;c)
7. in-rat-cube(k;p;d)
⊢ in-rat-cube(k;p;c ⋂ d)
BY
{ (All (RepUR ``in-rat-cube rat-cube-intersection``)
   THEN ParallelOp -2
   THEN MoveToConcl (-1)
   THEN (D -2 With ⌜i⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜p i⌝;⌜c i⌝;⌜d i⌝]⋅
   THEN All Thin
   THEN D 2
   THEN D -1
   THEN RepUR ``rat-interval-intersection`` 0) }

1
1. v : ℝ
2. v3 : ℚ
3. v4 : ℚ
4. v5 : ℚ
5. v6 : ℚ
⊢ ((rat2real(v5) ≤ v) ∧ (v ≤ rat2real(v6)))
⇒ ((rat2real(v3) ≤ v) ∧ (v ≤ rat2real(v4)))
⇒ ((rat2real(qmax(v3;v5)) ≤ v) ∧ (v ≤ rat2real(qmin(v4;v6))))

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  d  :  \mBbbQ{}Cube(k)
4.  Compatible(c;d)
5.  p  :  \mBbbR{}\^{}k
6.  in-rat-cube(k;p;c)
7.  in-rat-cube(k;p;d)
\mvdash{}  in-rat-cube(k;p;c  \mcap{}  d)


By

---

Latex:
(All  (RepUR  ``in-rat-cube  rat-cube-intersection``)
  THEN  ParallelOp  -2
  THEN  MoveToConcl  (-1)
  THEN  (D  -2  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}p  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{};\mkleeneopen{}d  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  2
  THEN  D  -1
  THEN  RepUR  ``rat-interval-intersection``  0)

---

Home Index