src/HOL/Filter.thy
changeset 60182 e1ea5a6379c9
parent 60040 1fa1023b13b9
child 60589 b5622eef7176
     1.1 --- a/src/HOL/Filter.thy	Wed May 06 15:04:38 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Thu May 07 15:34:28 2015 +0200
     1.3 @@ -822,6 +822,11 @@
     1.4  lemma filterlim_Suc: "filterlim Suc sequentially sequentially"
     1.5    by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)
     1.6  
     1.7 +lemma filterlim_If:
     1.8 +  "LIM x inf F (principal {x. P x}). f x :> G \<Longrightarrow>
     1.9 +    LIM x inf F (principal {x. \<not> P x}). g x :> G \<Longrightarrow>
    1.10 +    LIM x F. if P x then f x else g x :> G"
    1.11 +  unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
    1.12  
    1.13  subsection {* Limits to @{const at_top} and @{const at_bot} *}
    1.14