legacy/oldlocal/ch_local/cyclic_definition.hl

   1
   2 (* called azim(x) in text *)
   3
   4 let define_latex (a,b,c) =
   5
   6
   7 let azimdart = define `azimdart (V,E) (v,w) =
   8     azim (vec 0) v w (sigma_fan (vec 0) V E v w)`;;
   9
  10
  11 let cyclic_fan =  `cyclic_fan (V,E,F1) =
  12     FANO(V,E) /\
  13     face_set (hyp_of_fano(V,E)) F1 /\
  14     (!x.  (F1 x) ==> azimdart (V,E) x <= pi)
  15
  16 `;;