---

Step * 1 1 of Lemma union-metric-space_wf


1. T : Type
2. eq : EqDecider(T)
3. X : T ⟶ MetricSpace
4. i2 : T
5. x1 : fst((X i2))
6. i1 : T
7. y1 : fst((X i1))
8. i : T
9. z1 : fst((X i))
10. i2 = i ∈ T
11. i2 = i1 ∈ T
12. i = i1 ∈ T
⊢ rmin(mdist(snd((X i2));x1;z1);r1) ≤ (rmin(mdist(snd((X i2));x1;y1);r1) + rmin(mdist(snd((X i));z1;y1);r1))
BY
{ (RWO "-1< -3" 0 THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. X : T ⟶ MetricSpace
4. i2 : T
5. x1 : fst((X i2))
6. i1 : T
7. y1 : fst((X i1))
8. i : T
9. z1 : fst((X i))
10. i2 = i ∈ T
11. i2 = i1 ∈ T
12. i = i1 ∈ T
⊢ rmin(mdist(snd((X i));x1;z1);r1) ≤ (rmin(mdist(snd((X i));x1;y1);r1) + rmin(mdist(snd((X i));z1;y1);r1))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  X  :  T  {}\mrightarrow{}  MetricSpace
4.  i2  :  T
5.  x1  :  fst((X  i2))
6.  i1  :  T
7.  y1  :  fst((X  i1))
8.  i  :  T
9.  z1  :  fst((X  i))
10.  i2  =  i
11.  i2  =  i1
12.  i  =  i1
\mvdash{}  rmin(mdist(snd((X  i2));x1;z1);r1)  \mleq{}  (rmin(mdist(snd((X  i2));x1;y1);r1)
+  rmin(mdist(snd((X  i));z1;y1);r1))


By

---

Latex:
(RWO  "-1<  -3"  0  THEN  Auto)

---

Home Index