---

Step * 1 2 of Lemma in-some-half-cube


1. k : ℕ
2. x : ℝ^k
3. c : ℚCube(k)
4. ∀i:ℕk. ((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i)))))
5. ∀i:ℕk
     (¬¬(((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(qavg(fst((c i));snd((c i))))))
     ∨ ((rat2real(qavg(fst((c i));snd((c i)))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i)))))))
⊢ ¬¬(∃h:ℚCube(k). ((↑is-half-cube(k;h;c)) ∧ in-rat-cube(k;x;h)))
BY
{ ((Assert ¬¬(∀i:ℕk
                (((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(qavg(fst((c i));snd((c i))))))
                ∨ ((rat2real(qavg(fst((c i));snd((c i)))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i))))))) BY
          ((InstLemma `finite-double-negation-shift2` [⌜False⌝;⌜k⌝]⋅ THENA Auto)
           THEN Fold `not` (-1)
           THEN (D -1 With ⌜λi.(((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(qavg(fst((c i));snd((c i))))))
                               ∨ ((rat2real(qavg(fst((c i));snd((c i)))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i))))))⌝ 
                 THENA Auto
                 )
           THEN Reduce -1
           THEN BHyp -1
           THEN Auto))
   THEN Thin (-2)
   THEN RepeatFor 2 (ParallelLast)) }

1
1. k : ℕ
2. x : ℝ^k
3. c : ℚCube(k)
4. ∀i:ℕk. ((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i)))))
5. ∀i:ℕk
     (((rat2real(fst((c i))) ≤ (x i)) ∧ ((x i) ≤ rat2real(qavg(fst((c i));snd((c i))))))
     ∨ ((rat2real(qavg(fst((c i));snd((c i)))) ≤ (x i)) ∧ ((x i) ≤ rat2real(snd((c i))))))
⊢ ∃h:ℚCube(k). ((↑is-half-cube(k;h;c)) ∧ in-rat-cube(k;x;h))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}k
3.  c  :  \mBbbQ{}Cube(k)
4.  \mforall{}i:\mBbbN{}k.  ((rat2real(fst((c  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  rat2real(snd((c  i)))))
5.  \mforall{}i:\mBbbN{}k
          (\mneg{}\mneg{}(((rat2real(fst((c  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  rat2real(qavg(fst((c  i));snd((c  i))))))
          \mvee{}  ((rat2real(qavg(fst((c  i));snd((c  i))))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  rat2real(snd((c  i)))))))
\mvdash{}  \mneg{}\mneg{}(\mexists{}h:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;h;c))  \mwedge{}  in-rat-cube(k;x;h)))


By

---

Latex:
((Assert  \mneg{}\mneg{}(\mforall{}i:\mBbbN{}k
                            (((rat2real(fst((c  i)))  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  rat2real(qavg(fst((c  i));snd((c  i))))))
                            \mvee{}  ((rat2real(qavg(fst((c  i));snd((c  i))))  \mleq{}  (x  i))
                                \mwedge{}  ((x  i)  \mleq{}  rat2real(snd((c  i)))))))  BY
                ((InstLemma  `finite-double-negation-shift2`  [\mkleeneopen{}False\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  Fold  `not`  (-1)
                  THEN  (D  -1  With  \mkleeneopen{}\mlambda{}i.(((rat2real(fst((c  i)))  \mleq{}  (x  i))
                                                          \mwedge{}  ((x  i)  \mleq{}  rat2real(qavg(fst((c  i));snd((c  i))))))
                                                          \mvee{}  ((rat2real(qavg(fst((c  i));snd((c  i))))  \mleq{}  (x  i))
                                                              \mwedge{}  ((x  i)  \mleq{}  rat2real(snd((c  i))))))\mkleeneclose{} 
                              THENA  Auto
                              )
                  THEN  Reduce  -1
                  THEN  BHyp  -1
                  THEN  Auto))
  THEN  Thin  (-2)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index