---

Step * of Lemma simplex-face_wf

∀[n:ℤ]. ∀[v:Δ(n)]. ∀[i:ℕn + 2].  (simplex-face(v;i) ∈ Δ(n + 1))
BY
{ (Auto
   THEN ((Decide ⌜0 ≤ n⌝⋅ THENA Auto)
         THENL [((InstLemma `std-simplex-properties` [⌜n⌝;⌜v⌝]⋅ THENA Auto)
                 THEN MemTypeCD
                 THEN RepUR ``real-vec simplex-face`` 0
                 THEN Auto)
               ; (InstLemma `std-simplex-void` [⌜n⌝]⋅ THEN Auto)]
        )
   ) }

1
1. n : ℤ
2. v : Δ(n)
3. i : ℕn + 2
4. 0 ≤ n
5. ∀i:ℕn + 1. (r0 ≤ (v i))
6. Σ{v i | 0≤i≤n} = r1
7. ∀i@0:ℕ(n + 1) + 1. (r0 ≤ if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi )
⊢ Σ{if i@0 <z i then v i@0 if i <z i@0 then v (i@0 - 1) else r0 fi  | 0≤i@0≤n + 1} = r1

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[v:\mDelta{}(n)].  \mforall{}[i:\mBbbN{}n  +  2].    (simplex-face(v;i)  \mmember{}  \mDelta{}(n  +  1))


By

---

Latex:
(Auto
  THEN  ((Decide  \mkleeneopen{}0  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((InstLemma  `std-simplex-properties`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  MemTypeCD
                              THEN  RepUR  ``real-vec  simplex-face``  0
                              THEN  Auto)
                          ;  (InstLemma  `std-simplex-void`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)]
            )
  )

---

Home Index