---

Step * 1 3 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. ¬(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)
BY
{ (Assert r0 ≤ rmin(mdist(snd((X i2));x1;y1);r1)⋅ 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.  y1  :  fst((X  i1))
8.  i  :  T
9.  \mneg{}(i  =  i1)
10.  \mneg{}(i2  =  i)
11.  z1  :  fst((X  i))
12.  i2  =  i1
\mvdash{}  r1  \mleq{}  (rmin(mdist(snd((X  i2));x1;y1);r1)  +  r1)


By

---

Latex:
(Assert  r0  \mleq{}  rmin(mdist(snd((X  i2));x1;y1);r1)\mcdot{}  THEN  Auto)

---

Home Index