Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Topological_Spaces.thy Sprache: Isabelle

Original von: 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 (induct 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 toplogies\<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

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"
    ("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 \ (\\<^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 (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
  apply safe
   apply (case_tac "S = {a}")
    apply simp
   apply fast
  apply fast
  done

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)

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)

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.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 (rule tendsto_Lim[OF _ tendsto_ident_at]) auto

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" ("((_)/ \ (_))" [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 \<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"
  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 \<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>

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 \<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)

lemma LIMSEQ_subseq_LIMSEQ: "X \ L \ strict_mono f \ (X \ f) \ L"
  unfolding comp_def by (rule filterlim_compose [of X, OF _ filterlim_subseq])

lemma convergent_subseq_convergent: "convergent X \ strict_mono f \ convergent (X \ f)"
  by (auto simp: convergent_def intro: LIMSEQ_subseq_LIMSEQ)

lemma limI: "X \ L \ lim X = L"
  by (rule tendsto_Lim) (rule trivial_limit_sequentially)

lemma lim_le: "convergent f \ (\n. f n \ x) \ lim f \ x"
  for x :: "'a::linorder_topology"
  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)

lemma lim_const [simp]: "lim (\m. a) = a"
  by (simp add: limI)

subsubsection \<open>Increasing and Decreasing Series\<close>

lemma incseq_le: "incseq X \ X \ L \ X n \ L"
  for L :: "'a::linorder_topology"
  by (metis incseq_def LIMSEQ_le_const)

lemma decseq_ge: "decseq X \ X \ L \ L \ X n"
  for L :: "'a::linorder_topology"
  by (metis decseq_def LIMSEQ_le_const2)

subsection \<open>First countable topologies\<close>

class first_countable_topology = topological_space +
  assumes first_countable_basis:
    "\A::nat \ 'a set. (\i. x \ A i \ open (A i)) \ (\S. open S \ x \ S \ (\i. A i \ S))"

lemma (in first_countable_topology) countable_basis_at_decseq:
  obtains A :: "nat \ 'a set" where
    "\i. open (A i)" "\i. x \ (A i)"
    "\S. open S \ x \ S \ eventually (\i. A i \ S) sequentially"
proof atomize_elim
  from first_countable_basis[of x] obtain A :: "nat \ 'a set"
    where nhds: "\i. open (A i)" "\i. x \ A i"
      and incl: "\S. open S \ x \ S \ \i. A i \ S"
    by auto
  define F where "F n = (\i\n. A i)" for n
  show "\A. (\i. open (A i)) \ (\i. x \ A i) \
    (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
  proof (safe intro!: exI[of _ F])
    fix i
    show "open (F i)"
      using nhds(1) by (auto simp: F_def)
    show "x \ F i"
      using nhds(2) by (auto simp: F_def)
  next
    fix S
    assume "open S" "x \ S"
    from incl[OF this] obtain i where "F i \ S"
      unfolding F_def by auto
    moreover have "\j. i \ j \ F j \ F i"
      by (simp add: Inf_superset_mono F_def image_mono)
    ultimately show "eventually (\i. F i \ S) sequentially"
      by (auto simp: eventually_sequentially)
  qed
qed

lemma (in first_countable_topology) nhds_countable:
  obtains X :: "nat \ 'a set"
  where "decseq X" "\n. open (X n)" "\n. x \ X n" "nhds x = (INF n. principal (X n))"
proof -
  from first_countable_basis obtain A :: "nat \ 'a set"
    where *: "\n. x \ A n" "\n. open (A n)" "\S. open S \ x \ S \ \i. A i \ S"
    by metis
  show thesis
  proof
    show "decseq (\n. \i\n. A i)"
      by (simp add: antimono_iff_le_Suc atMost_Suc)
    show "x \ (\i\n. A i)" "\n. open (\i\n. A i)" for n
      using * by auto
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Topological_Spaces.thy Sprache: Isabelle

Original von: Isabelle©

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Original von: Isabelle^©