Step * of Lemma rn-metric-leq-max-metric

[n:ℕ]. rn-metric(n) ≤ r(n)*max-metric(n)
BY
(InstLemma `rn-metric-leq-rn-prod-metric` []
   THEN ParallelLast'
   THEN (InstLemma `rn-prod-metric-le-max-metric` [⌜n⌝]⋅ THENA Auto)) }

1
1. [n] : ℕ
2. rn-metric(n) ≤ rn-prod-metric(n)
3. rn-prod-metric(n) ≤ r(n)*max-metric(n)
⊢ rn-metric(n) ≤ r(n)*max-metric(n)


Latex:


Latex:
\mforall{}[n:\mBbbN{}].  rn-metric(n)  \mleq{}  r(n)*max-metric(n)


By


Latex:
(InstLemma  `rn-metric-leq-rn-prod-metric`  []
  THEN  ParallelLast'
  THEN  (InstLemma  `rn-prod-metric-le-max-metric`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))




Home Index