---

Step * of Lemma rat-complex-subdiv-non-nil

No Annotations
∀[k,n:ℕ]. ∀[K:n-dim-complex].  0 < ||(K)'|| supposing 0 < ||K||
BY
{ (Auto
   THEN ((InstLemma `member_not_nil` [⌜ℚCube(k)⌝;⌜(K)'⌝]⋅
         THENM (MoveToConcl (-1)
                THEN GenConclTerm ⌜(K)'⌝⋅
                THEN Auto
                THEN (RepeatFor 2 (DVar `v') THEN All Reduce)
                THEN Auto)
         )
         THENA (Auto
                THEN (RWO  "member-rat-complex-subdiv2" 0 THENA Auto)
                THEN RepeatFor 2 (DVar `K')
                THEN All Reduce
                THEN Auto
                THEN (Assert ⌜∃x:ℚCube(k). (↑is-half-cube(k;x;u))⌝⋅ THENM (ParallelLast THEN Auto))
                THEN All Thin)
         )
   ) }

1
1. k : ℕ
2. u : ℚCube(k)
⊢ ∃x:ℚCube(k). (↑is-half-cube(k;x;u))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:n-dim-complex].    0  <  ||(K)'||  supposing  0  <  ||K||


By

---

Latex:
(Auto
  THEN  ((InstLemma  `member\_not\_nil`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}(K)'\mkleeneclose{}]\mcdot{}
              THENM  (MoveToConcl  (-1)
                            THEN  GenConclTerm  \mkleeneopen{}(K)'\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  (RepeatFor  2  (DVar  `v')  THEN  All  Reduce)
                            THEN  Auto)
              )
              THENA  (Auto
                            THEN  (RWO    "member-rat-complex-subdiv2"  0  THENA  Auto)
                            THEN  RepeatFor  2  (DVar  `K')
                            THEN  All  Reduce
                            THEN  Auto
                            THEN  (Assert  \mkleeneopen{}\mexists{}x:\mBbbQ{}Cube(k).  (\muparrow{}is-half-cube(k;x;u))\mkleeneclose{}\mcdot{}  THENM  (ParallelLast  THEN  Auto))
                            THEN  All  Thin)
              )
  )

---

Home Index