---

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


1. k : ℕ
2. x : ℕk ⟶ ℚ
3. c : ℚCube(k)
4. d : ℚCube(k)
5. rat-point-in-cube(k;x;c)
6. ∀i:ℕk. (((fst((d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((d i)))))
7. i : ℕk
8. ((fst((d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((d i))))
⊢ ((fst((c ⋂ d i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c ⋂ d i))))
BY
{ ((D -4 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 (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.  rat-point-in-cube(k;x;c)
6.  \mforall{}i:\mBbbN{}k.  (((fst((d  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((d  i)))))
7.  i  :  \mBbbN{}k
8.  ((fst((d  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((d  i))))
\mvdash{}  ((fst((c  \mcap{}  d  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  (snd((c  \mcap{}  d  i))))


By

---

Latex:
((D  -4  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  (RWO  "qmax\_lb  qmin\_ub"  0  THENA  Auto)
  THEN  Auto)

---

Home Index