---

Step * 1 of Lemma rat-point-in-intersection


1. k : ℕ
2. x : ℕk ⟶ ℚ
3. c : ℚCube(k)
4. d : ℚCube(k)
5. ∀i:ℕk. (((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i)))))
6. i : ℕk
7. ((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i))))
⊢ ((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i))))
BY
{ (RepUR ``rat-cube-intersection`` -1
   THEN 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 (RWO "qmax_lb qmin_ub" 0 THENA Auto)
   THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  x  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
3.  c  :  \mBbbQ{}Cube(k)
4.  d  :  \mBbbQ{}Cube(k)
5.  \mforall{}i:\mBbbN{}k.  (((fst((c  \mcap{}  d  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((c  \mcap{}  d  i)))))
6.  i  :  \mBbbN{}k
7.  ((fst((c  \mcap{}  d  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((c  \mcap{}  d  i))))
\mvdash{}  ((fst((c  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((c  i))))


By

---

Latex:
(RepUR  ``rat-cube-intersection``  -1
  THEN  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  (RWO  "qmax\_lb  qmin\_ub"  0  THENA  Auto)
  THEN  Auto)

---

Home Index