---

Step * 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))
⊢ if eq i2 i then rmin(mdist(snd((X i2));x1;z1);r1) else r1 fi  ≤ (if eq i2 i1
then rmin(mdist(snd((X i2));x1;y1);r1)
else r1
fi 
+ if eq i i1 then rmin(mdist(snd((X i));z1;y1);r1) else r1 fi )
BY
{ RepeatFor 3 (AutoSplit) }

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 i2));x1;z1);r1) ≤ (rmin(mdist(snd((X i2));x1;y1);r1) + rmin(mdist(snd((X i));z1;y1);r1))

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

3
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. ¬(i = i1 ∈ T)
10. ¬(i2 = i ∈ T)
11. z1 : fst((X i))
12. i2 = i1 ∈ T
⊢ r1 ≤ (rmin(mdist(snd((X i2));x1;y1);r1) + 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))
\mvdash{}  if  eq  i2  i  then  rmin(mdist(snd((X  i2));x1;z1);r1)  else  r1  fi    \mleq{}  (if  eq  i2  i1
then  rmin(mdist(snd((X  i2));x1;y1);r1)
else  r1
fi 
+  if  eq  i  i1  then  rmin(mdist(snd((X  i));z1;y1);r1)  else  r1  fi  )


By

---

Latex:
RepeatFor  3  (AutoSplit)

---

Home Index