---

Step * of Lemma in-rat-cube-intersection

∀k:ℕ. ∀c,d:ℚCube(k). ∀x:ℝ^k.  (in-rat-cube(k;x;c ⋂ d) ⇐⇒ in-rat-cube(k;x;c) ∧ in-rat-cube(k;x;d))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN ((Progress(RepUR ``rat-cube-intersection`` -1) THEN MoveToConcl (-1))
   ORELSE ((D 5 With ⌜i⌝  THENA Auto) THEN RepUR ``rat-cube-intersection`` 0 THEN RepeatFor 2 (MoveToConcl (-1)))
   )
   THEN GenConclTerms Auto [⌜c i⌝;⌜d i⌝;⌜x i⌝]⋅
   THEN All Thin
   THEN (D 2 THEN D 1)
   THEN RepUR ``rat-interval-intersection`` 0
   THEN Auto
   THEN Try (Complete (((RWO "-2< -2" 0 THENA Auto)
                        THEN BLemma `rleq-rat2real`
                        THEN Auto
                        THEN RWO "qmax_ub qmin_lb" 0
                        THEN Auto)))) }

1
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℝ
6. rat2real(v3) ≤ v2
7. v2 ≤ rat2real(v4)
8. rat2real(v5) ≤ v2
9. v2 ≤ rat2real(v6)
⊢ rat2real(qmax(v5;v3)) ≤ v2

2
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℝ
6. rat2real(v3) ≤ v2
7. v2 ≤ rat2real(v4)
8. rat2real(v5) ≤ v2
9. v2 ≤ rat2real(v6)
10. rat2real(qmax(v5;v3)) ≤ v2
⊢ v2 ≤ rat2real(qmin(v6;v4))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,d:\mBbbQ{}Cube(k).  \mforall{}x:\mBbbR{}\^{}k.    (in-rat-cube(k;x;c  \mcap{}  d)  \mLeftarrow{}{}\mRightarrow{}  in-rat-cube(k;x;c)  \mwedge{}  in-rat-cube(k;x;d))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  ((Progress(RepUR  ``rat-cube-intersection``  -1)  THEN  MoveToConcl  (-1))
  ORELSE  ((D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
                  THEN  RepUR  ``rat-cube-intersection``  0
                  THEN  RepeatFor  2  (MoveToConcl  (-1)))
  )
  THEN  GenConclTerms  Auto  [\mkleeneopen{}c  i\mkleeneclose{};\mkleeneopen{}d  i\mkleeneclose{};\mkleeneopen{}x  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  (D  2  THEN  D  1)
  THEN  RepUR  ``rat-interval-intersection``  0
  THEN  Auto
  THEN  Try  (Complete  (((RWO  "-2<  -2"  0  THENA  Auto)
                                            THEN  BLemma  `rleq-rat2real`
                                            THEN  Auto
                                            THEN  RWO  "qmax\_ub  qmin\_lb"  0
                                            THEN  Auto))))

---

Home Index