---

Step * 2 of Lemma union-metric-space_wf


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
BY
{ (AutoSplit THEN (RWO "mdist-same" 0 THEN Auto) THEN RWO "rmin-req2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  X  :  T  {}\mrightarrow{}  MetricSpace
4.  \mforall{}x,y,z:i:T  \mtimes{}  (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    \mleq{}  (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))
\mvdash{}  if  eq  i  i  then  rmin(mdist(snd((X  i));x1;x1);r1)  else  r1  fi    =  r0


By

---

Latex:
(AutoSplit  THEN  (RWO  "mdist-same"  0  THEN  Auto)  THEN  RWO  "rmin-req2"  0  THEN  Auto)

---

Home Index