Lines Matching defs:inf
597 val inf = new_definition ("inf",
598 ``inf s = @a:real. (!x. x IN s ==> a <= x) /\
603 ==> (inf s = inf t)``,
604 SIMP_TAC std_ss [inf]);
608 ==> (!x. x IN s ==> inf s <= x) /\
609 !b. (!x. x IN s ==> b <= x) ==> b <= inf s``,
610 GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[inf] THEN
631 ``!s. FINITE s /\ ~(s = {}) ==> (inf s) IN s /\ !x. x IN s ==> inf s <= x``,
637 ``!s a:real. FINITE s /\ ~(s = {}) ==> (a <= inf s <=> !x. x IN s ==> a <= x)``,
641 ``!s a:real. FINITE s /\ ~(s = {}) ==> (inf s <= a <=> ?x. x IN s /\ x <= a)``,
645 ``!s a:real. FINITE s /\ ~(s = {}) ==> (a < inf s <=> !x. x IN s ==> a < x)``,
649 ``!s a:real. FINITE s /\ ~(s = {}) ==> (inf s < a <=> ?x. x IN s /\ x < a)``,
655 ==> (inf s = b)``,
656 REPEAT STRIP_TAC THEN REWRITE_TAC[inf] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
660 ``!b:real. ~(s = {}) /\ (!x. x IN s ==> b <= x) ==> b <= inf s``,
665 ==> inf s <= inf t``,
671 ==> a <= inf s /\ inf s <= b``,
681 ``!s a:real. ~(s = {}) /\ (!x. x IN s ==> abs(x) <= a) ==> abs(inf s) <= a``,
686 ==> abs(inf s - l) <= e``,
699 ==> ((inf s = a) <=> a IN s /\ !y. y IN s ==> a <= y)``,
715 ``!x s:real->bool. FINITE s ==> (inf(x INSERT s) = if s = {} then x else min x (inf s))``,
726 ==> ((sup s = inf s) <=> ?a. s = {a})``,
736 ``!a. inf {a} = a``,