equal
deleted
inserted
replaced
1880 using * by (force simp: top_ereal_def) |
1880 using * by (force simp: top_ereal_def) |
1881 then show "bdd_below A" "A \<noteq> {}" |
1881 then show "bdd_below A" "A \<noteq> {}" |
1882 by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq) |
1882 by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq) |
1883 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal) |
1883 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal) |
1884 |
1884 |
|
1885 lemma ereal_Inf': |
|
1886 assumes *: "bdd_below A" "A \<noteq> {}" |
|
1887 shows "ereal (Inf A) = (INF a:A. ereal a)" |
|
1888 proof (rule ereal_Inf) |
|
1889 from * obtain l u where "\<And>x. x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" |
|
1890 by (auto simp: bdd_below_def) |
|
1891 then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u" |
|
1892 by (auto intro!: INF_greatest INF_lower) |
|
1893 then show "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>" |
|
1894 by auto |
|
1895 qed |
|
1896 |
1885 lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))" |
1897 lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))" |
1886 using ereal_Inf[of "f`A"] by auto |
1898 using ereal_Inf[of "f`A"] by auto |
1887 |
1899 |
1888 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S" |
1900 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S" |
1889 by (auto intro!: SUP_eqI |
1901 by (auto intro!: SUP_eqI |