equal
deleted
inserted
replaced
2995 |
2995 |
2996 lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)" |
2996 lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: real set)" |
2997 by (auto simp: bounded_def bdd_below_def dist_real_def) |
2997 by (auto simp: bounded_def bdd_below_def dist_real_def) |
2998 (metis abs_le_D1 add.commute diff_le_eq) |
2998 (metis abs_le_D1 add.commute diff_le_eq) |
2999 |
2999 |
|
3000 lemma bounded_norm_le_SUP_norm: |
|
3001 "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))" |
|
3002 by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp) |
|
3003 |
3000 lemma bounded_has_Sup: |
3004 lemma bounded_has_Sup: |
3001 fixes S :: "real set" |
3005 fixes S :: "real set" |
3002 assumes "bounded S" |
3006 assumes "bounded S" |
3003 and "S \<noteq> {}" |
3007 and "S \<noteq> {}" |
3004 shows "\<forall>x\<in>S. x \<le> Sup S" |
3008 shows "\<forall>x\<in>S. x \<le> Sup S" |