---

Step * 1 1 1 of Lemma compact-metric-to-metric-continuity


1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
9. k : ℕ+
10. mtb2 : m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. cmp2 : mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
12. x1 : i:ℕ2 ⟶ X
13. x2 : i:ℕ2 ⟶ X
14. x1 ≡ x2
⊢ mdist(dY;f (x1 0);f (x1 1)) ≡ mdist(dY;f (x2 0);f (x2 1))
BY
{ ((InstLemma `prod-metric-meq` [⌜2⌝;⌜λ2i.X⌝;⌜λ2i.d⌝;⌜x1⌝;⌜x2⌝]⋅ THENA Auto)
   THEN D -1
   THEN Thin (-1)
   THEN (D -1 THENA Auto)) }

1
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
9. k : ℕ+
10. mtb2 : m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. cmp2 : mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
12. x1 : i:ℕ2 ⟶ X
13. x2 : i:ℕ2 ⟶ X
14. x1 ≡ x2
15. ∀i:ℕ2. x1 i ≡ x2 i
⊢ mdist(dY;f (x1 0);f (x1 1)) ≡ mdist(dY;f (x2 0);f (x2 1))

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  cmplt  :  mcomplete(X  with  d)
4.  mtb  :  m-TB(X;d)
5.  Y  :  Type
6.  dY  :  metric(Y)
7.  f  :  X  {}\mrightarrow{}  Y
8.  \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
9.  k  :  \mBbbN{}\msupplus{}
10.  mtb2  :  m-TB(i:\mBbbN{}2  {}\mrightarrow{}  X;prod-metric(2;\mlambda{}\msubtwo{}i.d))
11.  cmp2  :  mcomplete(i:\mBbbN{}2  {}\mrightarrow{}  X  with  prod-metric(2;\mlambda{}i.d))
12.  x1  :  i:\mBbbN{}2  {}\mrightarrow{}  X
13.  x2  :  i:\mBbbN{}2  {}\mrightarrow{}  X
14.  x1  \mequiv{}  x2
\mvdash{}  mdist(dY;f  (x1  0);f  (x1  1))  \mequiv{}  mdist(dY;f  (x2  0);f  (x2  1))


By

---

Latex:
((InstLemma  `prod-metric-meq`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.X\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.d\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Thin  (-1)
  THEN  (D  -1  THENA  Auto))

---

Home Index