---

Step * of Lemma member-rat-complex-subdiv2

∀k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k).  ((c ∈ (K)') ⇐⇒ ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜K ∈ {c:ℚCube(k)| ↑Inhabited(c)}  List⌝⋅
   THENM (InstLemma `member-rat-complex-subdiv` [⌜k⌝;⌜K⌝;⌜c⌝]⋅ THEN Auto)
   )
   THEN DVar `K') }

1
1. k : ℕ
2. n : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K) ∧ (∀c,d∈K.  Compatible(c;d)) ∧ (∀c∈K.dim(c) = n ∈ ℤ)
5. c : ℚCube(k)
⊢ K ∈ {c:ℚCube(k)| ↑Inhabited(c)}  List

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.  \mforall{}K:n-dim-complex.  \mforall{}c:\mBbbQ{}Cube(k).
    ((c  \mmember{}  (K)')  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:\mBbbQ{}Cube(k).  ((a  \mmember{}  K)  \mwedge{}  (\muparrow{}is-half-cube(k;c;a))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}K  \mmember{}  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    List\mkleeneclose{}\mcdot{}
  THENM  (InstLemma  `member-rat-complex-subdiv`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
  )
  THEN  DVar  `K')

---

Home Index