---

Step * of Lemma no_repeats-rat-cube-faces

No Annotations
∀k:ℕ. ∀c:ℚCube(k).  no_repeats(ℚCube(k);rat-cube-faces(k;c))
BY
{ (Auto THEN RepUR ``rat-cube-faces mapfilter`` 0 THEN (BLemma `no_repeats-concat` THENA Auto)) }

1
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))

2
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))

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).    no\_repeats(\mBbbQ{}Cube(k);rat-cube-faces(k;c))


By

---

Latex:
(Auto  THEN  RepUR  ``rat-cube-faces  mapfilter``  0  THEN  (BLemma  `no\_repeats-concat`  THENA  Auto))

---

Home Index