---

Step * of Lemma compatible-same-dim-cubes-with-interior-point

No Annotations
∀[k:ℕ]. ∀[a,b:ℚCube(k)].
  (a = b ∈ ℚCube(k)) supposing 
     ((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and 
     Compatible(a;b) and 
     (dim(a) = dim(b) ∈ ℤ))
BY
{ (InstLemma `compatible-cubes-with-interior-point` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ParallelOp -2
   THEN ParallelLast
   THEN InstLemma `rat-cube-face-dimension-equal` [⌜k⌝;⌜b⌝;⌜a⌝]⋅
   THEN Auto
   THEN ExRepD
   THEN EAuto 2) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[a,b:\mBbbQ{}Cube(k)].
    (a  =  b)  supposing 
          ((\mexists{}x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}.  (rat-point-in-cube-interior(k;x;a)  \mwedge{}  rat-point-in-cube(k;x;b)))  and 
          Compatible(a;b)  and 
          (dim(a)  =  dim(b)))


By

---

Latex:
(InstLemma  `compatible-cubes-with-interior-point`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ParallelLast
  THEN  InstLemma  `rat-cube-face-dimension-equal`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ExRepD
  THEN  EAuto  2)

---

Home Index