legacy/oldpacking/TIWWFYQ.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: TIWWFYQ                                                             *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 R^3 is the union of Voronoi cells.
  15
  16 We write this in pointwise form: for every p IN R^3, there exists a cell to which it belongs.
  17
  18 Deprecated, Dec 28 2011.  Content moved to pack_con.hl.
  19 *)
  20
  21
  22
  23 module type Tiwwfyq_def_type = sig
  24   val TIWWFYQ_concl : term
  25
  26 (* val TIWWFYQ : thm *)
  27
  28 end;;
  29
  30
  31
  32 module Tiwwfyq : Tiwwfyq_def_type = struct
  33
  34  let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v.  v IN V /\ p IN voronoi_closed V v)`;;
  35
  36 end;;
  37