src/HOL/Filter.thy
changeset 60721 c1b7793c23a3
parent 60589 b5622eef7176
child 60752 b48830b670a1
     1.1 --- a/src/HOL/Filter.thy	Tue Jul 14 13:37:44 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Tue Jul 14 13:48:03 2015 +0200
     1.3 @@ -602,8 +602,10 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 -lemma eventually_gt_at_top:
     1.8 -  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"
     1.9 +lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
    1.10 +  unfolding eventually_at_top_dense by auto
    1.11 +
    1.12 +lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    1.13    unfolding eventually_at_top_dense by auto
    1.14  
    1.15  definition at_bot :: "('a::order) filter"
    1.16 @@ -631,6 +633,9 @@
    1.17    finally show ?thesis .
    1.18  qed
    1.19  
    1.20 +lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
    1.21 +  unfolding eventually_at_bot_dense by auto
    1.22 +
    1.23  lemma eventually_gt_at_bot:
    1.24    "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
    1.25    unfolding eventually_at_bot_dense by auto
    1.26 @@ -778,6 +783,21 @@
    1.27  lemma filtermap_eq_strong: "inj f \<Longrightarrow> filtermap f F = filtermap f G \<longleftrightarrow> F = G"
    1.28    by (simp add: filtermap_mono_strong eq_iff)
    1.29  
    1.30 +lemma filtermap_fun_inverse:
    1.31 +  assumes g: "filterlim g F G"
    1.32 +  assumes f: "filterlim f G F"
    1.33 +  assumes ev: "eventually (\<lambda>x. f (g x) = x) G"
    1.34 +  shows "filtermap f F = G"
    1.35 +proof (rule antisym)
    1.36 +  show "filtermap f F \<le> G"
    1.37 +    using f unfolding filterlim_def .
    1.38 +  have "G = filtermap f (filtermap g G)"
    1.39 +    using ev by (auto elim: eventually_elim2 simp: filter_eq_iff eventually_filtermap)
    1.40 +  also have "\<dots> \<le> filtermap f F"
    1.41 +    using g by (intro filtermap_mono) (simp add: filterlim_def)
    1.42 +  finally show "G \<le> filtermap f F" .
    1.43 +qed
    1.44 +
    1.45  lemma filterlim_principal:
    1.46    "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
    1.47    unfolding filterlim_def eventually_filtermap le_principal ..