1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
7 (* Date: Feb 14, 2010 *)
8 (* ========================================================================== *)
11 Deprecated Dec 28, 2011. Content moved to pack_concl.hl
13 The corresponding theorem for `voronoi_open` has been proved by Nguyen Tat Thang.
14 Hopefully, his proof can be adapted to this context.
16 The conclusion should be separated into three separate statements for useability.
21 module type Druqufe_type = sig
22 val DRUQUFE_concl : term
27 module Druqufe : Druqufe_type = struct
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)`;;