Quelle Topological_Spaces.thy Sprache: Isabelle

(*  Title:      HOL/Topological_Spaces.thy
    Author:     Brian Huffman
    Author:     Johannes Hölzl
*)

section \<open>Topological Spaces\<close>

theory Topological_Spaces
  imports Main
begin

named_theorems continuous_intros "structural introduction rules for continuity"

subsection \<open>Topological space\<close>

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 \<open>Hausdorff and other separation properties\<close>

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 \<subseteq> 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 \<open>T2 spaces are also known as Hausdorff spaces.\<close>

class t2_space = topological_space +
  assumes hausdorff: "x \ y \ \U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}"

instance t2_space \<subseteq> 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 \<open>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.\<close>

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 \<open>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.\<close>

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 \<open>T4 is stronger than T3, and weaker than metric.\<close>

instance t4_space \<subseteq> 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 \<open>A perfect space is a topological space with no isolated points.\<close>

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 \<open>Generators for topologies\<close>

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 \<open>Order topologies\<close>

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 \<open>x < y\<close> have "x \<in> {..< y}" "y \<in> {x <..}" "{x <..} \<inter> {..< y} = {}"
    by auto
  then show ?thesis by blast
qed

instance linorder_topology \<subseteq> 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 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

lemma filterlim_atLeastAtMost_at_bot_at_top:
  fixes f g :: "'a \ 'b :: linorder_topology"
  assumes "filterlim f at_bot F" "filterlim g at_top F"
  assumes [simp]: "\a b. finite {a..b::'b}"
  shows   "filterlim (\x. {f x..g x}) finite_sets_at_top F"
  unfolding filterlim_finite_subsets_at_top
proof safe
  fix X :: "'b set"
  assume X: "finite X"
  from X obtain lb where lb: "\x. x \ X \ lb \ x"
    by (metis finite_has_minimal2 nle_le)
  from X obtain ub where ub: "\x. x \ X \ x \ ub"
    by (metis all_not_in_conv finite_has_maximal nle_le)
  have "eventually (\x. f x \ lb) F" "eventually (\x. g x \ ub) F"
    using assms by (simp_all add: filterlim_at_bot filterlim_at_top)
  thus "eventually (\x. finite {f x..g x} \ X \ {f x..g x} \ {f x..g x} \ UNIV) F"
  proof eventually_elim
    case (elim x)
    have "X \ {f x..g x}"
    proof
      fix y assume "y \ X"
      thus "y \ {f x..g x}"
        using lb[of y] ub[of y] elim by auto
    qed
    thus ?case
      by auto
  qed
qed

subsection \<open>Setup some topologies\<close>

subsubsection \<open>Boolean is an order topology\<close>

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} = {.. {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}" 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 \<open>Topological filters\<close>

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"
    (\<open>at (_)/ within (_)\<close> [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 \ (\\<^sub>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 eventually_nhds_conv_at:
  "eventually P (nhds x) \ eventually P (at x) \ P x"
  unfolding eventually_at_topological eventually_nhds by fast

lemma eventually_at_in_open:
  assumes "open A" "x \ A"
  shows   "eventually (\y. y \ A - {x}) (at x)"
  using assms eventually_at_topological by blast

lemma eventually_at_in_open':
  assumes "open A" "x \ A"
  shows   "eventually (\y. y \ A) (at x)"
  using assms eventually_at_topological by blast

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 \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
  then show "\\<^sub>F n in nhds x. (n \ x \ n \ T \ P n) = (n \ x \ n \ U \ P n)" for P
    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, 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 t1_space) eventually_neq_at_within:
  "eventually (\w. w \ x) (at z within A)"
  by (smt (verit, ccfv_threshold) eventually_True eventually_at_topological separation_t1)

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} =
      (\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>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\<in>{x <..}. principal ({..< a} \<inter> s - {x}))
        (INF a\<in>{..< x}. principal ({a <..} \<inter> 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) \ (\by>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: "\\<^sub>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<.. 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<.. P x" "a < b"
  shows   "eventually P (at_right a)"
  using assms unfolding eventually_at_topological by (intro exI[of _ "{..]) 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)) \
     (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> 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) \ (\by>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)

lemma filtermap_nhds_eq_imp_filtermap_at_eq:
  assumes "filtermap f (nhds z) = nhds (f z)"
  assumes "eventually (\x. f x = f z \ x = z) (at z)"
  shows   "filtermap f (at z) = at (f z)"
proof (rule filter_eqI)
  fix P :: "'a \ bool"
  have "eventually P (filtermap f (at z)) \ (\\<^sub>F x in nhds z. x \ z \ P (f x))"
    by (simp add: eventually_filtermap eventually_at_filter)
  also have "\ \ (\\<^sub>F x in nhds z. f x \ f z \ P (f x))"
    by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
  also have "\ \ (\\<^sub>F x in filtermap f (nhds z). x \ f z \ P x)"
    by (simp add: eventually_filtermap)
  also have "filtermap f (nhds z) = nhds (f z)"
    by (rule assms)
  also have "(\\<^sub>F x in nhds (f z). x \ f z \ P x) \ (\\<^sub>F x in at (f z). P x)"
    by (simp add: eventually_at_filter)
  finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
qed

subsubsection \<open>Tendsto\<close>

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 \<open>
  Global_Theory.add_thms_dynamic (\<^binding>\<open>tendsto_eq_intros\<close>,
    fn context =>
      Named_Theorems.get (Context.proof_of context) \<^named_theorems>\<open>tendsto_intros\<close>
      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
\<close>

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 \ (\lx. 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 \<longlongrightarrow> 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 "{..]
  by (auto intro!: order_class.order_antisym filter_leI
      simp: eventually_at_filter less_le
      elim: eventually_elim2)

lemma (in order_topology)
  shows at_within_Ici_at_right: "at a within {a..} = at_right a"
    and at_within_Iic_at_left:  "at a within {..a} = at_left a"
  using order_tendstoD(2)[OF tendsto_ident_at [where s = "{a<..}"]]
  using order_tendstoD(1)[OF tendsto_ident_at[where s = "{..]]
  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<..]) 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 \<open>a \<noteq> b\<close>] by fast
  have "eventually (\x. f x \ U) F"
    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
  moreover
  have "eventually (\x. f x \ V) F"
    using \<open>(f \<longlongrightarrow> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> 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 \<open>U \<inter> V = {}\<close> show ?case by simp
  qed
  with \<open>\<not> trivial_limit F\<close> 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 "\\<^sub>\\<^sub>1l. (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 \<open>closed S\<close> have "open (- S)" "l \<in> - 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>open U\<close> and \<open>x \<in> U\<close> 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 \<open>c \<notin> U\<close>, 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 \<open>(f \<longlongrightarrow> c) F\<close>] and \<open>c \<noteq> c'\<close> 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" "{.. {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 "\\<^sub>F x in F. f x \ U" using UV unfolding tendsto_def by auto
  moreover have  "\\<^sub>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 \<open>Rules about \<^const>\<open>Lim\<close>\<close>

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 (simp add: tendsto_Lim)

lemma Lim_cong:
  assumes "\\<^sub>F x in F. f x = g x" "F = G"
  shows "Lim F f = Lim F g"
  unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce

lemma eventually_Lim_ident_at:
  "(\\<^sub>F y in at x within X. P (Lim (at x within X) (\x. x)) y) \
    (\<forall>\<^sub>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 \<open>P z\<close>]]
      unfolding eventually_at_right[OF bound[OF bij(2)[OF \<open>P z\<close>]]]
      by (auto intro!: exI[of _ "g z"])
    with Q show "eventually (\x. f x \ z) (at_right a)"
      by eventually_elim (metis bij \<open>P z\<close> 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 \<open>P z\<close>]]
      unfolding eventually_at_left[OF bound[OF bij(2)[OF \<open>P z\<close>]]]
      by (auto intro!: exI[of _ "g z"])
    with Q show "eventually (\x. z \ f x) (at_left a)"
      by eventually_elim (metis bij \<open>P z\<close> 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) \ (\bz. b < z \ P z))"
  unfolding eventually_nhds
proof safe
  fix S :: "'a set"
  assume "open S" "top \ S"
  note open_left[OF this \<open>b < top\<close>]
  moreover assume "\s\S. P s"
  ultimately show "\bz>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 \<open>Limits on sequences\<close>

abbreviation (in topological_space)
  LIMSEQ :: "[nat \ 'a, 'a] \ bool" (\(\notation=\infix LIMSEQ\\(_)/ \ (_))\ [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

lemma closed_sequentially:
  assumes "closed S" and "\n. f n \ S" and "f \ l"
  shows "l \ S"
  by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)

subsection \<open>Monotone sequences and subsequences\<close>

text \<open>
  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.
\<close>
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 \<open>Definition of subsequence.\<close>

(* 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"
  by (simp add: mono_iff_le_Suc)

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"
  by (simp add: antimono_iff_le_Suc)

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 \<open>monoseq a\<close>[unfolded monoseq_def] by auto
  then show ?thesis by (rule monoI1)
qed

subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>

text \<open>For any sequence, there is a monotonic subsequence.\<close>
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 {.. x \ (\n. f {..n}) \ x"
  apply (subst filterlim_sequentially_Suc [symmetric])
  apply (simp only: lessThan_Suc_atMost)
  done

lemma (in t2_space) LIMSEQ_Uniq: "\\<^sub>\\<^sub>1l. 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:
  fixes X :: "nat \ 'a::{complete_linorder,linorder_topology}"
  assumes dec: "decseq X"
    and l: "X \ l"
  shows "(INF n. X n) = l"
  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
  by simp

lemma convergentD: "convergent X \ \L. X \ L"
  by (simp add: convergent_def)

lemma convergentI: "X \ L \ convergent X"
  by (auto simp add: convergent_def)

lemma convergent_LIMSEQ_iff: "convergent X \ X \ lim X"
  by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)

lemma convergent_const: "convergent (\n. c)"
  by (rule convergentI) (rule tendsto_const)

lemma monoseq_le:
  "monoseq a \ a \ x \
    (\<forall>n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n) \<or>
    (\<forall>n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m)"
  for x :: "'a::linorder_topology"
  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)

--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.36 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.