---

Step * 1 of Lemma meq-equiv


1. X : Type
2. d : X ⟶ X ⟶ ℝ
3. ∀x,y,z:X.  ((d x z) ≤ ((d x y) + (d z y)))
4. ∀x:X. ((d x x) = r0)
5. ∀x,y:X.  ((d x y) = (d y x))
6. Sym(X;x,y.(d x y) = r0)
7. a : X
8. b : X
9. c : X
10. (d a b) = r0
11. (d b c) = r0
⊢ (d a c) ≤ r0
BY
{ ((Assert (d a c) ≤ ((d a b) + (d c b)) BY Auto) THEN (RWO  "-1" 0 THENA Auto) THEN (RWO "-3" 0 THENA Auto)) }

1
1. X : Type
2. d : X ⟶ X ⟶ ℝ
3. ∀x,y,z:X.  ((d x z) ≤ ((d x y) + (d z y)))
4. ∀x:X. ((d x x) = r0)
5. ∀x,y:X.  ((d x y) = (d y x))
6. Sym(X;x,y.(d x y) = r0)
7. a : X
8. b : X
9. c : X
10. (d a b) = r0
11. (d b c) = r0
12. (d a c) ≤ ((d a b) + (d c b))
⊢ (r0 + (d c b)) ≤ r0

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x,y,z:X.    ((d  x  z)  \mleq{}  ((d  x  y)  +  (d  z  y)))
4.  \mforall{}x:X.  ((d  x  x)  =  r0)
5.  \mforall{}x,y:X.    ((d  x  y)  =  (d  y  x))
6.  Sym(X;x,y.(d  x  y)  =  r0)
7.  a  :  X
8.  b  :  X
9.  c  :  X
10.  (d  a  b)  =  r0
11.  (d  b  c)  =  r0
\mvdash{}  (d  a  c)  \mleq{}  r0


By

---

Latex:
((Assert  (d  a  c)  \mleq{}  ((d  a  b)  +  (d  c  b))  BY
                Auto)
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  (RWO  "-3"  0  THENA  Auto))

---

Home Index