Step
*
of Lemma
in-hull-unique-next2
∀g:OrientedPlane. ∀xs:{xs:Point List| geo-general-position(g;xs)} . ∀i,j:ℕ||xs||.
  ((¬(i = j ∈ ℤ)) 
⇒ (ij ∈ Hull(xs) ∧ 2 < ||xs||) 
⇒ (∃!k:ℕ||xs||. (((¬(k = i ∈ ℤ)) ∧ (¬(k = j ∈ ℤ))) ∧ ki ∈ Hull(xs))))
BY
{ (InstLemma `in-hull-next2` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN UnfoldTopAb 0
   THEN ParallelLast'
   THEN Auto) }
1
1. g : OrientedPlane
2. xs : {xs:Point List| geo-general-position(g;xs)} 
3. i : ℕ||xs||
4. j : ℕ||xs||
5. ¬(i = j ∈ ℤ)
6. ij ∈ Hull(xs)
7. 2 < ||xs||
8. k : ℕ||xs||
9. ¬(k = i ∈ ℤ)
10. ¬(k = j ∈ ℤ)
11. ki ∈ Hull(xs)
12. ¬(k = i ∈ ℤ)
13. ¬(k = j ∈ ℤ)
14. ki ∈ Hull(xs)
15. y : ℕ||xs||
16. ¬(y = i ∈ ℤ)
17. ¬(y = j ∈ ℤ)
18. yi ∈ Hull(xs)
⊢ y = k ∈ ℕ||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)  \mwedge{}  2  <  ||xs||)
    {}\mRightarrow{}  (\mexists{}!k:\mBbbN{}||xs||.  (((\mneg{}(k  =  i))  \mwedge{}  (\mneg{}(k  =  j)))  \mwedge{}  ki  \mmember{}  Hull(xs))))
By
Latex:
(InstLemma  `in-hull-next2`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  UnfoldTopAb  0
  THEN  ParallelLast'
  THEN  Auto)
Home
Index