---

Step * 1 2 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. ¬(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)
BY
{ (BLemma `rmin_lb`  THEN Auto) }

---

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.  \mneg{}(i2  =  i1)
8.  y1  :  fst((X  i1))
9.  i  :  T
10.  \mneg{}(i  =  i1)
11.  z1  :  fst((X  i))
12.  i2  =  i
\mvdash{}  rmin(mdist(snd((X  i2));x1;z1);r1)  \mleq{}  (r1  +  r1)


By

---

Latex:
(BLemma  `rmin\_lb`    THEN  Auto)

---

Home Index