Step
*
of Lemma
m-k-regular-mcauchy
∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X]. ∀b:ℕ+. (m-k-regular(d;b;s)
⇒ mcauchy(d;n.s n))
BY
{ (Auto
THEN UnfoldTopAb (-1)
THEN (D 0 THENA Auto)
THEN (D 0 With ⌜(2 * b) * k⌝ THENA Auto)
THEN ParallelOp -2
THEN ParallelLast
THEN (RWO "-1" 0 THENA Auto)
THEN All Thin
THEN Auto) }
1
1. b : ℕ+
2. k : ℕ+
3. n : ℕ
4. m : ℕ
5. ((2 * b) * k) ≤ n
6. ((2 * b) * k) ≤ m
⊢ ((r(b)/r(n + 1)) + (r(b)/r(m + 1))) ≤ (r1/r(k))
Latex:
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[s:\mBbbN{} {}\mrightarrow{} X]. \mforall{}b:\mBbbN{}\msupplus{}. (m-k-regular(d;b;s) {}\mRightarrow{} mcauchy(d;n.s n))
By
Latex:
(Auto
THEN UnfoldTopAb (-1)
THEN (D 0 THENA Auto)
THEN (D 0 With \mkleeneopen{}(2 * b) * k\mkleeneclose{} THENA Auto)
THEN ParallelOp -2
THEN ParallelLast
THEN (RWO "-1" 0 THENA Auto)
THEN All Thin
THEN Auto)
Home
Index