---

Step * of Lemma r2-equidistant-implies'

∀a,b:ℝ^2.  (a ≠ b ⇒ (∀x:ℝ^2. (xa=xb ⇒ (∃t:ℝ. req-vec(2;x;vec-midpoint(a;b) + t*r2-perp(b - a))))))
BY
{ (InstLemma `r2-equidistant-implies` [] THEN RepeatFor 6 ((ParallelLast' THENA Auto))) }

1
1. a : ℝ^2
2. b : ℝ^2
3. a ≠ b
4. x : ℝ^2
5. d(x;a) = d(x;b)
⊢ d(a;x) = d(b;x)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}\^{}2.    (a  \mneq{}  b  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}\^{}2.  (xa=xb  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  req-vec(2;x;vec-midpoint(a;b)  +  t*r2-perp(b  -  a))))))


By

---

Latex:
(InstLemma  `r2-equidistant-implies`  []  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto)))

---

Home Index