---

Step * 1 of Lemma no_repeats-rat-cube-faces


1. k : ℕ
2. c : ℚCube(k)
⊢ (∀l1,l2∈map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k))).
   l_disjoint(ℚCube(k);l1;l2))
BY
{ ((RWO  "pairwise-map" 0 THENA Auto)
   THEN (RWO "pairwise-iff2" 0 THENA Auto)
   THEN Try ((RepeatFor 3 (ParallelLast) THEN Auto))) }

1
1. k : ℕ
2. c : ℚCube(k)
⊢ ∀l1,l2:ℕk.
    ((l1 ∈ filter(λj.(dim(c j) =z 1);upto(k)))
    ⇒ (l2 ∈ filter(λj.(dim(c j) =z 1);upto(k)))
    ⇒ (¬(l1 = l2 ∈ ℕk))
    ⇒ l_disjoint(ℚCube(k);(λj.[lower-rc-face(c;j); upper-rc-face(c;j)]) 
                           l1;(λj.[lower-rc-face(c;j); upper-rc-face(c;j)]) l2))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
\mvdash{}  (\mforall{}l1,l2\mmember{}map(\mlambda{}j.[lower-rc-face(c;j);  upper-rc-face(c;j)];filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k))).
      l\_disjoint(\mBbbQ{}Cube(k);l1;l2))


By

---

Latex:
((RWO    "pairwise-map"  0  THENA  Auto)
  THEN  (RWO  "pairwise-iff2"  0  THENA  Auto)
  THEN  Try  ((RepeatFor  3  (ParallelLast)  THEN  Auto)))

---

Home Index