---

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


1. k : ℕ
2. c : ℚCube(k)
⊢ (∀l∈map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k))).no_repeats(ℚCube(k);l))
BY
{ (BLemma `l_all_iff` THEN Auto THEN GenListD (-1) THEN ExRepD) }

1
1. k : ℕ
2. c : ℚCube(k)
3. l : ℚCube(k) List
4. y : ℕk
5. (y ∈ filter(λj.(dim(c j) =z 1);upto(k)))
6. l = [lower-rc-face(c;y); upper-rc-face(c;y)] ∈ (ℚCube(k) List)
⊢ no_repeats(ℚCube(k);l)

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `l\_all\_iff`  THEN  Auto  THEN  GenListD  (-1)  THEN  ExRepD)

---

Home Index