legacy/oldlocal/ch_local/CKQOWSA.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: CKQOWSA                                                                  *)
   5 (* Chapter: local                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-03-12                                                           *)
   8 (* ========================================================================== *)
   9
  10 flyspeck_needs "general/sphere.hl";;
  11
  12 let tarski_3point_concl = `!v0 v1 v2.   {v0,v1,v2} SUBSET ball_annulus /\
  13   packing {v0,v1,v2} /\
  14    dist(v1,v2) <= &2 * h0 /\  ~(v0 IN {v1,v2}) ==>
  15   (   aff_ge {vec 0} {v0} INTER aff_ge {vec 0 } { v1,v2} = {vec 0})`;;
  16
  17 let tarski_4point_concl = `!v0 v1 v2 v3.  {v0,v1,v2,v3} SUBSET ball_annulus /\
  18    packing {v0,v1,v2,v3} /\
  19    dist(v1,v3) <= &2 * h0  /\ dist (v0,v2) <= &2 * h0 /\
  20    ({v0,v2} INTER {v1,v3} = {}) ==>
  21    ( aff_ge {vec 0} {v0,v2} INTER aff_ge {vec 0} {v1,v3} = {vec 0})`;;
  22
  23 let CKQOWSA_concl = `!V. packing V /\ V SUBEST ball_annulus ==>
  24   fan (vec 0,V,ESTD V)`;;
  25