---

Step * of Lemma union-metric-space_wf

No Annotations
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[X:T ⟶ MetricSpace].  (union-metric-space(T;eq;X) ∈ MetricSpace)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Reduce 0 THEN Auto THEN DProdsAndUnions THEN Reduce 0) }

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))
⊢ 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 )

2
1. T : Type
2. eq : EqDecider(T)
3. X : T ⟶ MetricSpace
4. ∀x,y,z:i:T × (fst((X i))).
     (let i,v = x 
      in let j,w = z 
         in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi  ≤ (let i,v = x 
                                                                         in let j,w = y 
                                                                            in if eq i j
                                                                               then rmin(mdist(snd((X i));v;w);r1)
                                                                               else r1
                                                                               fi 
     + let i,v = z 
       in let j,w = y 
          in if eq i j then rmin(mdist(snd((X i));v;w);r1) else r1 fi ))
5. i : T
6. x1 : fst((X i))
⊢ if eq i i then rmin(mdist(snd((X i));x1;x1);r1) else r1 fi  = r0

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[X:T  {}\mrightarrow{}  MetricSpace].    (union-metric-space(T;eq;X)  \mmember{}  MetricSpace)


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto  THEN  DProdsAndUnions  THEN  Reduce  0)

---

Home Index