---

Step * 2 of Lemma member-face-complex


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))
BY
{ (D 0 With ⌜if Inhabited(c) then rat-cube-faces(k;c) else [] fi ⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  f  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  (c  \mmember{}  K)
6.  \muparrow{}Inhabited(c)
7.  (f  \mmember{}  rat-cube-faces(k;c))
\mvdash{}  \mexists{}l:\mBbbQ{}Cube(k)  List
      ((\mexists{}y:\mBbbQ{}Cube(k).  ((y  \mmember{}  K)  \mwedge{}  (l  =  if  Inhabited(y)  then  rat-cube-faces(k;y)  else  []  fi  )))  \mwedge{}  (f  \mmember{}  l))


By

---

Latex:
(D  0  With  \mkleeneopen{}if  Inhabited(c)  then  rat-cube-faces(k;c)  else  []  fi  \mkleeneclose{}    THEN  Auto)

---

Home Index