---

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

.....wf..... 
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)
⊢ d ∈ {c:ℚCube(k)| ↑Inhabited(c)} 
BY
{ ((MemTypeCD THEN Auto) THEN BLemma `inhabited-rat-cube-iff-point`  THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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)
12.  d  =  a
\mvdash{}  d  \mmember{}  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\} 


By

---

Latex:
((MemTypeCD  THEN  Auto)  THEN  BLemma  `inhabited-rat-cube-iff-point`    THEN  Auto)

---

Home Index