---

Step * of Lemma in-rat-cube_functionality

∀[k:ℕ]. ∀[p,q:ℝ^k]. ∀[c:ℚCube(k)].  uiff(in-rat-cube(k;p;c);in-rat-cube(k;q;c)) supposing p ≡ q
BY
{ (Auto THEN (RWO "meq-rn-prod-metric" (-2) THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN D 5 With ⌜i⌝  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[p,q:\mBbbR{}\^{}k].  \mforall{}[c:\mBbbQ{}Cube(k)].    uiff(in-rat-cube(k;p;c);in-rat-cube(k;q;c))  supposing  p  \mequiv{}  q


By

---

Latex:
(Auto
  THEN  (RWO  "meq-rn-prod-metric"  (-2)  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  D  5  With  \mkleeneopen{}i\mkleeneclose{} 
  THEN  Auto)

---

Home Index