equal
deleted
inserted
replaced
1627 fixes c :: ennreal |
1627 fixes c :: ennreal |
1628 shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c" |
1628 shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c" |
1629 apply transfer |
1629 apply transfer |
1630 apply (simp add: SUP_ereal_add_left) |
1630 apply (simp add: SUP_ereal_add_left) |
1631 apply (subst (1 2) max.absorb2) |
1631 apply (subst (1 2) max.absorb2) |
1632 apply (auto intro: SUP_upper2 ereal_add_nonneg_nonneg) |
1632 apply (auto intro: SUP_upper2 add_nonneg_nonneg) |
1633 done |
1633 done |
1634 |
1634 |
1635 lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *) |
1635 lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *) |
1636 fixes f :: "'a \<Rightarrow> ennreal" |
1636 fixes f :: "'a \<Rightarrow> ennreal" |
1637 shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)" |
1637 shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)" |
1812 lemma add_diff_eq_ennreal: |
1812 lemma add_diff_eq_ennreal: |
1813 fixes x y z :: ennreal |
1813 fixes x y z :: ennreal |
1814 shows "z \<le> y \<Longrightarrow> x + (y - z) = x + y - z" |
1814 shows "z \<le> y \<Longrightarrow> x + (y - z) = x + y - z" |
1815 including ennreal.lifting |
1815 including ennreal.lifting |
1816 by transfer |
1816 by transfer |
1817 (insert ereal_add_mono[of 0], auto simp add: ereal_diff_positive max.absorb2 add_diff_eq_ereal) |
1817 (insert add_mono[of "0::ereal"], auto simp add: ereal_diff_positive max.absorb2 add_diff_eq_ereal) |
1818 |
1818 |
1819 lemma add_diff_inverse_ennreal: |
1819 lemma add_diff_inverse_ennreal: |
1820 fixes x y :: ennreal shows "x \<le> y \<Longrightarrow> x + (y - x) = y" |
1820 fixes x y :: ennreal shows "x \<le> y \<Longrightarrow> x + (y - x) = y" |
1821 by (cases x) (simp_all add: top_unique add_diff_eq_ennreal) |
1821 by (cases x) (simp_all add: top_unique add_diff_eq_ennreal) |
1822 |
1822 |