---

Step * of Lemma in-hull-next

∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i,j:ℕ||xs||.
  ((¬(i = j ∈ ℤ)) ⇒ ij ∈ Hull(xs) ⇒ (∃k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ∧ ki ∈ Hull(xs))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (Decide ⌜2 < ||xs||⌝⋅ THENA Auto)) }

1
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. 2 < ||xs||
⊢ ∀i,j:ℕ||xs||.  ((¬(i = j ∈ ℤ)) ⇒ ij ∈ Hull(xs) ⇒ (∃k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ∧ ki ∈ Hull(xs))))

2
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. ¬2 < ||xs||
⊢ ∀i,j:ℕ||xs||.  ((¬(i = j ∈ ℤ)) ⇒ ij ∈ Hull(xs) ⇒ (∃k:ℕ||xs||. ((¬(k = i ∈ ℤ)) ∧ ki ∈ Hull(xs))))

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}xs:\{xs:Point  List|  geo-general-position(g;xs)\}  .  \mforall{}i,j:\mBbbN{}||xs||.
    ((\mneg{}(i  =  j))  {}\mRightarrow{}  ij  \mmember{}  Hull(xs)  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}||xs||.  ((\mneg{}(k  =  i))  \mwedge{}  ki  \mmember{}  Hull(xs))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  (Decide  \mkleeneopen{}2  <  ||xs||\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index