---

Step * of Lemma in-compatible-cubes

∀k:ℕ. ∀c,d:ℚCube(k).
  (Compatible(c;d)
  ⇒ (∀p:ℝ^k. (in-rat-cube(k;p;c) ⇒ in-rat-cube(k;p;d) ⇒ (∃f:ℚCube(k). (f ≤ c ∧ f ≤ d ∧ in-rat-cube(k;p;f))))))
BY
{ (Auto THEN (Assert ⌜in-rat-cube(k;p;c ⋂ d)⌝⋅ THENM ((D 4 THENA BLemma `inhabited-iff-in-rat-cube`) THEN Auto))) }

1
.....assertion..... 
1. k : ℕ
2. c : ℚCube(k)
3. d : ℚCube(k)
4. Compatible(c;d)
5. p : ℝ^k
6. in-rat-cube(k;p;c)
7. in-rat-cube(k;p;d)
⊢ in-rat-cube(k;p;c ⋂ d)

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c,d:\mBbbQ{}Cube(k).
    (Compatible(c;d)
    {}\mRightarrow{}  (\mforall{}p:\mBbbR{}\^{}k
                (in-rat-cube(k;p;c)
                {}\mRightarrow{}  in-rat-cube(k;p;d)
                {}\mRightarrow{}  (\mexists{}f:\mBbbQ{}Cube(k).  (f  \mleq{}  c  \mwedge{}  f  \mleq{}  d  \mwedge{}  in-rat-cube(k;p;f))))))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}in-rat-cube(k;p;c  \mcap{}  d)\mkleeneclose{}\mcdot{}
            THENM  ((D  4  THENA  BLemma  `inhabited-iff-in-rat-cube`)  THEN  Auto)
            )
  )

---

Home Index