---

Step * of Lemma rat-cube-third-not-in-face

∀[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].
  ∀f:ℚCube(k). (¬in-rat-cube(k;p;f)) supposing ((¬(f = c ∈ ℚCube(k))) and f ≤ c) supposing rat-cube-third(k;p;c) ∧ (↑Inh\000Cabited(c))
BY
{ (Auto
   THEN ParallelLast
   THEN (FLemma `in-rat-cube-face` [-1;-2] THENA Auto)
   THEN (D 4 THENA Auto)
   THEN Unfold `rational-cube` 0
   THEN (FunExt THENW Auto)
   THEN RepeatFor 4 (((D -2 With ⌜x⌝  THENA Auto) THEN MoveToConcl (-1)))
   THEN GenConclTerms Auto [⌜f x⌝;⌜c x⌝;⌜p x⌝]⋅
   THEN All Thin
   THEN (D 0 THENA Auto)
   THEN D 2
   THEN D 1
   THEN RepUR ``rat-interval-face rat-point-interval`` (-1)
   THEN SplitOrHyps
   THEN (EqHD  (-1) THENA Auto)
   THEN All Reduce
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN Auto
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
2:n
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℝ
6. v5 = v3 ∈ ℚ
7. v6 = v3 ∈ ℚ
8. rat2real(v3) ≤ v2
9. v2 ≤ rat2real(v3)
10. rat2real(v3) ≤ v2
11. v2 ≤ rat2real(v4)
12. rat-interval-third(v2;<v3, v4>)
⊢ v3 = v4 ∈ ℚ

2
.....subterm..... T:t
1:n
1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℝ
6. v5 = v4 ∈ ℚ
7. v6 = v4 ∈ ℚ
8. rat2real(v4) ≤ v2
9. v2 ≤ rat2real(v4)
10. rat2real(v3) ≤ v2
11. v2 ≤ rat2real(v4)
12. rat-interval-third(v2;<v3, v4>)
⊢ v4 = v3 ∈ ℚ

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  (FLemma  `in-rat-cube-face`  [-1;-2]  THENA  Auto)
  THEN  (D  4  THENA  Auto)
  THEN  Unfold  `rational-cube`  0
  THEN  (FunExt  THENW  Auto)
  THEN  RepeatFor  4  (((D  -2  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1)))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}f  x\mkleeneclose{};\mkleeneopen{}c  x\mkleeneclose{};\mkleeneopen{}p  x\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  (D  0  THENA  Auto)
  THEN  D  2
  THEN  D  1
  THEN  RepUR  ``rat-interval-face  rat-point-interval``  (-1)
  THEN  SplitOrHyps
  THEN  (EqHD    (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index