src/HOL/Topological_Spaces.thy
changeset 56949 d1a937cbf858
parent 56524 f4ba736040fa
child 57025 e7fd64f82876
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue May 13 11:11:51 2014 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue May 13 11:35:47 2014 +0200
     1.3 @@ -973,6 +973,41 @@
     1.4  lemma tendsto_bot [simp]: "(f ---> a) bot"
     1.5    unfolding tendsto_def by simp
     1.6  
     1.7 +lemma tendsto_max:
     1.8 +  fixes x y :: "'a::linorder_topology"
     1.9 +  assumes X: "(X ---> x) net"
    1.10 +  assumes Y: "(Y ---> y) net"
    1.11 +  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
    1.12 +proof (rule order_tendstoI)
    1.13 +  fix a assume "a < max x y"
    1.14 +  then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
    1.15 +    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
    1.16 +    by (auto simp: less_max_iff_disj elim: eventually_elim1)
    1.17 +next
    1.18 +  fix a assume "max x y < a"
    1.19 +  then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
    1.20 +    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
    1.21 +    by (auto simp: eventually_conj_iff)
    1.22 +qed
    1.23 +
    1.24 +lemma tendsto_min:
    1.25 +  fixes x y :: "'a::linorder_topology"
    1.26 +  assumes X: "(X ---> x) net"
    1.27 +  assumes Y: "(Y ---> y) net"
    1.28 +  shows "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
    1.29 +proof (rule order_tendstoI)
    1.30 +  fix a assume "a < min x y"
    1.31 +  then show "eventually (\<lambda>x. a < min (X x) (Y x)) net"
    1.32 +    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
    1.33 +    by (auto simp: eventually_conj_iff)
    1.34 +next
    1.35 +  fix a assume "min x y < a"
    1.36 +  then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
    1.37 +    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
    1.38 +    by (auto simp: min_less_iff_disj elim: eventually_elim1)
    1.39 +qed
    1.40 +
    1.41 +
    1.42  lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
    1.43    unfolding tendsto_def eventually_at_topological by auto
    1.44