---

Step * of Lemma ip-ge-dist

∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point].  ((||a - b|| ≤ ||c - d||) ⇒ (¬¬(∃w:Point. (a_b_w ∧ cd=aw))))
BY
{ (Auto THEN (StableCases ⌜a # b⌝⋅ THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ||a - b|| ≤ ||c - d||
7. a # b
⊢ ¬¬(∃w:Point. (a_b_w ∧ cd=aw))

2
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ||a - b|| ≤ ||c - d||
7. ¬a # b
⊢ ¬¬(∃w:Point. (a_b_w ∧ cd=aw))

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,d:Point].
    ((||a  -  b||  \mleq{}  ||c  -  d||)  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}w:Point.  (a\_b\_w  \mwedge{}  cd=aw))))


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}a  \#  b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index