---

Step * of Lemma rv-Cauchy-Schwarz

∀[rv:InnerProductSpace]. ∀[a,b:Point].  (a ⋅ b^2 ≤ (a^2 * b^2))
BY
{ (Auto THEN (DoubleNegation THENA Auto) THEN ((DistinguishCases ⌜b # 0⌝⋅ THENM RemoveDoubleNegation) THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. b # 0
⊢ a ⋅ b^2 ≤ (a^2 * b^2)

2
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. ¬b # 0
⊢ a ⋅ b^2 ≤ (a^2 * b^2)

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b:Point].    (a  \mcdot{}  b\^{}2  \mleq{}  (a\^{}2  *  b\^{}2))


By

---

Latex:
(Auto
  THEN  (DoubleNegation  THENA  Auto)
  THEN  ((DistinguishCases  \mkleeneopen{}b  \#  0\mkleeneclose{}\mcdot{}  THENM  RemoveDoubleNegation)  THENA  Auto))

---

Home Index