equal
deleted
inserted
replaced
3435 using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] |
3435 using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] |
3436 by (auto intro!: exI[of _ "b + norm a"]) |
3436 by (auto intro!: exI[of _ "b + norm a"]) |
3437 qed |
3437 qed |
3438 |
3438 |
3439 lemma bounded_uminus [simp]: |
3439 lemma bounded_uminus [simp]: |
3440 fixes X :: "'a::euclidean_space set" |
3440 fixes X :: "'a::real_normed_vector set" |
3441 shows "bounded (uminus ` X) \<longleftrightarrow> bounded X" |
3441 shows "bounded (uminus ` X) \<longleftrightarrow> bounded X" |
3442 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute) |
3442 by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute) |
3443 |
3443 |
3444 |
3444 |
3445 text\<open>Some theorems on sups and infs using the notion "bounded".\<close> |
3445 text\<open>Some theorems on sups and infs using the notion "bounded".\<close> |