---

Step * of Lemma member-face-complex

∀k:ℕ. ∀K:ℚCube(k) List. ∀f:ℚCube(k).
  ((f ∈ face-complex(k;K)) ⇐⇒ ∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ (f ∈ rat-cube-faces(k;c))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `face-complex` 0
   THEN (RWO  "member-remove-repeats" 0 THENA Auto)
   THEN (RWW "l_all_iff member-concat member-map" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN ExRepD) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. f : ℚCube(k)
4. l : ℚCube(k) List
5. y : ℚCube(k)
6. (y ∈ K)
7. l = if Inhabited(y) then rat-cube-faces(k;y) else [] fi  ∈ (ℚCube(k) List)
8. (f ∈ l)
⊢ ∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ (f ∈ rat-cube-faces(k;c)))

2
1. k : ℕ
2. K : ℚCube(k) List
3. f : ℚCube(k)
4. c : ℚCube(k)
5. (c ∈ K)
6. ↑Inhabited(c)
7. (f ∈ rat-cube-faces(k;c))
⊢ ∃l:ℚCube(k) List
   ((∃y:ℚCube(k). ((y ∈ K) ∧ (l = if Inhabited(y) then rat-cube-faces(k;y) else [] fi  ∈ (ℚCube(k) List)))) ∧ (f ∈ l))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}K:\mBbbQ{}Cube(k)  List.  \mforall{}f:\mBbbQ{}Cube(k).
    ((f  \mmember{}  face-complex(k;K))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  \mwedge{}  (\muparrow{}Inhabited(c))  \mwedge{}  (f  \mmember{}  rat-cube-faces(k;c))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `face-complex`  0
  THEN  (RWO    "member-remove-repeats"  0  THENA  Auto)
  THEN  (RWW  "l\_all\_iff  member-concat  member-map"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index