---

Step * of Lemma rv-unit_wf

No Annotations
∀[rv:InnerProductSpace]. ∀[x:Point(rv)].  rv-unit(rv;x) ∈ {z:Point(rv)| z^2 = r1}  supposing x # 0
BY
{ (Auto THEN (FLemma `rv-norm-positive` [-1] THENA Auto) THEN Unfold `rv-unit` 0 THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. rv : InnerProductSpace
2. x : Point(rv)
3. x # 0
4. r0 < ||x||
⊢ (r1/||x||)*x^2 = r1

---

Latex:

---

Latex:
No  Annotations
\mforall{}[rv:InnerProductSpace].  \mforall{}[x:Point(rv)].    rv-unit(rv;x)  \mmember{}  \{z:Point(rv)|  z\^{}2  =  r1\}    supposing  x  \#  0


By

---

Latex:
(Auto
  THEN  (FLemma  `rv-norm-positive`  [-1]  THENA  Auto)
  THEN  Unfold  `rv-unit`  0
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index