Step
*
of Lemma
rv-Cauchy-Schwarz-equality'
∀rv:InnerProductSpace. ∀a,b:Point. ((|a ⋅ b| = (||a|| * ||b||))
⇒ b # 0
⇒ (∃t:ℝ. a ≡ t*b))
BY
{ (InstLemma `rv-Cauchy-Schwarz-equality` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }
1
.....antecedent.....
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. |a ⋅ b| = (||a|| * ||b||)
⊢ a ⋅ b^2 = (a^2 * b^2)
Latex:
Latex:
\mforall{}rv:InnerProductSpace. \mforall{}a,b:Point. ((|a \mcdot{} b| = (||a|| * ||b||)) {}\mRightarrow{} b \# 0 {}\mRightarrow{} (\mexists{}t:\mBbbR{}. a \mequiv{} t*b))
By
Latex:
(InstLemma `rv-Cauchy-Schwarz-equality` [] THEN RepeatFor 4 (ParallelLast') THEN Auto)
Home
Index