---

Step * of Lemma r2-perp_wf

∀[x:ℝ^2]. ((r0 < ||x||) ⇒ (r2-perp(x) ∈ {y:ℝ^2| (x⋅y = r0) ∧ (||y|| = r1)} ))
BY
{ (Auto THEN (Assert r2-perp(x) ∈ ℝ^2 BY ProveWfLemma) THEN MemTypeCD THEN Auto) }

1
1. x : ℝ^2
2. r0 < ||x||
3. r2-perp(x) ∈ ℝ^2
⊢ x⋅r2-perp(x) = r0

2
1. x : ℝ^2
2. r0 < ||x||
3. r2-perp(x) ∈ ℝ^2
4. x⋅r2-perp(x) = r0
⊢ ||r2-perp(x)|| = r1

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}\^{}2].  ((r0  <  ||x||)  {}\mRightarrow{}  (r2-perp(x)  \mmember{}  \{y:\mBbbR{}\^{}2|  (x\mcdot{}y  =  r0)  \mwedge{}  (||y||  =  r1)\}  ))


By

---

Latex:
(Auto  THEN  (Assert  r2-perp(x)  \mmember{}  \mBbbR{}\^{}2  BY  ProveWfLemma)  THEN  MemTypeCD  THEN  Auto)

---

Home Index