---

Step * of Lemma ip-ge-iff

No Annotations
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)].  uiff(cd ≥ ab;||a - b|| ≤ ||c - d||)
BY
{ Auto }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. cd ≥ ab
⊢ ||a - b|| ≤ ||c - d||

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. d : Point(rv)
6. ||a - b|| ≤ ||c - d||
⊢ cd ≥ ab

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,d:Point(rv)].    uiff(cd  \mgeq{}  ab;||a  -  b||  \mleq{}  ||c  -  d||)


By

---

Latex:
Auto

---

Home Index