---

Step * of Lemma simplex-metric_wf

∀[n:ℤ]. (simplex-metric(n) ∈ metric(Δ(n)))
BY
{ (Intro
   THEN Unhide
   THEN ((Decide ⌜n < 0⌝⋅ THEN Auto)
         THENL [(SubsumeC ⌜Top⌝⋅
                 THEN Try (BLemma  `metric-on-void` )
                 THEN Auto
                 THEN BLemma `std-simplex-void`
                 THEN Auto)
               ; ProveWfLemma]
   )) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (simplex-metric(n)  \mmember{}  metric(\mDelta{}(n)))


By

---

Latex:
(Intro
  THEN  Unhide
  THEN  ((Decide  \mkleeneopen{}n  <  0\mkleeneclose{}\mcdot{}  THEN  Auto)
              THENL  [(SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}
                              THEN  Try  (BLemma    `metric-on-void`  )
                              THEN  Auto
                              THEN  BLemma  `std-simplex-void`
                              THEN  Auto)
                          ;  ProveWfLemma]
  ))

---

Home Index