---

Step * of Lemma in-rat-cube-face

∀[k:ℕ]. ∀[p:ℝ^k]. ∀[c,f:ℚCube(k)].  (in-rat-cube(k;p;c)) supposing (in-rat-cube(k;p;f) and (↑Inhabited(c)) and f ≤ c)
BY
{ (Auto
   THEN (RWO "assert-inhabited-rat-cube" (-2) THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (D -4 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (D -3 With ⌜i⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜p i⌝;⌜f i⌝;⌜c i⌝]⋅
   THEN All Thin
   THEN D -2
   THEN D -1
   THEN RepUR ``rat-interval-face rat-point-interval`` 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN SplitOrHyps
   THEN (EqHD (-2) THENA Auto)
   THEN All Reduce
   THEN RationalElim ⌜v3⌝⋅
   THEN RationalElim ⌜v4⌝⋅
   THEN RepUR ``inhabited-rat-interval`` 0
   THEN RW assert_pushdownC 0
   THEN Auto) }

1
1. v5 : ℚ
2. v : ℝ
3. v6 : ℚ
4. rat2real(v5) ≤ v
5. v ≤ rat2real(v5)
6. v5 ≤ v6
7. rat2real(v5) ≤ v
⊢ v ≤ rat2real(v6)

2
1. v6 : ℚ
2. v : ℝ
3. v5 : ℚ
4. rat2real(v6) ≤ v
5. v ≤ rat2real(v6)
6. v5 ≤ v6
⊢ rat2real(v5) ≤ v

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[c,f:\mBbbQ{}Cube(k)].
    (in-rat-cube(k;p;c))  supposing  (in-rat-cube(k;p;f)  and  (\muparrow{}Inhabited(c))  and  f  \mleq{}  c)


By

---

Latex:
(Auto
  THEN  (RWO  "assert-inhabited-rat-cube"  (-2)  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  -4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}p  i\mkleeneclose{};\mkleeneopen{}f  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  D  -2
  THEN  D  -1
  THEN  RepUR  ``rat-interval-face  rat-point-interval``  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  SplitOrHyps
  THEN  (EqHD  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  RationalElim  \mkleeneopen{}v3\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v4\mkleeneclose{}\mcdot{}
  THEN  RepUR  ``inhabited-rat-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index