equal
deleted
inserted
replaced
353 shows "Inf (insert a X) = (if X={} then a else min a (Inf X))" |
353 shows "Inf (insert a X) = (if X={} then a else min a (Inf X))" |
354 by auto (metis Inf_insert_nonempty z) |
354 by auto (metis Inf_insert_nonempty z) |
355 |
355 |
356 lemma Inf_greater: |
356 lemma Inf_greater: |
357 fixes z :: real |
357 fixes z :: real |
358 shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z" |
358 shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z" |
359 by (metis Inf_real_iff mem_def not_leE) |
359 by (metis Inf_real_iff mem_def not_leE) |
360 |
360 |
361 lemma Inf_close: |
361 lemma Inf_close: |
362 fixes e :: real |
362 fixes e :: real |
363 shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e" |
363 shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e" |
364 by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict) |
364 by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict) |
365 |
365 |
366 lemma Inf_finite_Min: |
366 lemma Inf_finite_Min: |
367 fixes S :: "real set" |
367 fixes S :: "real set" |
368 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S" |
368 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S" |
369 by (simp add: Inf_real_def Sup_finite_Max image_image) |
369 by (simp add: Inf_real_def Sup_finite_Max image_image) |
415 have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>" |
415 have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>" |
416 by auto |
416 by auto |
417 also have "... \<le> e" |
417 also have "... \<le> e" |
418 apply (rule Sup_asclose) |
418 apply (rule Sup_asclose) |
419 apply (auto simp add: S) |
419 apply (auto simp add: S) |
420 apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) |
420 apply (metis abs_minus_add_cancel b add_commute real_diff_def) |
421 done |
421 done |
422 finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" . |
422 finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" . |
423 thus ?thesis |
423 thus ?thesis |
424 by (simp add: Inf_real_def) |
424 by (simp add: Inf_real_def) |
425 qed |
425 qed |