legacy/oldpacking/DRUQUFE.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Lemma: DRUQUFE                                                             *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 Deprecated Dec 28, 2011. Content moved to pack_concl.hl
  12
  13 The corresponding theorem for `voronoi_open` has been proved by Nguyen Tat Thang.
  14 Hopefully, his proof can be adapted to this context.
  15
  16 The conclusion should be separated into three separate statements for useability.
  17 *)
  18
  19
  20
  21 module type Druqufe_type = sig
  22   val DRUQUFE_concl : term
  23 end;;
  24
  25
  26
  27 module Druqufe : Druqufe_type = struct
  28
  29  let DRUQUFE_concl = `!V (v:real^3). packing V /\ saturated V  ==>
  30      compact (voronoi_closed V v) /\ convex (voronoi_closed V v) /\ measurable (voronoi_closed V v)`;;
  31
  32 end;;
  33
  34