src/HOL/Library/Extended_Real.thy

     | (MInf) "x = -\<infinity>"
   using assms by (cases x) auto
 
 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
+
+lemma ereal_all_split: "\<And>P. (\<forall>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<and> (\<forall>x. P (ereal x)) \<and> P (-\<infinity>)"
+  by (metis ereal_cases)
+
+lemma ereal_ex_split: "\<And>P. (\<exists>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<or> (\<exists>x. P (ereal x)) \<or> P (-\<infinity>)"
+  by (metis ereal_cases)
 
 lemma ereal_uminus_eq_iff[simp]:
   fixes a b :: ereal
   shows "-a = -b \<longleftrightarrow> a = b"
   by (cases rule: ereal2_cases[of a b]) simp_all

   with that[of "x - e" "x + e"] ereal_between[OF x, of e]
   show thesis
     by auto
 qed
 
-
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
   (is "?l = ?r")
 proof (intro iffI topological_tendstoI)