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