1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
7 (* Date: Feb 14, 2010 *)
8 (* ========================================================================== *)
14 R^3 is the union of Voronoi cells.
16 We write this in pointwise form: for every p IN R^3, there exists a cell to which it belongs.
18 Deprecated, Dec 28 2011. Content moved to pack_con.hl.
23 module type Tiwwfyq_def_type = sig
24 val TIWWFYQ_concl : term
26 (* val TIWWFYQ : thm *)
32 module Tiwwfyq : Tiwwfyq_def_type = struct
34 let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v. v IN V /\ p IN voronoi_closed V v)`;;