---

Step * 1 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 i));x1;z1);r1) ≤ (rmin(mdist(snd((X i));x1;y1);r1) + rmin(mdist(snd((X i));z1;y1);r1))
BY
{ ((Assert mdist(snd((X i));x1;z1) ≤ (mdist(snd((X i));x1;y1) + mdist(snd((X i));z1;y1)) BY
          Auto)
   THEN MoveToConcl (-1)
   THEN ((Assert r0 ≤ mdist(snd((X i));x1;y1) BY (BLemma `mdist-nonneg` THEN Auto)) THEN MoveToConcl (-1))
   THEN ((Assert r0 ≤ mdist(snd((X i));z1;y1) BY (BLemma `mdist-nonneg` THEN Auto)) THEN MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜mdist(snd((X i));x1;z1)⌝;⌜mdist(snd((X i));x1;y1)⌝;⌜mdist(snd((X i));z1;y1)⌝]⋅
   THEN All Thin
   THEN Auto) }

1
1. v : ℝ
2. v1 : ℝ
3. v2 : ℝ
4. r0 ≤ v2
5. r0 ≤ v1
6. v ≤ (v1 + v2)
⊢ rmin(v;r1) ≤ (rmin(v1;r1) + rmin(v2;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  i));x1;z1);r1)  \mleq{}  (rmin(mdist(snd((X  i));x1;y1);r1)
+  rmin(mdist(snd((X  i));z1;y1);r1))


By

---

Latex:
((Assert  mdist(snd((X  i));x1;z1)  \mleq{}  (mdist(snd((X  i));x1;y1)  +  mdist(snd((X  i));z1;y1))  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  ((Assert  r0  \mleq{}  mdist(snd((X  i));x1;y1)  BY
                            (BLemma  `mdist-nonneg`  THEN  Auto))
              THEN  MoveToConcl  (-1)
              )
  THEN  ((Assert  r0  \mleq{}  mdist(snd((X  i));z1;y1)  BY
                            (BLemma  `mdist-nonneg`  THEN  Auto))
              THEN  MoveToConcl  (-1)
              )
  THEN  GenConclTerms  Auto  [\mkleeneopen{}mdist(snd((X  i));x1;z1)\mkleeneclose{};\mkleeneopen{}mdist(snd((X  i));x1;y1)\mkleeneclose{};
  \mkleeneopen{}mdist(snd((X  i));z1;y1)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto)

---

Home Index