---

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

No Annotations
∀k:ℕ. ∀a,b:ℚCube(k).
  (a ≤ b) supposing ((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and Compatible(a;b))
BY
{ ((Auto THEN Unhide THEN Auto)
   THEN ExRepD
   THEN (Assert rat-point-in-cube(k;x;a) BY
               (UnfoldTopAb 0 THEN UnfoldTopAb 6 THEN ParallelOp 6 THEN Auto))
   THEN (D 4 THENA ((BLemma `inhabited-rat-cube-iff-point` THEN Auto) THEN D 0 With ⌜x⌝  THEN EAuto 1))) }

1
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}a,b:\mBbbQ{}Cube(k).
    (a  \mleq{}  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))


By

---

Latex:
((Auto  THEN  Unhide  THEN  Auto)
  THEN  ExRepD
  THEN  (Assert  rat-point-in-cube(k;x;a)  BY
                          (UnfoldTopAb  0  THEN  UnfoldTopAb  6  THEN  ParallelOp  6  THEN  Auto))
  THEN  (D  4
              THENA  ((BLemma  `inhabited-rat-cube-iff-point`  THEN  Auto)  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  EAuto  1)
              ))

---

Home Index