1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Local Fan *)
5 (* Author: Hoang Le Truong *)
7 (* ========================================================================= *)
11 remaining conclusions from appendix to Local Fan chapter
15 module Hxhytij = struct
27 open Wrgcvdr_cizmrrh;;
35 open Flyspeck_constants;;
51 open Wrgcvdr_cizmrrh;;
53 open Flyspeck_constants;;
79 let HXHYTIJ= prove_by_refinement(`!s vv ww.
83 (taustar_v39 s vv < taustar_v39 s ww \/
84 BBindex_v39 s vv <= BBindex_v39 s ww)`,
86 THEN MP_TAC(REAL_ARITH`(taustar_v39 s vv < taustar_v39 s ww)\/ taustar_v39 s ww <= taustar_v39 s vv`)
88 THEN SUBGOAL_THEN`BBprime_v39 s ww` ASSUME_TAC;
91 THEN ASM_REWRITE_TAC[IN;BBprime_v39;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39]
94 REPLICATE_TAC (7-2)(POP_ASSUM MP_TAC)
95 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
96 THEN MRESA1_TAC th`ww':num->real^3`)
97 THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC)
100 REPLICATE_TAC (6-2)(POP_ASSUM MP_TAC)
101 THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC
102 THEN MRESA1_TAC th`ww:num->real^3`)
107 THEN ASM_REWRITE_TAC[IN;BBprime2_v39;scs_v39_explicit;override;LET_DEF;LET_END_DEF;restriction_cs1_v39;BBindex_min_v39]
109 THEN SUBGOAL_THEN`(BBindex_v39 s ww) IN IMAGE (BBindex_v39 s) (BBprime_v39 s)` ASSUME_TAC;
111 REWRITE_TAC[IMAGE;IN_ELIM_THM;IN]
112 THEN EXISTS_TAC`ww:num->real^3`
113 THEN ASM_REWRITE_TAC[];
118 THEN MRESA_TAC Misc_defs_and_lemmas.min_least[`(IMAGE (BBindex_v39 s) (BBprime_v39 s))`;`BBindex_v39 s ww`]]);;
125 let check_completeness_claimA_concl =
126 Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x)