---

Step * of Lemma prod-metric_wf

∀[k:ℕ]. ∀[X:ℕk ⟶ Type]. ∀[d:i:ℕk ⟶ metric(X[i])].  (prod-metric(k;d) ∈ metric(i:ℕk ⟶ X[i]))
BY
{ (RepUR ``prod-metric`` 0
   THEN Auto
   THEN (MemTypeCD THEN Auto)
   THEN Reduce 0
   THEN Try ((RWO "rsum-of-nonneg-zero-iff" 0 THEN Auto))
   THEN (RWO "rsum_linearity1<" 0 THENA Auto)
   THEN BLemma `rsum_functionality_wrt_rleq`
   THEN Auto
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[X:\mBbbN{}k  {}\mrightarrow{}  Type].  \mforall{}[d:i:\mBbbN{}k  {}\mrightarrow{}  metric(X[i])].    (prod-metric(k;d)  \mmember{}  metric(i:\mBbbN{}k  {}\mrightarrow{}  X[i]))


By

---

Latex:
(RepUR  ``prod-metric``  0
  THEN  Auto
  THEN  (MemTypeCD  THEN  Auto)
  THEN  Reduce  0
  THEN  Try  ((RWO  "rsum-of-nonneg-zero-iff"  0  THEN  Auto))
  THEN  (RWO  "rsum\_linearity1<"  0  THENA  Auto)
  THEN  BLemma  `rsum\_functionality\_wrt\_rleq`
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index