---

Step * 1 of Lemma has-interior-point-implies


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
BY
{ (FLemma `rat-point-in-cube-interior-not-in-face` [6;-2] THEN 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)
12. d = a ∈ ℚCube(k)
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  a  :  \mBbbQ{}Cube(k)
4.  x  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
5.  rat-point-in-cube(k;x;c)
6.  rat-point-in-cube-interior(k;x;a)
7.  dim(c)  <  dim(a)
8.  d  :  \mBbbQ{}Cube(k)
9.  \muparrow{}is-half-cube(k;c;d)
10.  d  \mleq{}  a
11.  rat-point-in-cube(k;x;d)
\mvdash{}  False


By

---

Latex:
(FLemma  `rat-point-in-cube-interior-not-in-face`  [6;-2]  THEN  Auto)

---

Home Index