---

Step * 1 of Lemma compatible-cubes-with-interior-point


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. x : ℕk ⟶ ℚ
5. rat-point-in-cube-interior(k;x;a)
6. rat-point-in-cube(k;x;b)
7. rat-point-in-cube(k;x;a)
8. a ⋂ b ≤ a ∧ a ⋂ b ≤ b
⊢ a ≤ b
BY
{ (InstLemma `rat-point-in-cube-interior-not-in-face` [⌜k⌝;⌜x⌝;⌜a⌝;⌜a ⋂ b⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  x  :  \mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}
5.  rat-point-in-cube-interior(k;x;a)
6.  rat-point-in-cube(k;x;b)
7.  rat-point-in-cube(k;x;a)
8.  a  \mcap{}  b  \mleq{}  a  \mwedge{}  a  \mcap{}  b  \mleq{}  b
\mvdash{}  a  \mleq{}  b


By

---

Latex:
(InstLemma  `rat-point-in-cube-interior-not-in-face`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a  \mcap{}  b\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index