---

Step * 1 of Lemma intersecting-0-dim-cubes


1. k : ℕ
2. b : ℚCube(k)
3. q : ℝ^k
4. c : ℚCube(k)
5. req-vec(k;q;λj.rat2real(fst((c j))))
6. req-vec(k;q;λj.rat2real(fst((b j))))
7. ∀i:ℕk. ((fst((c i))) = (snd((c i))) ∈ ℚ)
8. ∀i:ℕk. ((fst((b i))) = (snd((b i))) ∈ ℚ)
9. ∀i:ℕk. ((fst((c i))) = (fst((b i))) ∈ ℚ)
10. x : ℕk
⊢ (c x) = (b x) ∈ ℚInterval
BY
{ (∀h:hyp. ((InstHyp [⌜x⌝] h⋅ THENA Auto) THEN MoveToConcl (-1)) 
   THEN GenConclTerms Auto [⌜c x⌝;⌜b x⌝]⋅
   THEN All Thin
   THEN D -2
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  b  :  \mBbbQ{}Cube(k)
3.  q  :  \mBbbR{}\^{}k
4.  c  :  \mBbbQ{}Cube(k)
5.  req-vec(k;q;\mlambda{}j.rat2real(fst((c  j))))
6.  req-vec(k;q;\mlambda{}j.rat2real(fst((b  j))))
7.  \mforall{}i:\mBbbN{}k.  ((fst((c  i)))  =  (snd((c  i))))
8.  \mforall{}i:\mBbbN{}k.  ((fst((b  i)))  =  (snd((b  i))))
9.  \mforall{}i:\mBbbN{}k.  ((fst((c  i)))  =  (fst((b  i))))
10.  x  :  \mBbbN{}k
\mvdash{}  (c  x)  =  (b  x)


By

---

Latex:
(\mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1)) 
  THEN  GenConclTerms  Auto  [\mkleeneopen{}c  x\mkleeneclose{};\mkleeneopen{}b  x\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -2
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index