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 ((ParallelLast' THENA Auto))
   THEN UnfoldTopAb 0
   THEN ParallelLast'
   THEN Auto) }

1
1. OrientedPlane
2. xs {xs:Point List| geo-general-position(g;xs)} 
3. : ℕ||xs||
4. : ℕ||xs||
5. ¬(i j ∈ ℤ)
6. ij ∈ Hull(xs)
7. 2 < ||xs||
8. : ℕ||xs||
9. ¬(k i ∈ ℤ)
10. ¬(k j ∈ ℤ)
11. ki ∈ Hull(xs)
12. ¬(k i ∈ ℤ)
13. ¬(k j ∈ ℤ)
14. ki ∈ Hull(xs)
15. : ℕ||xs||
16. ¬(y i ∈ ℤ)
17. ¬(y j ∈ ℤ)
18. yi ∈ Hull(xs)
⊢ 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