(* Title: HOL/Topological_Spaces.thy Author: Brian Huffman Author: Johannes Hölzl *) section ‹Topological Spaces› theory Topological_Spaces imports Main begin named_theorems continuous_intros "structural introduction rules for continuity" subsection ‹Topological space› class "open" = fixes "open" :: "'a set ⇒ bool" class topological_space = "open" + assumes open_UNIV [simp, intro]: "open UNIV" assumes open_Int [intro]: "open S ⟹ open T ⟹ open (S ∩ T)" assumes open_Union [intro]: "∀S∈K. open S ⟹ open (⋃K)" begin definition closed :: "'a set ⇒ bool" where "closed S ⟷ open (- S)" lemma open_empty [continuous_intros, intro, simp]: "open {}" using open_Union [of "{}"] by simp lemma open_Un [continuous_intros, intro]: "open S ⟹ open T ⟹ open (S ∪ T)" using open_Union [of "{S, T}"] by simp lemma open_UN [continuous_intros, intro]: "∀x∈A. open (B x) ⟹ open (⋃x∈A. B x)" using open_Union [of "B ` A"] by simp lemma open_Inter [continuous_intros, intro]: "finite S ⟹ ∀T∈S. open T ⟹ open (⋂S)" by (induction set: finite) auto lemma open_INT [continuous_intros, intro]: "finite A ⟹ ∀x∈A. open (B x) ⟹ open (⋂x∈A. B x)" using open_Inter [of "B ` A"] by simp lemma openI: assumes "⋀x. x ∈ S ⟹ ∃T. open T ∧ x ∈ T ∧ T ⊆ S" shows "open S" proof - have "open (⋃{T. open T ∧ T ⊆ S})" by auto moreover have "⋃{T. open T ∧ T ⊆ S} = S" by (auto dest!: assms) ultimately show "open S" by simp qed lemma open_subopen: "open S ⟷ (∀x∈S. ∃T. open T ∧ x ∈ T ∧ T ⊆ S)" by (auto intro: openI) lemma closed_empty [continuous_intros, intro, simp]: "closed {}" unfolding closed_def by simp lemma closed_Un [continuous_intros, intro]: "closed S ⟹ closed T ⟹ closed (S ∪ T)" unfolding closed_def by auto lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV" unfolding closed_def by simp lemma closed_Int [continuous_intros, intro]: "closed S ⟹ closed T ⟹ closed (S ∩ T)" unfolding closed_def by auto lemma closed_INT [continuous_intros, intro]: "∀x∈A. closed (B x) ⟹ closed (⋂x∈A. B x)" unfolding closed_def by auto lemma closed_Inter [continuous_intros, intro]: "∀S∈K. closed S ⟹ closed (⋂K)" unfolding closed_def uminus_Inf by auto lemma closed_Union [continuous_intros, intro]: "finite S ⟹ ∀T∈S. closed T ⟹ closed (⋃S)" by (induct set: finite) auto lemma closed_UN [continuous_intros, intro]: "finite A ⟹ ∀x∈A. closed (B x) ⟹ closed (⋃x∈A. B x)" using closed_Union [of "B ` A"] by simp lemma open_closed: "open S ⟷ closed (- S)" by (simp add: closed_def) lemma closed_open: "closed S ⟷ open (- S)" by (rule closed_def) lemma open_Diff [continuous_intros, intro]: "open S ⟹ closed T ⟹ open (S - T)" by (simp add: closed_open Diff_eq open_Int) lemma closed_Diff [continuous_intros, intro]: "closed S ⟹ open T ⟹ closed (S - T)" by (simp add: open_closed Diff_eq closed_Int) lemma open_Compl [continuous_intros, intro]: "closed S ⟹ open (- S)" by (simp add: closed_open) lemma closed_Compl [continuous_intros, intro]: "open S ⟹ closed (- S)" by (simp add: open_closed) lemma open_Collect_neg: "closed {x. P x} ⟹ open {x. ¬ P x}" unfolding Collect_neg_eq by (rule open_Compl) lemma open_Collect_conj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x ∧ Q x}" using open_Int[OF assms] by (simp add: Int_def) lemma open_Collect_disj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x ∨ Q x}" using open_Un[OF assms] by (simp add: Un_def) lemma open_Collect_ex: "(⋀i. open {x. P i x}) ⟹ open {x. ∃i. P i x}" using open_UN[of UNIV "λi. {x. P i x}"] unfolding Collect_ex_eq by simp lemma open_Collect_imp: "closed {x. P x} ⟹ open {x. Q x} ⟹ open {x. P x ⟶ Q x}" unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg) lemma open_Collect_const: "open {x. P}" by (cases P) auto lemma closed_Collect_neg: "open {x. P x} ⟹ closed {x. ¬ P x}" unfolding Collect_neg_eq by (rule closed_Compl) lemma closed_Collect_conj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x ∧ Q x}" using closed_Int[OF assms] by (simp add: Int_def) lemma closed_Collect_disj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x ∨ Q x}" using closed_Un[OF assms] by (simp add: Un_def) lemma closed_Collect_all: "(⋀i. closed {x. P i x}) ⟹ closed {x. ∀i. P i x}" using closed_INT[of UNIV "λi. {x. P i x}"] by (simp add: Collect_all_eq) lemma closed_Collect_imp: "open {x. P x} ⟹ closed {x. Q x} ⟹ closed {x. P x ⟶ Q x}" unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg) lemma closed_Collect_const: "closed {x. P}" by (cases P) auto end subsection ‹Hausdorff and other separation properties› class t0_space = topological_space + assumes t0_space: "x ≠ y ⟹ ∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U)" class t1_space = topological_space + assumes t1_space: "x ≠ y ⟹ ∃U. open U ∧ x ∈ U ∧ y ∉ U" instance t1_space ⊆ t0_space by standard (fast dest: t1_space) context t1_space begin lemma separation_t1: "x ≠ y ⟷ (∃U. open U ∧ x ∈ U ∧ y ∉ U)" using t1_space[of x y] by blast lemma closed_singleton [iff]: "closed {a}" proof - let ?T = "⋃{S. open S ∧ a ∉ S}" have "open ?T" by (simp add: open_Union) also have "?T = - {a}" by (auto simp add: set_eq_iff separation_t1) finally show "closed {a}" by (simp only: closed_def) qed lemma closed_insert [continuous_intros, simp]: assumes "closed S" shows "closed (insert a S)" proof - from closed_singleton assms have "closed ({a} ∪ S)" by (rule closed_Un) then show "closed (insert a S)" by simp qed lemma finite_imp_closed: "finite S ⟹ closed S" by (induct pred: finite) simp_all end text ‹T2 spaces are also known as Hausdorff spaces.› class t2_space = topological_space + assumes hausdorff: "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}" instance t2_space ⊆ t1_space by standard (fast dest: hausdorff) lemma (in t2_space) separation_t2: "x ≠ y ⟷ (∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {})" using hausdorff [of x y] by blast lemma (in t0_space) separation_t0: "x ≠ y ⟷ (∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U))" using t0_space [of x y] by blast text ‹A classical separation axiom for topological space, the T3 axiom -- also called regularity: if a point is not in a closed set, then there are open sets separating them.› class t3_space = t2_space + assumes t3_space: "closed S ⟹ y ∉ S ⟹ ∃U V. open U ∧ open V ∧ y ∈ U ∧ S ⊆ V ∧ U ∩ V = {}" text ‹A classical separation axiom for topological space, the T4 axiom -- also called normality: if two closed sets are disjoint, then there are open sets separating them.› class t4_space = t2_space + assumes t4_space: "closed S ⟹ closed T ⟹ S ∩ T = {} ⟹ ∃U V. open U ∧ open V ∧ S ⊆ U ∧ T ⊆ V ∧ U ∩ V = {}" text ‹T4 is stronger than T3, and weaker than metric.› instance t4_space ⊆ t3_space proof fix S and y::'a assume "closed S" "y ∉ S" then show "∃U V. open U ∧ open V ∧ y ∈ U ∧ S ⊆ V ∧ U ∩ V = {}" using t4_space[of "{y}" S] by auto qed text ‹A perfect space is a topological space with no isolated points.› class perfect_space = topological_space + assumes not_open_singleton: "¬ open {x}" lemma (in perfect_space) UNIV_not_singleton: "UNIV ≠ {x}" for x::'a by (metis (no_types) open_UNIV not_open_singleton) subsection ‹Generators for toplogies› inductive generate_topology :: "'a set set ⇒ 'a set ⇒ bool" for S :: "'a set set" where UNIV: "generate_topology S UNIV" | Int: "generate_topology S (a ∩ b)" if "generate_topology S a" and "generate_topology S b" | UN: "generate_topology S (⋃K)" if "(⋀k. k ∈ K ⟹ generate_topology S k)" | Basis: "generate_topology S s" if "s ∈ S" hide_fact (open) UNIV Int UN Basis lemma generate_topology_Union: "(⋀k. k ∈ I ⟹ generate_topology S (K k)) ⟹ generate_topology S (⋃k∈I. K k)" using generate_topology.UN [of "K ` I"] by auto lemma topological_space_generate_topology: "class.topological_space (generate_topology S)" by standard (auto intro: generate_topology.intros) subsection ‹Order topologies› class order_topology = order + "open" + assumes open_generated_order: "open = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))" begin subclass topological_space unfolding open_generated_order by (rule topological_space_generate_topology) lemma open_greaterThan [continuous_intros, simp]: "open {a <..}" unfolding open_generated_order by (auto intro: generate_topology.Basis) lemma open_lessThan [continuous_intros, simp]: "open {..< a}" unfolding open_generated_order by (auto intro: generate_topology.Basis) lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}" unfolding greaterThanLessThan_eq by (simp add: open_Int) end class linorder_topology = linorder + order_topology lemma closed_atMost [continuous_intros, simp]: "closed {..a}" for a :: "'a::linorder_topology" by (simp add: closed_open) lemma closed_atLeast [continuous_intros, simp]: "closed {a..}" for a :: "'a::linorder_topology" by (simp add: closed_open) lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}" for a b :: "'a::linorder_topology" proof - have "{a .. b} = {a ..} ∩ {.. b}" by auto then show ?thesis by (simp add: closed_Int) qed lemma (in order) less_separate: assumes "x < y" shows "∃a b. x ∈ {..< a} ∧ y ∈ {b <..} ∧ {..< a} ∩ {b <..} = {}" proof (cases "∃z. x < z ∧ z < y") case True then obtain z where "x < z ∧ z < y" .. then have "x ∈ {..< z} ∧ y ∈ {z <..} ∧ {z <..} ∩ {..< z} = {}" by auto then show ?thesis by blast next case False with ‹x < y› have "x ∈ {..< y}" "y ∈ {x <..}" "{x <..} ∩ {..< y} = {}" by auto then show ?thesis by blast qed instance linorder_topology ⊆ t2_space proof fix x y :: 'a show "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}" using less_separate [of x y] less_separate [of y x] by (elim neqE; metis open_lessThan open_greaterThan Int_commute) qed lemma (in linorder_topology) open_right: assumes "open S" "x ∈ S" and gt_ex: "x < y" shows "∃b>x. {x ..< b} ⊆ S" using assms unfolding open_generated_order proof induct case UNIV then show ?case by blast next case (Int A B) then obtain a b where "a > x" "{x ..< a} ⊆ A" "b > x" "{x ..< b} ⊆ B" by auto then show ?case by (auto intro!: exI[of _ "min a b"]) next case UN then show ?case by blast next case Basis then show ?case by (fastforce intro: exI[of _ y] gt_ex) qed lemma (in linorder_topology) open_left: assumes "open S" "x ∈ S" and lt_ex: "y < x" shows "∃b<x. {b <.. x} ⊆ S" using assms unfolding open_generated_order proof induction case UNIV then show ?case by blast next case (Int A B) then obtain a b where "a < x" "{a <.. x} ⊆ A" "b < x" "{b <.. x} ⊆ B" by auto then show ?case by (auto intro!: exI[of _ "max a b"]) next case UN then show ?case by blast next case Basis then show ?case by (fastforce intro: exI[of _ y] lt_ex) qed subsection ‹Setup some topologies› subsubsection ‹Boolean is an order topology› class discrete_topology = topological_space + assumes open_discrete: "⋀A. open A" instance discrete_topology < t2_space proof fix x y :: 'a assume "x ≠ y" then show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}" by (intro exI[of _ "{_}"]) (auto intro!: open_discrete) qed instantiation bool :: linorder_topology begin definition open_bool :: "bool set ⇒ bool" where "open_bool = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))" instance by standard (rule open_bool_def) end instance bool :: discrete_topology proof fix A :: "bool set" have *: "{False <..} = {True}" "{..< True} = {False}" by auto have "A = UNIV ∨ A = {} ∨ A = {False <..} ∨ A = {..< True}" using subset_UNIV[of A] unfolding UNIV_bool * by blast then show "open A" by auto qed instantiation nat :: linorder_topology begin definition open_nat :: "nat set ⇒ bool" where "open_nat = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))" instance by standard (rule open_nat_def) end instance nat :: discrete_topology proof fix A :: "nat set" have "open {n}" for n :: nat proof (cases n) case 0 moreover have "{0} = {..<1::nat}" by auto ultimately show ?thesis by auto next case (Suc n') then have "{n} = {..<Suc n} ∩ {n' <..}" by auto with Suc show ?thesis by (auto intro: open_lessThan open_greaterThan) qed then have "open (⋃a∈A. {a})" by (intro open_UN) auto then show "open A" by simp qed instantiation int :: linorder_topology begin definition open_int :: "int set ⇒ bool" where "open_int = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))" instance by standard (rule open_int_def) end instance int :: discrete_topology proof fix A :: "int set" have "{..<i + 1} ∩ {i-1 <..} = {i}" for i :: int by auto then have "open {i}" for i :: int using open_Int[OF open_lessThan[of "i + 1"] open_greaterThan[of "i - 1"]] by auto then have "open (⋃a∈A. {a})" by (intro open_UN) auto then show "open A" by simp qed subsubsection ‹Topological filters› definition (in topological_space) nhds :: "'a ⇒ 'a filter" where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)" definition (in topological_space) at_within :: "'a ⇒ 'a set ⇒ 'a filter" ("at (_)/ within (_)" [1000, 60] 60) where "at a within s = inf (nhds a) (principal (s - {a}))" abbreviation (in topological_space) at :: "'a ⇒ 'a filter" ("at") where "at x ≡ at x within (CONST UNIV)" abbreviation (in order_topology) at_right :: "'a ⇒ 'a filter" where "at_right x ≡ at x within {x <..}" abbreviation (in order_topology) at_left :: "'a ⇒ 'a filter" where "at_left x ≡ at x within {..< x}" lemma (in topological_space) nhds_generated_topology: "open = generate_topology T ⟹ nhds x = (INF S∈{S∈T. x ∈ S}. principal S)" unfolding nhds_def proof (safe intro!: antisym INF_greatest) fix S assume "generate_topology T S" "x ∈ S" then show "(INF S∈{S ∈ T. x ∈ S}. principal S) ≤ principal S" by induct (auto intro: INF_lower order_trans simp: inf_principal[symmetric] simp del: inf_principal) qed (auto intro!: INF_lower intro: generate_topology.intros) lemma (in topological_space) eventually_nhds: "eventually P (nhds a) ⟷ (∃S. open S ∧ a ∈ S ∧ (∀x∈S. P x))" unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal) lemma eventually_eventually: "eventually (λy. eventually P (nhds y)) (nhds x) = eventually P (nhds x)" by (auto simp: eventually_nhds) lemma (in topological_space) eventually_nhds_in_open: "open s ⟹ x ∈ s ⟹ eventually (λy. y ∈ s) (nhds x)" by (subst eventually_nhds) blast lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) ⟹ P x" by (subst (asm) eventually_nhds) blast lemma (in topological_space) nhds_neq_bot [simp]: "nhds a ≠ bot" by (simp add: trivial_limit_def eventually_nhds) lemma (in t1_space) t1_space_nhds: "x ≠ y ⟹ (∀⇩_{F}x in nhds x. x ≠ y)" by (drule t1_space) (auto simp: eventually_nhds) lemma (in topological_space) nhds_discrete_open: "open {x} ⟹ nhds x = principal {x}" by (auto simp: nhds_def intro!: antisym INF_greatest INF_lower2[of "{x}"]) lemma (in discrete_topology) nhds_discrete: "nhds x = principal {x}" by (simp add: nhds_discrete_open open_discrete) lemma (in discrete_topology) at_discrete: "at x within S = bot" unfolding at_within_def nhds_discrete by simp lemma (in discrete_topology) tendsto_discrete: "filterlim (f :: 'b ⇒ 'a) (nhds y) F ⟷ eventually (λx. f x = y) F" by (auto simp: nhds_discrete filterlim_principal) lemma (in topological_space) at_within_eq: "at x within s = (INF S∈{S. open S ∧ x ∈ S}. principal (S ∩ s - {x}))" unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib) lemma (in topological_space) eventually_at_filter: "eventually P (at a within s) ⟷ eventually (λx. x ≠ a ⟶ x ∈ s ⟶ P x) (nhds a)" by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute) lemma (in topological_space) at_le: "s ⊆ t ⟹ at x within s ≤ at x within t" unfolding at_within_def by (intro inf_mono) auto lemma (in topological_space) eventually_at_topological: "eventually P (at a within s) ⟷ (∃S. open S ∧ a ∈ S ∧ (∀x∈S. x ≠ a ⟶ x ∈ s ⟶ P x))" by (simp add: eventually_nhds eventually_at_filter) lemma (in topological_space) at_within_open: "a ∈ S ⟹ open S ⟹ at a within S = at a" unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I) lemma (in topological_space) at_within_open_NO_MATCH: "a ∈ s ⟹ open s ⟹ NO_MATCH UNIV s ⟹ at a within s = at a" by (simp only: at_within_open) lemma (in topological_space) at_within_open_subset: "a ∈ S ⟹ open S ⟹ S ⊆ T ⟹ at a within T = at a" by (metis at_le at_within_open dual_order.antisym subset_UNIV) lemma (in topological_space) at_within_nhd: assumes "x ∈ S" "open S" "T ∩ S - {x} = U ∩ S - {x}" shows "at x within T = at x within U" unfolding filter_eq_iff eventually_at_filter proof (intro allI eventually_subst) have "eventually (λx. x ∈ S) (nhds x)" using ‹x ∈ S› ‹open S› by (auto simp: eventually_nhds) then show "∀⇩_{F}n in nhds x. (n ≠ x ⟶ n ∈ T ⟶ P n) = (n ≠ x ⟶ n ∈ U ⟶ P n)" for P by eventually_elim (insert ‹T ∩ S - {x} = U ∩ S - {x}›, blast) qed lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot" unfolding at_within_def by simp lemma (in topological_space) at_within_union: "at x within (S ∪ T) = sup (at x within S) (at x within T)" unfolding filter_eq_iff eventually_sup eventually_at_filter by (auto elim!: eventually_rev_mp) lemma (in topological_space) at_eq_bot_iff: "at a = bot ⟷ open {a}" unfolding trivial_limit_def eventually_at_topological by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff) lemma (in perfect_space) at_neq_bot [simp]: "at a ≠ bot" by (simp add: at_eq_bot_iff not_open_singleton) lemma (in order_topology) nhds_order: "nhds x = inf (INF a∈{x <..}. principal {..< a}) (INF a∈{..< x}. principal {a <..})" proof - have 1: "{S ∈ range lessThan ∪ range greaterThan. x ∈ S} = (λa. {..< a}) ` {x <..} ∪ (λa. {a <..}) ` {..< x}" by auto show ?thesis by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def) qed lemma (in topological_space) filterlim_at_within_If: assumes "filterlim f G (at x within (A ∩ {x. P x}))" and "filterlim g G (at x within (A ∩ {x. ¬P x}))" shows "filterlim (λx. if P x then f x else g x) G (at x within A)" proof (rule filterlim_If) note assms(1) also have "at x within (A ∩ {x. P x}) = inf (nhds x) (principal (A ∩ Collect P - {x}))" by (simp add: at_within_def) also have "A ∩ Collect P - {x} = (A - {x}) ∩ Collect P" by blast also have "inf (nhds x) (principal …) = inf (at x within A) (principal (Collect P))" by (simp add: at_within_def inf_assoc) finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" . next note assms(2) also have "at x within (A ∩ {x. ¬ P x}) = inf (nhds x) (principal (A ∩ {x. ¬ P x} - {x}))" by (simp add: at_within_def) also have "A ∩ {x. ¬ P x} - {x} = (A - {x}) ∩ {x. ¬ P x}" by blast also have "inf (nhds x) (principal …) = inf (at x within A) (principal {x. ¬ P x})" by (simp add: at_within_def inf_assoc) finally show "filterlim g G (inf (at x within A) (principal {x. ¬ P x}))" . qed lemma (in topological_space) filterlim_at_If: assumes "filterlim f G (at x within {x. P x})" and "filterlim g G (at x within {x. ¬P x})" shows "filterlim (λx. if P x then f x else g x) G (at x)" using assms by (intro filterlim_at_within_If) simp_all lemma (in linorder_topology) at_within_order: assumes "UNIV ≠ {x}" shows "at x within s = inf (INF a∈{x <..}. principal ({..< a} ∩ s - {x})) (INF a∈{..< x}. principal ({a <..} ∩ s - {x}))" proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split]) case True_True have "UNIV = {..< x} ∪ {x} ∪ {x <..}" by auto with assms True_True show ?thesis by auto qed (auto simp del: inf_principal simp: at_within_def nhds_order Int_Diff inf_principal[symmetric] INF_inf_const2 inf_sup_aci[where 'a="'a filter"]) lemma (in linorder_topology) at_left_eq: "y < x ⟹ at_left x = (INF a∈{..< x}. principal {a <..< x})" by (subst at_within_order) (auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant intro!: INF_lower2 inf_absorb2) lemma (in linorder_topology) eventually_at_left: "y < x ⟹ eventually P (at_left x) ⟷ (∃b<x. ∀y>b. y < x ⟶ P y)" unfolding at_left_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def) lemma (in linorder_topology) at_right_eq: "x < y ⟹ at_right x = (INF a∈{x <..}. principal {x <..< a})" by (subst at_within_order) (auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute intro!: INF_lower2 inf_absorb1) lemma (in linorder_topology) eventually_at_right: "x < y ⟹ eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y < b ⟶ P y)" unfolding at_right_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def) lemma eventually_at_right_less: "∀⇩_{F}y in at_right (x::'a::{linorder_topology, no_top}). x < y" using gt_ex[of x] eventually_at_right[of x] by auto lemma trivial_limit_at_right_top: "at_right (top::_::{order_top,linorder_topology}) = bot" by (auto simp: filter_eq_iff eventually_at_topological) lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot,linorder_topology}) = bot" by (auto simp: filter_eq_iff eventually_at_topological) lemma trivial_limit_at_left_real [simp]: "¬ trivial_limit (at_left x)" for x :: "'a::{no_bot,dense_order,linorder_topology}" using lt_ex [of x] by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense) lemma trivial_limit_at_right_real [simp]: "¬ trivial_limit (at_right x)" for x :: "'a::{no_top,dense_order,linorder_topology}" using gt_ex[of x] by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense) lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)" by (auto simp: eventually_at_filter filter_eq_iff eventually_sup elim: eventually_elim2 eventually_mono) lemma (in linorder_topology) eventually_at_split: "eventually P (at x) ⟷ eventually P (at_left x) ∧ eventually P (at_right x)" by (subst at_eq_sup_left_right) (simp add: eventually_sup) lemma (in order_topology) eventually_at_leftI: assumes "⋀x. x ∈ {a<..<b} ⟹ P x" "a < b" shows "eventually P (at_left b)" using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto lemma (in order_topology) eventually_at_rightI: assumes "⋀x. x ∈ {a<..<b} ⟹ P x" "a < b" shows "eventually P (at_right a)" using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto lemma eventually_filtercomap_nhds: "eventually P (filtercomap f (nhds x)) ⟷ (∃S. open S ∧ x ∈ S ∧ (∀x. f x ∈ S ⟶ P x))" unfolding eventually_filtercomap eventually_nhds by auto lemma eventually_filtercomap_at_topological: "eventually P (filtercomap f (at A within B)) ⟷ (∃S. open S ∧ A ∈ S ∧ (∀x. f x ∈ S ∩ B - {A} ⟶ P x))" (is "?lhs = ?rhs") unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal eventually_filtercomap_nhds eventually_principal by blast lemma eventually_at_right_field: "eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y < b ⟶ P y)" for x :: "'a::{linordered_field, linorder_topology}" using linordered_field_no_ub[rule_format, of x] by (auto simp: eventually_at_right) lemma eventually_at_left_field: "eventually P (at_left x) ⟷ (∃b<x. ∀y>b. y < x ⟶ P y)" for x :: "'a::{linordered_field, linorder_topology}" using linordered_field_no_lb[rule_format, of x] by (auto simp: eventually_at_left) subsubsection ‹Tendsto› abbreviation (in topological_space) tendsto :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b filter ⇒ bool" (infixr "⤏" 55) where "(f ⤏ l) F ≡ filterlim f (nhds l) F" definition (in t2_space) Lim :: "'f filter ⇒ ('f ⇒ 'a) ⇒ 'a" where "Lim A f = (THE l. (f ⤏ l) A)" lemma (in topological_space) tendsto_eq_rhs: "(f ⤏ x) F ⟹ x = y ⟹ (f ⤏ y) F" by simp named_theorems tendsto_intros "introduction rules for tendsto" setup ‹ Global_Theory.add_thms_dynamic (\<^binding>‹tendsto_eq_intros›, fn context => Named_Theorems.get (Context.proof_of context) \<^named_theorems>‹tendsto_intros› |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm]))) › context topological_space begin lemma tendsto_def: "(f ⤏ l) F ⟷ (∀S. open S ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) F)" unfolding nhds_def filterlim_INF filterlim_principal by auto lemma tendsto_cong: "(f ⤏ c) F ⟷ (g ⤏ c) F" if "eventually (λx. f x = g x) F" by (rule filterlim_cong [OF refl refl that]) lemma tendsto_mono: "F ≤ F' ⟹ (f ⤏ l) F' ⟹ (f ⤏ l) F" unfolding tendsto_def le_filter_def by fast lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((λx. x) ⤏ a) (at a within s)" by (auto simp: tendsto_def eventually_at_topological) lemma tendsto_const [tendsto_intros, simp, intro]: "((λx. k) ⤏ k) F" by (simp add: tendsto_def) lemma filterlim_at: "(LIM x F. f x :> at b within s) ⟷ eventually (λx. f x ∈ s ∧ f x ≠ b) F ∧ (f ⤏ b) F" by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute) lemma (in -) assumes "filterlim f (nhds L) F" shows tendsto_imp_filterlim_at_right: "eventually (λx. f x > L) F ⟹ filterlim f (at_right L) F" and tendsto_imp_filterlim_at_left: "eventually (λx. f x < L) F ⟹ filterlim f (at_left L) F" using assms by (auto simp: filterlim_at elim: eventually_mono) lemma filterlim_at_withinI: assumes "filterlim f (nhds c) F" assumes "eventually (λx. f x ∈ A - {c}) F" shows "filterlim f (at c within A) F" using assms by (simp add: filterlim_at) lemma filterlim_atI: assumes "filterlim f (nhds c) F" assumes "eventually (λx. f x ≠ c) F" shows "filterlim f (at c) F" using assms by (intro filterlim_at_withinI) simp_all lemma topological_tendstoI: "(⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F) ⟹ (f ⤏ l) F" by (auto simp: tendsto_def) lemma topological_tendstoD: "(f ⤏ l) F ⟹ open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F" by (auto simp: tendsto_def) lemma tendsto_bot [simp]: "(f ⤏ a) bot" by (simp add: tendsto_def) lemma tendsto_eventually: "eventually (λx. f x = l) net ⟹ ((λx. f x) ⤏ l) net" by (rule topological_tendstoI) (auto elim: eventually_mono) (* Contributed by Dominique Unruh *) lemma tendsto_principal_singleton[simp]: shows "(f ⤏ f x) (principal {x})" unfolding tendsto_def eventually_principal by simp end lemma (in topological_space) filterlim_within_subset: "filterlim f l (at x within S) ⟹ T ⊆ S ⟹ filterlim f l (at x within T)" by (blast intro: filterlim_mono at_le) lemmas tendsto_within_subset = filterlim_within_subset lemma (in order_topology) order_tendsto_iff: "(f ⤏ x) F ⟷ (∀l<x. eventually (λx. l < f x) F) ∧ (∀u>x. eventually (λx. f x < u) F)" by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal) lemma (in order_topology) order_tendstoI: "(⋀a. a < y ⟹ eventually (λx. a < f x) F) ⟹ (⋀a. y < a ⟹ eventually (λx. f x < a) F) ⟹ (f ⤏ y) F" by (auto simp: order_tendsto_iff) lemma (in order_topology) order_tendstoD: assumes "(f ⤏ y) F" shows "a < y ⟹ eventually (λx. a < f x) F" and "y < a ⟹ eventually (λx. f x < a) F" using assms by (auto simp: order_tendsto_iff) lemma (in linorder_topology) tendsto_max[tendsto_intros]: assumes X: "(X ⤏ x) net" and Y: "(Y ⤏ y) net" shows "((λx. max (X x) (Y x)) ⤏ max x y) net" proof (rule order_tendstoI) fix a assume "a < max x y" then show "eventually (λx. a < max (X x) (Y x)) net" using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a] by (auto simp: less_max_iff_disj elim: eventually_mono) next fix a assume "max x y < a" then show "eventually (λx. max (X x) (Y x) < a) net" using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] by (auto simp: eventually_conj_iff) qed lemma (in linorder_topology) tendsto_min[tendsto_intros]: assumes X: "(X ⤏ x) net" and Y: "(Y ⤏ y) net" shows "((λx. min (X x) (Y x)) ⤏ min x y) net" proof (rule order_tendstoI) fix a assume "a < min x y" then show "eventually (λx. a < min (X x) (Y x)) net" using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a] by (auto simp: eventually_conj_iff) next fix a assume "min x y < a" then show "eventually (λx. min (X x) (Y x) < a) net" using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a] by (auto simp: min_less_iff_disj elim: eventually_mono) qed lemma (in order_topology) assumes "a < b" shows at_within_Icc_at_right: "at a within {a..b} = at_right a" and at_within_Icc_at_left: "at b within {a..b} = at_left b" using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"] using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"] by (auto intro!: order_class.order_antisym filter_leI simp: eventually_at_filter less_le elim: eventually_elim2) lemma (in order_topology) at_within_Icc_at: "a < x ⟹ x < b ⟹ at x within {a..b} = at x" by (rule at_within_open_subset[where S="{a<..<b}"]) auto lemma (in t2_space) tendsto_unique: assumes "F ≠ bot" and "(f ⤏ a) F" and "(f ⤏ b) F" shows "a = b" proof (rule ccontr) assume "a ≠ b" obtain U V where "open U" "open V" "a ∈ U" "b ∈ V" "U ∩ V = {}" using hausdorff [OF ‹a ≠ b›] by fast have "eventually (λx. f x ∈ U) F" using ‹(f ⤏ a) F› ‹open U› ‹a ∈ U› by (rule topological_tendstoD) moreover have "eventually (λx. f x ∈ V) F" using ‹(f ⤏ b) F› ‹open V› ‹b ∈ V› by (rule topological_tendstoD) ultimately have "eventually (λx. False) F" proof eventually_elim case (elim x) then have "f x ∈ U ∩ V" by simp with ‹U ∩ V = {}› show ?case by simp qed with ‹¬ trivial_limit F› show "False" by (simp add: trivial_limit_def) qed lemma (in t2_space) tendsto_const_iff: fixes a b :: 'a assumes "¬ trivial_limit F" shows "((λx. a) ⤏ b) F ⟷ a = b" by (auto intro!: tendsto_unique [OF assms tendsto_const]) lemma (in t2_space) tendsto_unique': assumes "F ≠ bot" shows "∃⇩_{≤}⇩_{1}l. (f ⤏ l) F" using Uniq_def assms local.tendsto_unique by fastforce lemma Lim_in_closed_set: assumes "closed S" "eventually (λx. f(x) ∈ S) F" "F ≠ bot" "(f ⤏ l) F" shows "l ∈ S" proof (rule ccontr) assume "l ∉ S" with ‹closed S› have "open (- S)" "l ∈ - S" by (simp_all add: open_Compl) with assms(4) have "eventually (λx. f x ∈ - S) F" by (rule topological_tendstoD) with assms(2) have "eventually (λx. False) F" by (rule eventually_elim2) simp with assms(3) show "False" by (simp add: eventually_False) qed lemma (in t3_space) nhds_closed: assumes "x ∈ A" and "open A" shows "∃A'. x ∈ A' ∧ closed A' ∧ A' ⊆ A ∧ eventually (λy. y ∈ A') (nhds x)" proof - from assms have "∃U V. open U ∧ open V ∧ x ∈ U ∧ - A ⊆ V ∧ U ∩ V = {}" by (intro t3_space) auto then obtain U V where UV: "open U" "open V" "x ∈ U" "-A ⊆ V" "U ∩ V = {}" by auto have "eventually (λy. y ∈ U) (nhds x)" using ‹open U› and ‹x ∈ U› by (intro eventually_nhds_in_open) hence "eventually (λy. y ∈ -V) (nhds x)" by eventually_elim (use UV in auto) with UV show ?thesis by (intro exI[of _ "-V"]) auto qed lemma (in order_topology) increasing_tendsto: assumes bdd: "eventually (λn. f n ≤ l) F" and en: "⋀x. x < l ⟹ eventually (λn. x < f n) F" shows "(f ⤏ l) F" using assms by (intro order_tendstoI) (auto elim!: eventually_mono) lemma (in order_topology) decreasing_tendsto: assumes bdd: "eventually (λn. l ≤ f n) F" and en: "⋀x. l < x ⟹ eventually (λn. f n < x) F" shows "(f ⤏ l) F" using assms by (intro order_tendstoI) (auto elim!: eventually_mono) lemma (in order_topology) tendsto_sandwich: assumes ev: "eventually (λn. f n ≤ g n) net" "eventually (λn. g n ≤ h n) net" assumes lim: "(f ⤏ c) net" "(h ⤏ c) net" shows "(g ⤏ c) net" proof (rule order_tendstoI) fix a show "a < c ⟹ eventually (λx. a < g x) net" using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2) next fix a show "c < a ⟹ eventually (λx. g x < a) net" using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2) qed lemma (in t1_space) limit_frequently_eq: assumes "F ≠ bot" and "frequently (λx. f x = c) F" and "(f ⤏ d) F" shows "d = c" proof (rule ccontr) assume "d ≠ c" from t1_space[OF this] obtain U where "open U" "d ∈ U" "c ∉ U" by blast with assms have "eventually (λx. f x ∈ U) F" unfolding tendsto_def by blast then have "eventually (λx. f x ≠ c) F" by eventually_elim (insert ‹c ∉ U›, blast) with assms(2) show False unfolding frequently_def by contradiction qed lemma (in t1_space) tendsto_imp_eventually_ne: assumes "(f ⤏ c) F" "c ≠ c'" shows "eventually (λz. f z ≠ c') F" proof (cases "F=bot") case True thus ?thesis by auto next case False show ?thesis proof (rule ccontr) assume "¬ eventually (λz. f z ≠ c') F" then have "frequently (λz. f z = c') F" by (simp add: frequently_def) from limit_frequently_eq[OF False this ‹(f ⤏ c) F›] and ‹c ≠ c'› show False by contradiction qed qed lemma (in linorder_topology) tendsto_le: assumes F: "¬ trivial_limit F" and x: "(f ⤏ x) F" and y: "(g ⤏ y) F" and ev: "eventually (λx. g x ≤ f x) F" shows "y ≤ x" proof (rule ccontr) assume "¬ y ≤ x" with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} ∩ {b<..} = {}" by (auto simp: not_le) then have "eventually (λx. f x < a) F" "eventually (λx. b < g x) F" using x y by (auto intro: order_tendstoD) with ev have "eventually (λx. False) F" by eventually_elim (insert xy, fastforce) with F show False by (simp add: eventually_False) qed lemma (in linorder_topology) tendsto_lowerbound: assumes x: "(f ⤏ x) F" and ev: "eventually (λi. a ≤ f i) F" and F: "¬ trivial_limit F" shows "a ≤ x" using F x tendsto_const ev by (rule tendsto_le) lemma (in linorder_topology) tendsto_upperbound: assumes x: "(f ⤏ x) F" and ev: "eventually (λi. a ≥ f i) F" and F: "¬ trivial_limit F" shows "a ≥ x" by (rule tendsto_le [OF F tendsto_const x ev]) lemma filterlim_at_within_not_equal: fixes f::"'a ⇒ 'b::t2_space" assumes "filterlim f (at a within s) F" shows "eventually (λw. f w∈s ∧ f w ≠b) F" proof (cases "a=b") case True then show ?thesis using assms by (simp add: filterlim_at) next case False from hausdorff[OF this] obtain U V where UV:"open U" "open V" "a ∈ U" "b ∈ V" "U ∩ V = {}" by auto have "(f ⤏ a) F" using assms filterlim_at by auto then have "∀⇩_{F}x in F. f x ∈ U" using UV unfolding tendsto_def by auto moreover have "∀⇩_{F}x in F. f x ∈ s ∧ f x≠a" using assms filterlim_at by auto ultimately show ?thesis apply eventually_elim using UV by auto qed subsubsection ‹Rules about \<^const>‹Lim›› lemma tendsto_Lim: "¬ trivial_limit net ⟹ (f ⤏ l) net ⟹ Lim net f = l" unfolding Lim_def using tendsto_unique [of net f] by auto lemma Lim_ident_at: "¬ trivial_limit (at x within s) ⟹ Lim (at x within s) (λx. x) = x" by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto lemma eventually_Lim_ident_at: "(∀⇩_{F}y in at x within X. P (Lim (at x within X) (λx. x)) y) ⟷ (∀⇩_{F}y in at x within X. P x y)" for x::"'a::t2_space" by (cases "at x within X = bot") (auto simp: Lim_ident_at) lemma filterlim_at_bot_at_right: fixes f :: "'a::linorder_topology ⇒ 'b::linorder" assumes mono: "⋀x y. Q x ⟹ Q y ⟹ x ≤ y ⟹ f x ≤ f y" and bij: "⋀x. P x ⟹ f (g x) = x" "⋀x. P x ⟹ Q (g x)" and Q: "eventually Q (at_right a)" and bound: "⋀b. Q b ⟹ a < b" and P: "eventually P at_bot" shows "filterlim f at_bot (at_right a)" proof - from P obtain x where x: "⋀y. y ≤ x ⟹ P y" unfolding eventually_at_bot_linorder by auto show ?thesis proof (intro filterlim_at_bot_le[THEN iffD2] allI impI) fix z assume "z ≤ x" with x have "P z" by auto have "eventually (λx. x ≤ g z) (at_right a)" using bound[OF bij(2)[OF ‹P z›]] unfolding eventually_at_right[OF bound[OF bij(2)[OF ‹P z›]]] by (auto intro!: exI[of _ "g z"]) with Q show "eventually (λx. f x ≤ z) (at_right a)" by eventually_elim (metis bij ‹P z› mono) qed qed lemma filterlim_at_top_at_left: fixes f :: "'a::linorder_topology ⇒ 'b::linorder" assumes mono: "⋀x y. Q x ⟹ Q y ⟹ x ≤ y ⟹ f x ≤ f y" and bij: "⋀x. P x ⟹ f (g x) = x" "⋀x. P x ⟹ Q (g x)" and Q: "eventually Q (at_left a)" and bound: "⋀b. Q b ⟹ b < a" and P: "eventually P at_top" shows "filterlim f at_top (at_left a)" proof - from P obtain x where x: "⋀y. x ≤ y ⟹ P y" unfolding eventually_at_top_linorder by auto show ?thesis proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) fix z assume "x ≤ z" with x have "P z" by auto have "eventually (λx. g z ≤ x) (at_left a)" using bound[OF bij(2)[OF ‹P z›]] unfolding eventually_at_left[OF bound[OF bij(2)[OF ‹P z›]]] by (auto intro!: exI[of _ "g z"]) with Q show "eventually (λx. z ≤ f x) (at_left a)" by eventually_elim (metis bij ‹P z› mono) qed qed lemma filterlim_split_at: "filterlim f F (at_left x) ⟹ filterlim f F (at_right x) ⟹ filterlim f F (at x)" for x :: "'a::linorder_topology" by (subst at_eq_sup_left_right) (rule filterlim_sup) lemma filterlim_at_split: "filterlim f F (at x) ⟷ filterlim f F (at_left x) ∧ filterlim f F (at_right x)" for x :: "'a::linorder_topology" by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup) lemma eventually_nhds_top: fixes P :: "'a :: {order_top,linorder_topology} ⇒ bool" and b :: 'a assumes "b < top" shows "eventually P (nhds top) ⟷ (∃b<top. (∀z. b < z ⟶ P z))" unfolding eventually_nhds proof safe fix S :: "'a set" assume "open S" "top ∈ S" note open_left[OF this ‹b < top›] moreover assume "∀s∈S. P s" ultimately show "∃b<top. ∀z>b. P z" by (auto simp: subset_eq Ball_def) next fix b assume "b < top" "∀z>b. P z" then show "∃S. open S ∧ top ∈ S ∧ (∀xa∈S. P xa)" by (intro exI[of _ "{b <..}"]) auto qed lemma tendsto_at_within_iff_tendsto_nhds: "(g ⤏ g l) (at l within S) ⟷ (g ⤏ g l) (inf (nhds l) (principal S))" unfolding tendsto_def eventually_at_filter eventually_inf_principal by (intro ext all_cong imp_cong) (auto elim!: eventually_mono) subsection ‹Limits on sequences› abbreviation (in topological_space) LIMSEQ :: "[nat ⇒ 'a, 'a] ⇒ bool" ("((_)/ ⇢ (_))" [60, 60] 60) where "X ⇢ L ≡ (X ⤏ L) sequentially" abbreviation (in t2_space) lim :: "(nat ⇒ 'a) ⇒ 'a" where "lim X ≡ Lim sequentially X" definition (in topological_space) convergent :: "(nat ⇒ 'a) ⇒ bool" where "convergent X = (∃L. X ⇢ L)" lemma lim_def: "lim X = (THE L. X ⇢ L)" unfolding Lim_def .. lemma lim_explicit: "f ⇢ f0 ⟷ (∀S. open S ⟶ f0 ∈ S ⟶ (∃N. ∀n≥N. f n ∈ S))" unfolding tendsto_def eventually_sequentially by auto subsection ‹Monotone sequences and subsequences› text ‹ Definition of monotonicity. The use of disjunction here complicates proofs considerably. One alternative is to add a Boolean argument to indicate the direction. Another is to develop the notions of increasing and decreasing first. › definition monoseq :: "(nat ⇒ 'a::order) ⇒ bool" where "monoseq X ⟷ (∀m. ∀n≥m. X m ≤ X n) ∨ (∀m. ∀n≥m. X n ≤ X m)" abbreviation incseq :: "(nat ⇒ 'a::order) ⇒ bool" where "incseq X ≡ mono X" lemma incseq_def: "incseq X ⟷ (∀m. ∀n≥m. X n ≥ X m)" unfolding mono_def .. abbreviation decseq :: "(nat ⇒ 'a::order) ⇒ bool" where "decseq X ≡ antimono X" lemma decseq_def: "decseq X ⟷ (∀m. ∀n≥m. X n ≤ X m)" unfolding antimono_def .. subsubsection ‹Definition of subsequence.› (* For compatibility with the old "subseq" *) lemma strict_mono_leD: "strict_mono r ⟹ m ≤ n ⟹ r m ≤ r n" by (erule (1) monoD [OF strict_mono_mono]) lemma strict_mono_id: "strict_mono id" by (simp add: strict_mono_def) lemma incseq_SucI: "(⋀n. X n ≤ X (Suc n)) ⟹ incseq X" using lift_Suc_mono_le[of X] by (auto simp: incseq_def) lemma incseqD: "incseq f ⟹ i ≤ j ⟹ f i ≤ f j" by (auto simp: incseq_def) lemma incseq_SucD: "incseq A ⟹ A i ≤ A (Suc i)" using incseqD[of A i "Suc i"] by auto lemma incseq_Suc_iff: "incseq f ⟷ (∀n. f n ≤ f (Suc n))" by (auto intro: incseq_SucI dest: incseq_SucD) lemma incseq_const[simp, intro]: "incseq (λx. k)" unfolding incseq_def by auto lemma decseq_SucI: "(⋀n. X (Suc n) ≤ X n) ⟹ decseq X" using order.lift_Suc_mono_le[OF dual_order, of X] by (auto simp: decseq_def) lemma decseqD: "decseq f ⟹ i ≤ j ⟹ f j ≤ f i" by (auto simp: decseq_def) lemma decseq_SucD: "decseq A ⟹ A (Suc i) ≤ A i" using decseqD[of A i "Suc i"] by auto lemma decseq_Suc_iff: "decseq f ⟷ (∀n. f (Suc n) ≤ f n)" by (auto intro: decseq_SucI dest: decseq_SucD) lemma decseq_const[simp, intro]: "decseq (λx. k)" unfolding decseq_def by auto lemma monoseq_iff: "monoseq X ⟷ incseq X ∨ decseq X" unfolding monoseq_def incseq_def decseq_def .. lemma monoseq_Suc: "monoseq X ⟷ (∀n. X n ≤ X (Suc n)) ∨ (∀n. X (Suc n) ≤ X n)" unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff .. lemma monoI1: "∀m. ∀n ≥ m. X m ≤ X n ⟹ monoseq X" by (simp add: monoseq_def) lemma monoI2: "∀m. ∀n ≥ m. X n ≤ X m ⟹ monoseq X" by (simp add: monoseq_def) lemma mono_SucI1: "∀n. X n ≤ X (Suc n) ⟹ monoseq X" by (simp add: monoseq_Suc) lemma mono_SucI2: "∀n. X (Suc n) ≤ X n ⟹ monoseq X" by (simp add: monoseq_Suc) lemma monoseq_minus: fixes a :: "nat ⇒ 'a::ordered_ab_group_add" assumes "monoseq a" shows "monoseq (λ n. - a n)" proof (cases "∀m. ∀n ≥ m. a m ≤ a n") case True then have "∀m. ∀n ≥ m. - a n ≤ - a m" by auto then show ?thesis by (rule monoI2) next case False then have "∀m. ∀n ≥ m. - a m ≤ - a n" using ‹monoseq a›[unfolded monoseq_def] by auto then show ?thesis by (rule monoI1) qed subsubsection ‹Subsequence (alternative definition, (e.g. Hoskins)› lemma strict_mono_Suc_iff: "strict_mono f ⟷ (∀n. f n < f (Suc n))" proof (intro iffI strict_monoI) assume *: "∀n. f n < f (Suc n)" fix m n :: nat assume "m < n" thus "f m < f n" by (induction rule: less_Suc_induct) (use * in auto) qed (auto simp: strict_mono_def) lemma strict_mono_add: "strict_mono (λn::'a::linordered_semidom. n + k)" by (auto simp: strict_mono_def) text ‹For any sequence, there is a monotonic subsequence.› lemma seq_monosub: fixes s :: "nat ⇒ 'a::linorder" shows "∃f. strict_mono f ∧ monoseq (λn. (s (f n)))" proof (cases "∀n. ∃p>n. ∀m≥p. s m ≤ s p") case True then have "∃f. ∀n. (∀m≥f n. s m ≤ s (f n)) ∧ f n < f (Suc n)" by (intro dependent_nat_choice) (auto simp: conj_commute) then obtain f :: "nat ⇒ nat" where f: "strict_mono f" and mono: "⋀n m. f n ≤ m ⟹ s m ≤ s (f n)" by (auto simp: strict_mono_Suc_iff) then have "incseq f" unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le) then have "monoseq (λn. s (f n))" by (auto simp add: incseq_def intro!: mono monoI2) with f show ?thesis by auto next case False then obtain N where N: "p > N ⟹ ∃m>p. s p < s m" for p by (force simp: not_le le_less) have "∃f. ∀n. N < f n ∧ f n < f (Suc n) ∧ s (f n) ≤ s (f (Suc n))" proof (intro dependent_nat_choice) fix x assume "N < x" with N[of x] show "∃y>N. x < y ∧ s x ≤ s y" by (auto intro: less_trans) qed auto then show ?thesis by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff) qed lemma seq_suble: assumes sf: "strict_mono (f :: nat ⇒ nat)" shows "n ≤ f n" proof (induct n) case 0 show ?case by simp next case (Suc n) with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)" by arith then show ?case by arith qed lemma eventually_subseq: "strict_mono r ⟹ eventually P sequentially ⟹ eventually (λn. P (r n)) sequentially" unfolding eventually_sequentially by (metis seq_suble le_trans) lemma not_eventually_sequentiallyD: assumes "¬ eventually P sequentially" shows "∃r::nat⇒nat. strict_mono r ∧ (∀n. ¬ P (r n))" proof - from assms have "∀n. ∃m≥n. ¬ P m" unfolding eventually_sequentially by (simp add: not_less) then obtain r where "⋀n. r n ≥ n" "⋀n. ¬ P (r n)" by (auto simp: choice_iff) then show ?thesis by (auto intro!: exI[of _ "λn. r (((Suc ∘ r) ^^ Suc n) 0)"] simp: less_eq_Suc_le strict_mono_Suc_iff) qed lemma sequentially_offset: assumes "eventually (λi. P i) sequentially" shows "eventually (λi. P (i + k)) sequentially" using assms by (rule eventually_sequentially_seg [THEN iffD2]) lemma seq_offset_neg: "(f ⤏ l) sequentially ⟹ ((λi. f(i - k)) ⤏ l) sequentially" apply (erule filterlim_compose) apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially, arith) done lemma filterlim_subseq: "strict_mono f ⟹ filterlim f sequentially sequentially" unfolding filterlim_iff by (metis eventually_subseq) lemma strict_mono_o: "strict_mono r ⟹ strict_mono s ⟹ strict_mono (r ∘ s)" unfolding strict_mono_def by simp lemma strict_mono_compose: "strict_mono r ⟹ strict_mono s ⟹ strict_mono (λx. r (s x))" using strict_mono_o[of r s] by (simp add: o_def) lemma incseq_imp_monoseq: "incseq X ⟹ monoseq X" by (simp add: incseq_def monoseq_def) lemma decseq_imp_monoseq: "decseq X ⟹ monoseq X" by (simp add: decseq_def monoseq_def) lemma decseq_eq_incseq: "decseq X = incseq (λn. - X n)" for X :: "nat ⇒ 'a::ordered_ab_group_add" by (simp add: decseq_def incseq_def) lemma INT_decseq_offset: assumes "decseq F" shows "(⋂i. F i) = (⋂i∈{n..}. F i)" proof safe fix x i assume x: "x ∈ (⋂i∈{n..}. F i)" show "x ∈ F i" proof cases from x have "x ∈ F n" by auto also assume "i ≤ n" with ‹decseq F› have "F n ⊆ F i" unfolding decseq_def by simp finally show ?thesis . qed (insert x, simp) qed auto lemma LIMSEQ_const_iff: "(λn. k) ⇢ l ⟷ k = l" for k l :: "'a::t2_space" using trivial_limit_sequentially by (rule tendsto_const_iff) lemma LIMSEQ_SUP: "incseq X ⟹ X ⇢ (SUP i. X i :: 'a::{complete_linorder,linorder_topology})" by (intro increasing_tendsto) (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans) lemma LIMSEQ_INF: "decseq X ⟹ X ⇢ (INF i. X i :: 'a::{complete_linorder,linorder_topology})" by (intro decreasing_tendsto) (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans) lemma LIMSEQ_ignore_initial_segment: "f ⇢ a ⟹ (λn. f (n + k)) ⇢ a" unfolding tendsto_def by (subst eventually_sequentially_seg[where k=k]) lemma LIMSEQ_offset: "(λn. f (n + k)) ⇢ a ⟹ f ⇢ a" unfolding tendsto_def by (subst (asm) eventually_sequentially_seg[where k=k]) lemma LIMSEQ_Suc: "f ⇢ l ⟹ (λn. f (Suc n)) ⇢ l" by (drule LIMSEQ_ignore_initial_segment [where k="Suc 0"]) simp lemma LIMSEQ_imp_Suc: "(λn. f (Suc n)) ⇢ l ⟹ f ⇢ l" by (rule LIMSEQ_offset [where k="Suc 0"]) simp lemma LIMSEQ_lessThan_iff_atMost: shows "(λn. f {..<n}) ⇢ x ⟷ (λn. f {..n}) ⇢ x" apply (subst filterlim_sequentially_Suc [symmetric]) apply (simp only: lessThan_Suc_atMost) done lemma (in t2_space) LIMSEQ_Uniq: "∃⇩_{≤}⇩_{1}l. X ⇢ l" by (simp add: tendsto_unique') lemma (in t2_space) LIMSEQ_unique: "X ⇢ a ⟹ X ⇢ b ⟹ a = b" using trivial_limit_sequentially by (rule tendsto_unique) lemma LIMSEQ_le_const: "X ⇢ x ⟹ ∃N. ∀n≥N. a ≤ X n ⟹ a ≤ x" for a x :: "'a::linorder_topology" by (simp add: eventually_at_top_linorder tendsto_lowerbound) lemma LIMSEQ_le: "X ⇢ x ⟹ Y ⇢ y ⟹ ∃N. ∀n≥N. X n ≤ Y n ⟹ x ≤ y" for x y :: "'a::linorder_topology" using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially) lemma LIMSEQ_le_const2: "X ⇢ x ⟹ ∃N. ∀n≥N. X n ≤ a ⟹ x ≤ a" for a x :: "'a::linorder_topology" by (rule LIMSEQ_le[of X x "λn. a"]) auto lemma Lim_bounded: "f ⇢ l ⟹ ∀n≥M. f n ≤ C ⟹ l ≤ C" for l :: "'a::linorder_topology" by (intro LIMSEQ_le_const2) auto lemma Lim_bounded2: fixes f :: "nat ⇒ 'a::linorder_topology" assumes lim:"f ⇢ l" and ge: "∀n≥N. f n ≥ C" shows "l ≥ C" using ge by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const]) (auto simp: eventually_sequentially) lemma lim_mono: fixes X Y :: "nat ⇒ 'a::linorder_topology" assumes "⋀n. N ≤ n ⟹ X n ≤ Y n" and "X ⇢ x" and "Y ⇢ y" shows "x ≤ y" using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto lemma Sup_lim: fixes a :: "'a::{complete_linorder,linorder_topology}" assumes "⋀n. b n ∈ s" and "b ⇢ a" shows "a ≤ Sup s" by (metis Lim_bounded assms complete_lattice_class.Sup_upper) lemma Inf_lim: fixes a :: "'a::{complete_linorder,linorder_topology}" assumes "⋀n. b n ∈ s" and "b ⇢ a" shows "Inf s ≤ a" by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower) lemma SUP_Lim: fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}" assumes inc: "incseq X" and l: "X ⇢ l" shows "(SUP n. X n) = l" using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp lemma INF_Lim: