---

Step * of Lemma ip-gt-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  >  ab;||a  -  b||  <  ||c  -  d||)


By

---

Latex:
Auto

---

Home Index