---

Step * of Lemma circle-param-onto

∀p:{p:ℝ^2| r2-unit-circle(p)} . ((r(-1) < (p 0)) ⇒ (∃t:ℝ. req-vec(2;circle-param(t);p)))
BY
{ (Auto THEN (Assert r2-unit-circle(p) BY (All (Unfold `r2-unit-circle`)⋅ THEN Auto)) THEN D 1 THEN Thin 2) }

1
1. p : ℝ^2
2. r(-1) < (p 0)
3. r2-unit-circle(p)
⊢ ∃t:ℝ. req-vec(2;circle-param(t);p)

---

Latex:

---

Latex:
\mforall{}p:\{p:\mBbbR{}\^{}2|  r2-unit-circle(p)\}  .  ((r(-1)  <  (p  0))  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  req-vec(2;circle-param(t);p)))


By

---

Latex:
(Auto
  THEN  (Assert  r2-unit-circle(p)  BY
                          (All  (Unfold  `r2-unit-circle`)\mcdot{}  THEN  Auto))
  THEN  D  1
  THEN  Thin  2)

---

Home Index