---

Step * of Lemma has-interior-point-implies

No Annotations
∀[k:ℕ]. ∀[c,a:ℚCube(k)].
  (has-interior-point(k;c;a) ⇒ dim(c) < dim(a) ⇒ (∀d:ℚCube(k). ((↑is-half-cube(k;c;d)) ⇒ (¬d ≤ a))))
BY
{ (Auto THEN (D 4 THENM D 0) THEN Auto THEN (FLemma `rat-point-in-half-cube` [5;-2] THENA Auto)) }

1
1. k : ℕ
2. c : ℚCube(k)
3. a : ℚCube(k)
4. x : ℕk ⟶ ℚ
5. rat-point-in-cube(k;x;c)
6. rat-point-in-cube-interior(k;x;a)
7. dim(c) < dim(a)
8. d : ℚCube(k)
9. ↑is-half-cube(k;c;d)
10. d ≤ a
11. rat-point-in-cube(k;x;d)
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[c,a:\mBbbQ{}Cube(k)].
    (has-interior-point(k;c;a)
    {}\mRightarrow{}  dim(c)  <  dim(a)
    {}\mRightarrow{}  (\mforall{}d:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;c;d))  {}\mRightarrow{}  (\mneg{}d  \mleq{}  a))))


By

---

Latex:
(Auto  THEN  (D  4  THENM  D  0)  THEN  Auto  THEN  (FLemma  `rat-point-in-half-cube`  [5;-2]  THENA  Auto))

---

Home Index