---

Step * of Lemma ip-ge-sep

∀rv:InnerProductSpace. ∀a,c:Point.  ∀[b:Point]. (a # c) supposing (a # b and ac ≥ ab)
BY
{ (Auto THEN Unhide THEN Auto THEN (FLemma `ip-ge-iff` [-2] THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. c : Point
4. b : Point
5. ac ≥ ab
6. a # b
7. ||a - b|| ≤ ||a - c||
⊢ a # c

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,c:Point.    \mforall{}[b:Point].  (a  \#  c)  supposing  (a  \#  b  and  ac  \mgeq{}  ab)


By

---

Latex:
(Auto  THEN  Unhide  THEN  Auto  THEN  (FLemma  `ip-ge-iff`  [-2]  THENA  Auto))

---

Home Index