(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Lemma: TIWWFYQ                                                             *)
(* Chapter: Packing                                                           *)
(* Author: Thomas C. Hales                                                    *)
(* Date: Feb 14, 2010                                                         *)
(* ========================================================================== *)




(*
R^3 is the union of Voronoi cells.

We write this in pointwise form: for every p IN R^3, there exists a cell to which it belongs.

Deprecated, Dec 28 2011.  Content moved to pack_con.hl.
*)



module type Tiwwfyq_def_type = sig
  val TIWWFYQ_concl : term

(* val TIWWFYQ : thm *)

end;;



module Tiwwfyq : Tiwwfyq_def_type = struct

 let TIWWFYQ_concl = `!V (p:real^3). packing V /\ saturated V ==> (?v.  v IN V /\ p IN voronoi_closed V v)`;;

end;;