1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
7 (* Date: Feb 14, 2010 *)
8 (* ========================================================================== *)
14 There are two main separate conclusions
15 (1) The boundedness of the Voronoi cell
17 The statement of the lemma has been broken into substatements.
18 All statements need a proof.
20 Closely related theorems for `voronoi_open` have been proved by Thang. It might be possible
23 Deprecated Dec 28, 2011. Content moved to pack_concl.hl
28 module type Rhwvgnp_type = sig
29 val RHWVGNP_concl : term
30 val VORONOI_BALL2_concl : term
31 val VORONOI_INTER_BIS_LE_concl : term
32 val VORONOI_POLYHEDRON_concl : term
37 module Rhwvgnp : Rhwvgnp_type = struct
39 let VORONOI_BALL2_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==> voronoi_closed V v SUBSET ball(v, &2)`;;
41 let VORONOI_INTER_BIS_LE_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
42 (voronoi_closed V v =INTERS { bis_le v u | u IN V /\ u IN ball(v, &4) /\ ~(u=v) })`;;
44 let VORONOI_POLYHEDRON_concl = `!V (v:real^3). packing V /\ saturated V /\ (v IN V) ==>
45 polyhedron (voronoi_closed V v)`;;
47 let RHWVGNP_concl = VORONOI_POLYHEDRON_concl;;