Step
*
of Lemma
meq-max-metric-iff-meq-rn-metric
∀[n:ℕ]. ∀[x,y:ℝ^n]. uiff(x ≡ y;x ≡ y)
BY
{ (Intros
THEN (InstLemma `rn-metric-leq-max-metric` [⌜n⌝]⋅ THENA Auto)
THEN (InstLemma `max-metric-leq-rn-metric` [⌜n⌝]⋅ THENA Auto)
THEN RepUR ``meq`` 0
THEN Fold `mdist` 0
THEN Auto
THEN BLemma `rleq_antisymmetry`
THEN Auto) }
1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. max-metric(n) ≤ rn-metric(n)
6. mdist(max-metric(n);x;y) = r0
⊢ mdist(rn-metric(n);x;y) ≤ r0
2
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. max-metric(n) ≤ rn-metric(n)
6. mdist(rn-metric(n);x;y) = r0
⊢ mdist(max-metric(n);x;y) ≤ r0
Latex:
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[x,y:\mBbbR{}\^{}n]. uiff(x \mequiv{} y;x \mequiv{} y)
By
Latex:
(Intros
THEN (InstLemma `rn-metric-leq-max-metric` [\mkleeneopen{}n\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `max-metric-leq-rn-metric` [\mkleeneopen{}n\mkleeneclose{}]\mcdot{} THENA Auto)
THEN RepUR ``meq`` 0
THEN Fold `mdist` 0
THEN Auto
THEN BLemma `rleq\_antisymmetry`
THEN Auto)
Home
Index