src/HOL/Topological_Spaces.thy
author wenzelm
Tue, 06 Oct 2015 17:46:07 +0200
changeset 61342 b98cd131e2b5
parent 61306 9dd394c866fc
child 61426 d53db136e8fd
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52265
bb907eba5902 tuned headers;
wenzelm
parents: 51775
diff changeset
     1
(*  Title:      HOL/Topological_Spaces.thy
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     2
    Author:     Brian Huffman
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     3
    Author:     Johannes Hölzl
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     4
*)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     5
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
     6
section \<open>Topological Spaces\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     7
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
     8
theory Topological_Spaces
51773
9328c6681f3c spell conditional_ly_-complete lattices correct
hoelzl
parents: 51641
diff changeset
     9
imports Main Conditionally_Complete_Lattices
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    10
begin
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    11
57953
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
    12
named_theorems continuous_intros "structural introduction rules for continuity"
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
    13
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    14
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
    15
subsection \<open>Topological space\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    16
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    17
class "open" =
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    18
  fixes "open" :: "'a set \<Rightarrow> bool"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    19
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    20
class topological_space = "open" +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    21
  assumes open_UNIV [simp, intro]: "open UNIV"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    22
  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60182
diff changeset
    23
  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    24
begin
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    25
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    26
definition
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    27
  closed :: "'a set \<Rightarrow> bool" where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    28
  "closed S \<longleftrightarrow> open (- S)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    29
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    30
lemma open_empty [continuous_intros, intro, simp]: "open {}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    31
  using open_Union [of "{}"] by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    32
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    33
lemma open_Un [continuous_intros, intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    34
  using open_Union [of "{S, T}"] by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    35
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    36
lemma open_UN [continuous_intros, intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56020
diff changeset
    37
  using open_Union [of "B ` A"] by simp
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    38
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    39
lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    40
  by (induct set: finite) auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    41
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    42
lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56020
diff changeset
    43
  using open_Inter [of "B ` A"] by simp
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    44
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    45
lemma openI:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    46
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    47
  shows "open S"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    48
proof -
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    49
  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    50
  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    51
  ultimately show "open S" by simp
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    52
qed
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
    53
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    54
lemma closed_empty [continuous_intros, intro, simp]:  "closed {}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    55
  unfolding closed_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    56
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    57
lemma closed_Un [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    58
  unfolding closed_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    59
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    60
lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    61
  unfolding closed_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    62
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    63
lemma closed_Int [continuous_intros, intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    64
  unfolding closed_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    65
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    66
lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    67
  unfolding closed_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    68
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60182
diff changeset
    69
lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    70
  unfolding closed_def uminus_Inf by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    71
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    72
lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    73
  by (induct set: finite) auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    74
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    75
lemma closed_UN [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56020
diff changeset
    76
  using closed_Union [of "B ` A"] by simp
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    77
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    78
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    79
  unfolding closed_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    80
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    81
lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    82
  unfolding closed_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    83
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    84
lemma open_Diff [continuous_intros, intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    85
  unfolding closed_open Diff_eq by (rule open_Int)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    86
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    87
lemma closed_Diff [continuous_intros, intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    88
  unfolding open_closed Diff_eq by (rule closed_Int)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    89
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    90
lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open (- S)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    91
  unfolding closed_open .
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    92
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
    93
lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    94
  unfolding open_closed .
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
    95
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
    96
lemma open_Collect_neg: "closed {x. P x} \<Longrightarrow> open {x. \<not> P x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
    97
  unfolding Collect_neg_eq by (rule open_Compl)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
    98
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
    99
lemma open_Collect_conj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<and> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   100
  using open_Int[OF assms] by (simp add: Int_def)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   101
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   102
lemma open_Collect_disj: assumes "open {x. P x}" "open {x. Q x}" shows "open {x. P x \<or> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   103
  using open_Un[OF assms] by (simp add: Un_def)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   104
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   105
lemma open_Collect_ex: "(\<And>i. open {x. P i x}) \<Longrightarrow> open {x. \<exists>i. P i x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   106
  using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp 
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   107
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   108
lemma open_Collect_imp: "closed {x. P x} \<Longrightarrow> open {x. Q x} \<Longrightarrow> open {x. P x \<longrightarrow> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   109
  unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   110
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   111
lemma open_Collect_const: "open {x. P}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   112
  by (cases P) auto
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   113
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   114
lemma closed_Collect_neg: "open {x. P x} \<Longrightarrow> closed {x. \<not> P x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   115
  unfolding Collect_neg_eq by (rule closed_Compl)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   116
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   117
lemma closed_Collect_conj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<and> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   118
  using closed_Int[OF assms] by (simp add: Int_def)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   119
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   120
lemma closed_Collect_disj: assumes "closed {x. P x}" "closed {x. Q x}" shows "closed {x. P x \<or> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   121
  using closed_Un[OF assms] by (simp add: Un_def)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   122
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   123
lemma closed_Collect_all: "(\<And>i. closed {x. P i x}) \<Longrightarrow> closed {x. \<forall>i. P i x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   124
  using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_all_eq by simp 
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   125
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   126
lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   127
  unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   128
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   129
lemma closed_Collect_const: "closed {x. P}"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   130
  by (cases P) auto
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   131
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   132
end
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   133
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   134
subsection\<open>Hausdorff and other separation properties\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   135
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   136
class t0_space = topological_space +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   137
  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   138
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   139
class t1_space = topological_space +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   140
  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   141
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   142
instance t1_space \<subseteq> t0_space
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   143
proof qed (fast dest: t1_space)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   144
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   145
lemma separation_t1:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   146
  fixes x y :: "'a::t1_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   147
  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   148
  using t1_space[of x y] by blast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   149
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   150
lemma closed_singleton:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   151
  fixes a :: "'a::t1_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   152
  shows "closed {a}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   153
proof -
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   154
  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   155
  have "open ?T" by (simp add: open_Union)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   156
  also have "?T = - {a}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   157
    by (simp add: set_eq_iff separation_t1, auto)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   158
  finally show "closed {a}" unfolding closed_def .
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   159
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   160
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   161
lemma closed_insert [continuous_intros, simp]:
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   162
  fixes a :: "'a::t1_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   163
  assumes "closed S" shows "closed (insert a S)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   164
proof -
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   165
  from closed_singleton assms
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   166
  have "closed ({a} \<union> S)" by (rule closed_Un)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   167
  thus "closed (insert a S)" by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   168
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   169
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   170
lemma finite_imp_closed:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   171
  fixes S :: "'a::t1_space set"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   172
  shows "finite S \<Longrightarrow> closed S"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   173
by (induct set: finite, simp_all)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   174
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   175
text \<open>T2 spaces are also known as Hausdorff spaces.\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   176
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   177
class t2_space = topological_space +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   178
  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   179
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   180
instance t2_space \<subseteq> t1_space
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   181
proof qed (fast dest: hausdorff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   182
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   183
lemma separation_t2:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   184
  fixes x y :: "'a::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   185
  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   186
  using hausdorff[of x y] by blast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   187
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   188
lemma separation_t0:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   189
  fixes x y :: "'a::t0_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   190
  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   191
  using t0_space[of x y] by blast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   192
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   193
text \<open>A perfect space is a topological space with no isolated points.\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   194
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   195
class perfect_space = topological_space +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   196
  assumes not_open_singleton: "\<not> open {x}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   197
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   198
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   199
subsection \<open>Generators for toplogies\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   200
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   201
inductive generate_topology for S where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   202
  UNIV: "generate_topology S UNIV"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   203
| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   204
| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   205
| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   206
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   207
hide_fact (open) UNIV Int UN Basis 
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   208
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   209
lemma generate_topology_Union: 
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   210
  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
56166
9a241bc276cd normalising simp rules for compound operators
haftmann
parents: 56020
diff changeset
   211
  using generate_topology.UN [of "K ` I"] by auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   212
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   213
lemma topological_space_generate_topology:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   214
  "class.topological_space (generate_topology S)"
61169
4de9ff3ea29a tuned proofs -- less legacy;
wenzelm
parents: 60762
diff changeset
   215
  by standard (auto intro: generate_topology.intros)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   216
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   217
subsection \<open>Order topologies\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   218
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   219
class order_topology = order + "open" +
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   220
  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   221
begin
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   222
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   223
subclass topological_space
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   224
  unfolding open_generated_order
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   225
  by (rule topological_space_generate_topology)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   226
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   227
lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   228
  unfolding open_generated_order by (auto intro: generate_topology.Basis)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   229
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   230
lemma open_lessThan [continuous_intros, simp]: "open {..< a}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   231
  unfolding open_generated_order by (auto intro: generate_topology.Basis)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   232
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   233
lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   234
   unfolding greaterThanLessThan_eq by (simp add: open_Int)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   235
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   236
end
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   237
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   238
class linorder_topology = linorder + order_topology
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   239
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   240
lemma closed_atMost [continuous_intros, simp]: "closed {.. a::'a::linorder_topology}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   241
  by (simp add: closed_open)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   242
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   243
lemma closed_atLeast [continuous_intros, simp]: "closed {a::'a::linorder_topology ..}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   244
  by (simp add: closed_open)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   245
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56329
diff changeset
   246
lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a::'a::linorder_topology .. b}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   247
proof -
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   248
  have "{a .. b} = {a ..} \<inter> {.. b}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   249
    by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   250
  then show ?thesis
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   251
    by (simp add: closed_Int)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   252
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   253
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   254
lemma (in linorder) less_separate:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   255
  assumes "x < y"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   256
  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   257
proof (cases "\<exists>z. x < z \<and> z < y")
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   258
  case True
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   259
  then obtain z where "x < z \<and> z < y" ..
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   260
  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   261
    by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   262
  then show ?thesis by blast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   263
next
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
   264
  case False
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   265
  with \<open>x < y\<close> have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   266
    by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   267
  then show ?thesis by blast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   268
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   269
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   270
instance linorder_topology \<subseteq> t2_space
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   271
proof
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   272
  fix x y :: 'a
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   273
  from less_separate[of x y] less_separate[of y x]
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   274
  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   275
    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   276
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   277
51480
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   278
lemma (in linorder_topology) open_right:
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   279
  assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   280
  using assms unfolding open_generated_order
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   281
proof induction
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   282
  case (Int A B)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   283
  then obtain a b where "a > x" "{x ..< a} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> B" by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   284
  then show ?case by (auto intro!: exI[of _ "min a b"])
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   285
next
51480
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   286
  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex)
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   287
qed blast+
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   288
51480
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   289
lemma (in linorder_topology) open_left:
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   290
  assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   291
  using assms unfolding open_generated_order
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   292
proof induction
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   293
  case (Int A B)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   294
  then obtain a b where "a < x" "{a <.. x} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B" by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   295
  then show ?case by (auto intro!: exI[of _ "max a b"])
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   296
next
51480
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   297
  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
   298
qed blast+
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   299
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   300
subsubsection \<open>Boolean is an order topology\<close>
59106
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   301
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   302
text \<open>It also is a discrete topology, but don't have a type class for it (yet).\<close>
59106
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   303
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   304
instantiation bool :: order_topology
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   305
begin
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   306
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   307
definition open_bool :: "bool set \<Rightarrow> bool" where
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   308
  "open_bool = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   309
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   310
instance
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   311
  proof qed (rule open_bool_def)
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   312
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   313
end
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   314
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   315
lemma open_bool[simp, intro!]: "open (A::bool set)"
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   316
proof -
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   317
  have *: "{False <..} = {True}" "{..< True} = {False}"
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   318
    by auto
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   319
  have "A = UNIV \<or> A = {} \<or> A = {False <..} \<or> A = {..< True}"
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   320
    using subset_UNIV[of A] unfolding UNIV_bool * by auto
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   321
  then show "open A"
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   322
    by auto
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   323
qed
af691e67f71f instance bool and enat as topologies
hoelzl
parents: 58889
diff changeset
   324
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   325
subsubsection \<open>Topological filters\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   326
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   327
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
57276
49c51eeaa623 filters are easier to define with INF on filters.
hoelzl
parents: 57275
diff changeset
   328
  where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   329
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   330
definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   331
  where "at a within s = inf (nhds a) (principal (s - {a}))"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   332
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   333
abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   334
  "at x \<equiv> at x within (CONST UNIV)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   335
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   336
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   337
  "at_right x \<equiv> at x within {x <..}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   338
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   339
abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter" where
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   340
  "at_left x \<equiv> at x within {..< x}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   341
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   342
lemma (in topological_space) nhds_generated_topology:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   343
  "open = generate_topology T \<Longrightarrow> nhds x = (INF S:{S\<in>T. x \<in> S}. principal S)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   344
  unfolding nhds_def
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   345
proof (safe intro!: antisym INF_greatest)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   346
  fix S assume "generate_topology T S" "x \<in> S"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   347
  then show "(INF S:{S \<in> T. x \<in> S}. principal S) \<le> principal S"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   348
    by induction 
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   349
       (auto intro: INF_lower order_trans simp add: inf_principal[symmetric] simp del: inf_principal)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   350
qed (auto intro!: INF_lower intro: generate_topology.intros)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   351
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   352
lemma (in topological_space) eventually_nhds:
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   353
  "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
57276
49c51eeaa623 filters are easier to define with INF on filters.
hoelzl
parents: 57275
diff changeset
   354
  unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   355
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   356
lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   357
  unfolding trivial_limit_def eventually_nhds by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   358
60182
e1ea5a6379c9 generalized tends over powr; added DERIV rule for powr
hoelzl
parents: 60172
diff changeset
   359
lemma (in t1_space) t1_space_nhds:
e1ea5a6379c9 generalized tends over powr; added DERIV rule for powr
hoelzl
parents: 60172
diff changeset
   360
  "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
e1ea5a6379c9 generalized tends over powr; added DERIV rule for powr
hoelzl
parents: 60172
diff changeset
   361
  by (drule t1_space) (auto simp: eventually_nhds)
e1ea5a6379c9 generalized tends over powr; added DERIV rule for powr
hoelzl
parents: 60172
diff changeset
   362
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   363
lemma at_within_eq: "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   364
  unfolding nhds_def at_within_def by (subst INF_inf_const2[symmetric]) (auto simp add: Diff_Int_distrib)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   365
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   366
lemma eventually_at_filter:
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   367
  "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   368
  unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   369
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   370
lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   371
  unfolding at_within_def by (intro inf_mono) auto
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   372
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   373
lemma eventually_at_topological:
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   374
  "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   375
  unfolding eventually_nhds eventually_at_filter by simp
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   376
51481
ef949192e5d6 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents: 51480
diff changeset
   377
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   378
  unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
51481
ef949192e5d6 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents: 51480
diff changeset
   379
61234
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   380
lemma at_within_open_NO_MATCH:
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   381
  "a \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   382
  by (simp only: at_within_open)
a9e6052188fa New lemmas
paulson <lp15@cam.ac.uk>
parents: 61204
diff changeset
   383
61245
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   384
lemma at_within_nhd:
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   385
  assumes "x \<in> S" "open S" "T \<inter> S - {x} = U \<inter> S - {x}"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   386
  shows "at x within T = at x within U"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   387
  unfolding filter_eq_iff eventually_at_filter
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   388
proof (intro allI eventually_subst)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   389
  have "eventually (\<lambda>x. x \<in> S) (nhds x)"
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   390
    using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   391
  then show "\<forall>\<^sub>F n in nhds x. (n \<noteq> x \<longrightarrow> n \<in> T \<longrightarrow> P n) = (n \<noteq> x \<longrightarrow> n \<in> U \<longrightarrow> P n)" for P  
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   392
    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   393
qed
b77bf45efe21 prove Liminf_inverse_ereal
hoelzl
parents: 61234
diff changeset
   394
53859
e6cb01686f7b replace lemma with more general simp rule
huffman
parents: 53381
diff changeset
   395
lemma at_within_empty [simp]: "at a within {} = bot"
e6cb01686f7b replace lemma with more general simp rule
huffman
parents: 53381
diff changeset
   396
  unfolding at_within_def by simp
e6cb01686f7b replace lemma with more general simp rule
huffman
parents: 53381
diff changeset
   397
53860
f2d683432580 factor out new lemma
huffman
parents: 53859
diff changeset
   398
lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
f2d683432580 factor out new lemma
huffman
parents: 53859
diff changeset
   399
  unfolding filter_eq_iff eventually_sup eventually_at_filter
f2d683432580 factor out new lemma
huffman
parents: 53859
diff changeset
   400
  by (auto elim!: eventually_rev_mp)
f2d683432580 factor out new lemma
huffman
parents: 53859
diff changeset
   401
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   402
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   403
  unfolding trivial_limit_def eventually_at_topological
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   404
  by (safe, case_tac "S = {a}", simp, fast, fast)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   405
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   406
lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   407
  by (simp add: at_eq_bot_iff not_open_singleton)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   408
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   409
lemma (in order_topology) nhds_order: "nhds x =
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   410
  inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   411
proof -
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   412
  have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} = 
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   413
      (\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   414
    by auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   415
  show ?thesis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   416
    unfolding nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def ..
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   417
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   418
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   419
lemma (in linorder_topology) at_within_order: "UNIV \<noteq> {x} \<Longrightarrow> 
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   420
  at x within s = inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   421
                      (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   422
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split[case_product case_split])
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   423
  assume "UNIV \<noteq> {x}" "{x<..} = {}" "{..< x} = {}"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   424
  moreover have "UNIV = {..< x} \<union> {x} \<union> {x <..}"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   425
    by auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   426
  ultimately show ?thesis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   427
    by auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   428
qed (auto simp: at_within_def nhds_order Int_Diff inf_principal[symmetric] INF_inf_const2
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   429
                inf_sup_aci[where 'a="'a filter"]
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   430
          simp del: inf_principal)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   431
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   432
lemma (in linorder_topology) at_left_eq:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   433
  "y < x \<Longrightarrow> at_left x = (INF a:{..< x}. principal {a <..< x})"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   434
  by (subst at_within_order)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   435
     (auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   436
           intro!: INF_lower2 inf_absorb2)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   437
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   438
lemma (in linorder_topology) eventually_at_left:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   439
  "y < x \<Longrightarrow> eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   440
  unfolding at_left_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   441
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   442
lemma (in linorder_topology) at_right_eq:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   443
  "x < y \<Longrightarrow> at_right x = (INF a:{x <..}. principal {x <..< a})"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   444
  by (subst at_within_order)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   445
     (auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   446
           intro!: INF_lower2 inf_absorb1)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   447
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   448
lemma (in linorder_topology) eventually_at_right:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   449
  "x < y \<Longrightarrow> eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   450
  unfolding at_right_eq by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   451
57275
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   452
lemma trivial_limit_at_right_top: "at_right (top::_::{order_top, linorder_topology}) = bot"
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   453
  unfolding filter_eq_iff eventually_at_topological by auto
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   454
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   455
lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot, linorder_topology}) = bot"
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   456
  unfolding filter_eq_iff eventually_at_topological by auto
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   457
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   458
lemma trivial_limit_at_left_real [simp]:
57275
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   459
  "\<not> trivial_limit (at_left (x::'a::{no_bot, dense_order, linorder_topology}))"
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   460
  using lt_ex[of x]
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   461
  by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   462
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   463
lemma trivial_limit_at_right_real [simp]:
57275
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   464
  "\<not> trivial_limit (at_right (x::'a::{no_top, dense_order, linorder_topology}))"
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   465
  using gt_ex[of x]
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   466
  by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   467
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   468
lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   469
  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   470
           elim: eventually_elim2 eventually_elim1)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   472
lemma eventually_at_split:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   473
  "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   474
  by (subst at_eq_sup_left_right) (simp add: eventually_sup)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   475
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   476
subsubsection \<open>Tendsto\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   477
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   478
abbreviation (in topological_space)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   479
  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   480
  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   481
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   482
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   483
  "Lim A f = (THE l. (f ---> l) A)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   484
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   485
lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   486
  by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   487
57953
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
   488
named_theorems tendsto_intros "introduction rules for tendsto"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   489
setup \<open>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   490
  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
57953
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
   491
    fn context =>
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
   492
      Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
69728243a614 updated to named_theorems;
wenzelm
parents: 57448
diff changeset
   493
      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   494
\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   495
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   496
lemma (in topological_space) tendsto_def:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   497
   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
57276
49c51eeaa623 filters are easier to define with INF on filters.
hoelzl
parents: 57275
diff changeset
   498
   unfolding nhds_def filterlim_INF filterlim_principal by auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   499
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   500
lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   501
  unfolding tendsto_def le_filter_def by fast
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   502
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   503
lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   504
  by (blast intro: tendsto_mono at_le)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   505
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   506
lemma filterlim_at:
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   507
  "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   508
  by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   509
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   510
lemma (in topological_space) topological_tendstoI:
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   511
  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   512
  unfolding tendsto_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   513
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   514
lemma (in topological_space) topological_tendstoD:
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   515
  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   516
  unfolding tendsto_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   517
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   518
lemma (in order_topology) order_tendsto_iff:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   519
  "(f ---> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   520
  unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   521
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   522
lemma (in order_topology) order_tendstoI:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   523
  "(\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F) \<Longrightarrow> (\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F) \<Longrightarrow>
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   524
    (f ---> y) F"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   525
  unfolding order_tendsto_iff by auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   526
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   527
lemma (in order_topology) order_tendstoD:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   528
  assumes "(f ---> y) F"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   529
  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   530
    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   531
  using assms unfolding order_tendsto_iff by auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   532
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   533
lemma tendsto_bot [simp]: "(f ---> a) bot"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   534
  unfolding tendsto_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   535
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   536
lemma (in linorder_topology) tendsto_max:
56949
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   537
  assumes X: "(X ---> x) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   538
  assumes Y: "(Y ---> y) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   539
  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   540
proof (rule order_tendstoI)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   541
  fix a assume "a < max x y"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   542
  then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   543
    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   544
    by (auto simp: less_max_iff_disj elim: eventually_elim1)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   545
next
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   546
  fix a assume "max x y < a"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   547
  then show "eventually (\<lambda>x. max (X x) (Y x) < a) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   548
    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   549
    by (auto simp: eventually_conj_iff)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   550
qed
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   551
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   552
lemma (in linorder_topology) tendsto_min:
56949
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   553
  assumes X: "(X ---> x) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   554
  assumes Y: "(Y ---> y) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   555
  shows "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   556
proof (rule order_tendstoI)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   557
  fix a assume "a < min x y"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   558
  then show "eventually (\<lambda>x. a < min (X x) (Y x)) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   559
    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   560
    by (auto simp: eventually_conj_iff)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   561
next
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   562
  fix a assume "min x y < a"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   563
  then show "eventually (\<lambda>x. min (X x) (Y x) < a) net"
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   564
    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   565
    by (auto simp: min_less_iff_disj elim: eventually_elim1)
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   566
qed
d1a937cbf858 clean up Lebesgue integration
hoelzl
parents: 56524
diff changeset
   567
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57953
diff changeset
   568
lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   569
  unfolding tendsto_def eventually_at_topological by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   570
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57953
diff changeset
   571
lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   572
  by (simp add: tendsto_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   573
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   574
lemma (in t2_space) tendsto_unique:
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   575
  assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   576
  shows "a = b"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   577
proof (rule ccontr)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   578
  assume "a \<noteq> b"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   579
  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   580
    using hausdorff [OF \<open>a \<noteq> b\<close>] by fast
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   581
  have "eventually (\<lambda>x. f x \<in> U) F"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   582
    using \<open>(f ---> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   583
  moreover
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   584
  have "eventually (\<lambda>x. f x \<in> V) F"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   585
    using \<open>(f ---> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   586
  ultimately
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   587
  have "eventually (\<lambda>x. False) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   588
  proof eventually_elim
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   589
    case (elim x)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   590
    hence "f x \<in> U \<inter> V" by simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   591
    with \<open>U \<inter> V = {}\<close> show ?case by simp
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   592
  qed
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   593
  with \<open>\<not> trivial_limit F\<close> show "False"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   594
    by (simp add: trivial_limit_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   595
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   596
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   597
lemma (in t2_space) tendsto_const_iff:
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   598
  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57953
diff changeset
   599
  by (auto intro!: tendsto_unique [OF assms tendsto_const])
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   600
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   601
lemma increasing_tendsto:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   602
  fixes f :: "_ \<Rightarrow> 'a::order_topology"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   603
  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   604
      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   605
  shows "(f ---> l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   606
  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   607
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   608
lemma decreasing_tendsto:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   609
  fixes f :: "_ \<Rightarrow> 'a::order_topology"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   610
  assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   611
      and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   612
  shows "(f ---> l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   613
  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   614
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   615
lemma tendsto_sandwich:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   616
  fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   617
  assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   618
  assumes lim: "(f ---> c) net" "(h ---> c) net"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   619
  shows "(g ---> c) net"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   620
proof (rule order_tendstoI)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   621
  fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   622
    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   623
next
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   624
  fix a show "c < a \<Longrightarrow> eventually (\<lambda>x. g x < a) net"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   625
    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   626
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   627
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   628
lemma tendsto_le:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   629
  fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   630
  assumes F: "\<not> trivial_limit F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   631
  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   632
  assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   633
  shows "y \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   634
proof (rule ccontr)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   635
  assume "\<not> y \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   636
  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} \<inter> {b<..} = {}"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   637
    by (auto simp: not_le)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   638
  then have "eventually (\<lambda>x. f x < a) F" "eventually (\<lambda>x. b < g x) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   639
    using x y by (auto intro: order_tendstoD)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   640
  with ev have "eventually (\<lambda>x. False) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   641
    by eventually_elim (insert xy, fastforce)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   642
  with F show False
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   643
    by (simp add: eventually_False)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   644
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   645
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   646
lemma tendsto_le_const:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   647
  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   648
  assumes F: "\<not> trivial_limit F"
56289
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   649
  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   650
  shows "a \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   651
  using F x tendsto_const a by (rule tendsto_le)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   652
56289
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   653
lemma tendsto_ge_const:
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   654
  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   655
  assumes F: "\<not> trivial_limit F"
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   656
  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   657
  shows "a \<ge> x"
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   658
  by (rule tendsto_le [OF F tendsto_const x a])
d8d2a2b97168 Some useful lemmas
paulson <lp15@cam.ac.uk>
parents: 56231
diff changeset
   659
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   660
subsubsection \<open>Rules about @{const Lim}\<close>
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   661
57276
49c51eeaa623 filters are easier to define with INF on filters.
hoelzl
parents: 57275
diff changeset
   662
lemma tendsto_Lim:
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   663
  "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   664
  unfolding Lim_def using tendsto_unique[of net f] by auto
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   665
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
   666
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   667
  by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   668
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   669
lemma filterlim_at_bot_at_right:
57275
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   670
  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   671
  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   672
  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   673
  assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   674
  assumes P: "eventually P at_bot"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   675
  shows "filterlim f at_bot (at_right a)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   676
proof -
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   677
  from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   678
    unfolding eventually_at_bot_linorder by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   679
  show ?thesis
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   680
  proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   681
    fix z assume "z \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   682
    with x have "P z" by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   683
    have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   684
      using bound[OF bij(2)[OF \<open>P z\<close>]]
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   685
      unfolding eventually_at_right[OF bound[OF bij(2)[OF \<open>P z\<close>]]] by (auto intro!: exI[of _ "g z"])
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   686
    with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   687
      by eventually_elim (metis bij \<open>P z\<close> mono)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   688
  qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   689
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   690
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   691
lemma filterlim_at_top_at_left:
57275
0ddb5b755cdc moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents: 57025
diff changeset
   692
  fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   693
  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   694
  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   695
  assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   696
  assumes P: "eventually P at_top"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   697
  shows "filterlim f at_top (at_left a)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   698
proof -
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   699
  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   700
    unfolding eventually_at_top_linorder by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   701
  show ?thesis
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   702
  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   703
    fix z assume "x \<le> z"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   704
    with x have "P z" by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   705
    have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   706
      using bound[OF bij(2)[OF \<open>P z\<close>]]
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   707
      unfolding eventually_at_left[OF bound[OF bij(2)[OF \<open>P z\<close>]]] by (auto intro!: exI[of _ "g z"])
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   708
    with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   709
      by eventually_elim (metis bij \<open>P z\<close> mono)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   710
  qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   711
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   712
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   713
lemma filterlim_split_at:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   714
  "filterlim f F (at_left x) \<Longrightarrow> filterlim f F (at_right x) \<Longrightarrow> filterlim f F (at (x::'a::linorder_topology))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   715
  by (subst at_eq_sup_left_right) (rule filterlim_sup)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   716
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   717
lemma filterlim_at_split:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   718
  "filterlim f F (at (x::'a::linorder_topology)) \<longleftrightarrow> filterlim f F (at_left x) \<and> filterlim f F (at_right x)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   719
  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   720
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   721
lemma eventually_nhds_top:
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   722
  fixes P :: "'a :: {order_top, linorder_topology} \<Rightarrow> bool"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   723
  assumes "(b::'a) < top"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   724
  shows "eventually P (nhds top) \<longleftrightarrow> (\<exists>b<top. (\<forall>z. b < z \<longrightarrow> P z))"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   725
  unfolding eventually_nhds
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   726
proof safe
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   727
  fix S :: "'a set" assume "open S" "top \<in> S"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   728
  note open_left[OF this \<open>b < top\<close>]
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   729
  moreover assume "\<forall>s\<in>S. P s"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   730
  ultimately show "\<exists>b<top. \<forall>z>b. P z"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   731
    by (auto simp: subset_eq Ball_def)
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   732
next
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   733
  fix b assume "b < top" "\<forall>z>b. P z"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   734
  then show "\<exists>S. open S \<and> top \<in> S \<and> (\<forall>xa\<in>S. P xa)"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   735
    by (intro exI[of _ "{b <..}"]) auto
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
   736
qed
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   737
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   738
lemma tendsto_at_within_iff_tendsto_nhds:
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   739
  "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   740
  unfolding tendsto_def eventually_at_filter eventually_inf_principal
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   741
  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
   742
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   743
subsection \<open>Limits on sequences\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   744
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   745
abbreviation (in topological_space)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   746
  LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   747
    ("((_)/ ----> (_))" [60, 60] 60) where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   748
  "X ----> L \<equiv> (X ---> L) sequentially"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   749
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   750
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   751
  "lim X \<equiv> Lim sequentially X"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   752
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   753
definition (in topological_space) convergent :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   754
  "convergent X = (\<exists>L. X ----> L)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   755
51478
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   756
lemma lim_def: "lim X = (THE L. X ----> L)"
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   757
  unfolding Lim_def ..
270b21f3ae0a move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
hoelzl
parents: 51474
diff changeset
   758
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   759
subsubsection \<open>Monotone sequences and subsequences\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   760
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   761
definition
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   762
  monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   763
    --\<open>Definition of monotonicity.
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   764
        The use of disjunction here complicates proofs considerably.
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   765
        One alternative is to add a Boolean argument to indicate the direction.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   766
        Another is to develop the notions of increasing and decreasing first.\<close>
56020
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   767
  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   768
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   769
abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   770
  "incseq X \<equiv> mono X"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   771
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   772
lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   773
  unfolding mono_def ..
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   774
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   775
abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   776
  "decseq X \<equiv> antimono X"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   777
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   778
lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
f92479477c52 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents: 55945
diff changeset
   779
  unfolding antimono_def ..
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   780
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   781
definition
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   782
  subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   783
    --\<open>Definition of subsequence\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   784
  "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   785
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   786
lemma incseq_SucI:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   787
  "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   788
  using lift_Suc_mono_le[of X]
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   789
  by (auto simp: incseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   790
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   791
lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   792
  by (auto simp: incseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   793
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   794
lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   795
  using incseqD[of A i "Suc i"] by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   796
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   797
lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   798
  by (auto intro: incseq_SucI dest: incseq_SucD)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   799
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   800
lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   801
  unfolding incseq_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   802
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   803
lemma decseq_SucI:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   804
  "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   805
  using order.lift_Suc_mono_le[OF dual_order, of X]
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   806
  by (auto simp: decseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   807
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   808
lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   809
  by (auto simp: decseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   810
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   811
lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   812
  using decseqD[of A i "Suc i"] by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   813
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   814
lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   815
  by (auto intro: decseq_SucI dest: decseq_SucD)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   816
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   817
lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   818
  unfolding decseq_def by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   819
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   820
lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   821
  unfolding monoseq_def incseq_def decseq_def ..
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   822
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   823
lemma monoseq_Suc:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   824
  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   825
  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   826
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   827
lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   828
by (simp add: monoseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   829
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   830
lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   831
by (simp add: monoseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   832
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   833
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   834
by (simp add: monoseq_Suc)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   835
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   836
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   837
by (simp add: monoseq_Suc)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   838
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   839
lemma monoseq_minus:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   840
  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   841
  assumes "monoseq a"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   842
  shows "monoseq (\<lambda> n. - a n)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   843
proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   844
  case True
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   845
  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   846
  thus ?thesis by (rule monoI2)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   847
next
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   848
  case False
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   849
  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using \<open>monoseq a\<close>[unfolded monoseq_def] by auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   850
  thus ?thesis by (rule monoI1)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   851
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   852
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   853
text\<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   854
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   855
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   856
apply (simp add: subseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   857
apply (auto dest!: less_imp_Suc_add)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   858
apply (induct_tac k)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   859
apply (auto intro: less_trans)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   860
done
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   861
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   862
text\<open>for any sequence, there is a monotonic subsequence\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   863
lemma seq_monosub:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   864
  fixes s :: "nat => 'a::linorder"
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   865
  shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   866
proof cases
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   867
  assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   868
  then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   869
    by (intro dependent_nat_choice) (auto simp: conj_commute)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   870
  then obtain f where "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   871
    by (auto simp: subseq_Suc_iff)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   872
  moreover 
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   873
  then have "incseq f"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   874
    unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   875
  then have "monoseq (\<lambda>n. s (f n))"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   876
    by (auto simp add: incseq_def intro!: mono monoI2)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   877
  ultimately show ?thesis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   878
    by auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   879
next
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   880
  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   881
  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   882
  have "\<exists>f. \<forall>n. N < f n \<and> f n < f (Suc n) \<and> s (f n) \<le> s (f (Suc n))"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   883
  proof (intro dependent_nat_choice)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   884
    fix x assume "N < x" with N[of x] show "\<exists>y>N. x < y \<and> s x \<le> s y"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   885
      by (auto intro: less_trans)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   886
  qed auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   887
  then show ?thesis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
   888
    by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   889
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   890
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   891
lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   892
proof(induct n)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   893
  case 0 thus ?case by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   894
next
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   895
  case (Suc n)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   896
  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   897
  have "n < f (Suc n)" by arith
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   898
  thus ?case by arith
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   899
qed
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   900
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   901
lemma eventually_subseq:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   902
  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   903
  unfolding eventually_sequentially by (metis seq_suble le_trans)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   904
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   905
lemma not_eventually_sequentiallyD:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   906
  assumes P: "\<not> eventually P sequentially"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   907
  shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   908
proof -
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   909
  from P have "\<forall>n. \<exists>m\<ge>n. \<not> P m"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   910
    unfolding eventually_sequentially by (simp add: not_less)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   911
  then obtain r where "\<And>n. r n \<ge> n" "\<And>n. \<not> P (r n)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   912
    by (auto simp: choice_iff)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   913
  then show ?thesis
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   914
    by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   915
             simp: less_eq_Suc_le subseq_Suc_iff)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   916
qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
   917
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   918
lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   919
  unfolding filterlim_iff by (metis eventually_subseq)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   920
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   921
lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   922
  unfolding subseq_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   923
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   924
lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   925
  using assms by (auto simp: subseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   926
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   927
lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   928
  by (simp add: incseq_def monoseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   929
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   930
lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   931
  by (simp add: decseq_def monoseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   932
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   933
lemma decseq_eq_incseq:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   934
  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   935
  by (simp add: decseq_def incseq_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   936
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   937
lemma INT_decseq_offset:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   938
  assumes "decseq F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   939
  shows "(\<Inter>i. F i) = (\<Inter>i\<in>{n..}. F i)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   940
proof safe
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   941
  fix x i assume x: "x \<in> (\<Inter>i\<in>{n..}. F i)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   942
  show "x \<in> F i"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   943
  proof cases
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   944
    from x have "x \<in> F n" by auto
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
   945
    also assume "i \<le> n" with \<open>decseq F\<close> have "F n \<subseteq> F i"
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   946
      unfolding decseq_def by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   947
    finally show ?thesis .
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   948
  qed (insert x, simp)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   949
qed auto
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   950
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   951
lemma LIMSEQ_const_iff:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   952
  fixes k l :: "'a::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   953
  shows "(\<lambda>n. k) ----> l \<longleftrightarrow> k = l"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   954
  using trivial_limit_sequentially by (rule tendsto_const_iff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   955
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   956
lemma LIMSEQ_SUP:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   957
  "incseq X \<Longrightarrow> X ----> (SUP i. X i :: 'a :: {complete_linorder, linorder_topology})"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   958
  by (intro increasing_tendsto)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   959
     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   960
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   961
lemma LIMSEQ_INF:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   962
  "decseq X \<Longrightarrow> X ----> (INF i. X i :: 'a :: {complete_linorder, linorder_topology})"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   963
  by (intro decreasing_tendsto)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   964
     (auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   965
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   966
lemma LIMSEQ_ignore_initial_segment:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   967
  "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
51474
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51473
diff changeset
   968
  unfolding tendsto_def
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51473
diff changeset
   969
  by (subst eventually_sequentially_seg[where k=k])
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   970
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   971
lemma LIMSEQ_offset:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   972
  "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
51474
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51473
diff changeset
   973
  unfolding tendsto_def
1e9e68247ad1 generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
hoelzl
parents: 51473
diff changeset
   974
  by (subst (asm) eventually_sequentially_seg[where k=k])
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   975
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   976
lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   977
by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   978
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   979
lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   980
by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   981
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   982
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   983
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   984
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   985
lemma LIMSEQ_unique:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   986
  fixes a b :: "'a::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   987
  shows "\<lbrakk>X ----> a; X ----> b\<rbrakk> \<Longrightarrow> a = b"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   988
  using trivial_limit_sequentially by (rule tendsto_unique)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   989
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   990
lemma LIMSEQ_le_const:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   991
  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   992
  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   993
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   994
lemma LIMSEQ_le:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   995
  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::'a::linorder_topology)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   996
  using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   997
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   998
lemma LIMSEQ_le_const2:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
   999
  "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
58729
e8ecc79aee43 add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents: 57953
diff changeset
  1000
  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1001
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1002
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1003
by (simp add: convergent_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1004
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1005
lemma convergentI: "(X ----> L) ==> convergent X"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1006
by (auto simp add: convergent_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1007
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1008
lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1009
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1010
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1011
lemma convergent_const: "convergent (\<lambda>n. c)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1012
  by (rule convergentI, rule tendsto_const)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1013
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1014
lemma monoseq_le:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1015
  "monoseq a \<Longrightarrow> a ----> (x::'a::linorder_topology) \<Longrightarrow>
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1016
    ((\<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))"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1017
  by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1018
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1019
lemma LIMSEQ_subseq_LIMSEQ:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1020
  "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1021
  unfolding comp_def by (rule filterlim_compose[of X, OF _ filterlim_subseq])
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1022
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1023
lemma convergent_subseq_convergent:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1024
  "\<lbrakk>convergent X; subseq f\<rbrakk> \<Longrightarrow> convergent (X o f)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1025
  unfolding convergent_def by (auto intro: LIMSEQ_subseq_LIMSEQ)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1026
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1027
lemma limI: "X ----> L ==> lim X = L"
57276
49c51eeaa623 filters are easier to define with INF on filters.
hoelzl
parents: 57275
diff changeset
  1028
  by (rule tendsto_Lim) (rule trivial_limit_sequentially)
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1029
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1030
lemma lim_le: "convergent f \<Longrightarrow> (\<And>n. f n \<le> (x::'a::linorder_topology)) \<Longrightarrow> lim f \<le> x"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1031
  using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1032
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1033
subsubsection\<open>Increasing and Decreasing Series\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1034
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1035
lemma incseq_le: "incseq X \<Longrightarrow> X ----> L \<Longrightarrow> X n \<le> (L::'a::linorder_topology)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1036
  by (metis incseq_def LIMSEQ_le_const)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1037
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1038
lemma decseq_le: "decseq X \<Longrightarrow> X ----> L \<Longrightarrow> (L::'a::linorder_topology) \<le> X n"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1039
  by (metis decseq_def LIMSEQ_le_const2)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1040
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1041
subsection \<open>First countable topologies\<close>
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1042
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1043
class first_countable_topology = topological_space +
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1044
  assumes first_countable_basis:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1045
    "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1046
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1047
lemma (in first_countable_topology) countable_basis_at_decseq:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1048
  obtains A :: "nat \<Rightarrow> 'a set" where
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1049
    "\<And>i. open (A i)" "\<And>i. x \<in> (A i)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1050
    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1051
proof atomize_elim
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1052
  from first_countable_basis[of x] obtain A :: "nat \<Rightarrow> 'a set" where
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1053
    nhds: "\<And>i. open (A i)" "\<And>i. x \<in> A i"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1054
    and incl: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>i. A i \<subseteq> S"  by auto
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1055
  def F \<equiv> "\<lambda>n. \<Inter>i\<le>n. A i"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1056
  show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and>
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1057
      (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1058
  proof (safe intro!: exI[of _ F])
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1059
    fix i
51480
3793c3a11378 move connected to HOL image; used to show intermediate value theorem
hoelzl
parents: 51479
diff changeset
  1060
    show "open (F i)" using nhds(1) by (auto simp: F_def)
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1061
    show "x \<in> F i" using nhds(2) by (auto simp: F_def)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1062
  next
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1063
    fix S assume "open S" "x \<in> S"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1064
    from incl[OF this] obtain i where "F i \<subseteq> S" unfolding F_def by auto
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1065
    moreover have "\<And>j. i \<le> j \<Longrightarrow> F j \<subseteq> F i"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1066
      by (auto simp: F_def)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1067
    ultimately show "eventually (\<lambda>i. F i \<subseteq> S) sequentially"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1068
      by (auto simp: eventually_sequentially)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1069
  qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1070
qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1071
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1072
lemma (in first_countable_topology) nhds_countable:
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1073
  obtains X :: "nat \<Rightarrow> 'a set"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1074
  where "decseq X" "\<And>n. open (X n)" "\<And>n. x \<in> X n" "nhds x = (INF n. principal (X n))"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1075
proof -
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1076
  from first_countable_basis obtain A :: "nat \<Rightarrow> 'a set"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1077
    where A: "\<And>n. x \<in> A n" "\<And>n. open (A n)" "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>i. A i \<subseteq> S"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1078
    by metis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1079
  show thesis
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1080
  proof
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1081
    show "decseq (\<lambda>n. \<Inter>i\<le>n. A i)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1082
      by (auto simp: decseq_def)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1083
    show "\<And>n. x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)"
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1084
      using A by auto
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60182
diff changeset
  1085
    show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1086
      using A unfolding nhds_def
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1087
      apply (intro INF_eq)
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1088
      apply simp_all
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1089
      apply force
60585
48fdff264eb2 tuned whitespace;
wenzelm
parents: 60182
diff changeset
  1090
      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
57448
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1091
      apply auto
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1092
      done
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1093
  qed
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1094
qed
159e45728ceb more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents: 57447
diff changeset
  1095
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1096
lemma (in first_countable_topology) countable_basis:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1097
  obtains A :: "nat \<Rightarrow> 'a set" where
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1098
    "\<And>i. open (A i)" "\<And>i. x \<in> A i"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1099
    "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1100
proof atomize_elim
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1101
  obtain A :: "nat \<Rightarrow> 'a set" where A:
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1102
    "\<And>i. open (A i)"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1103
    "\<And>i. x \<in> A i"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1104
    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1105
    by (rule countable_basis_at_decseq) blast
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1106
  {
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1107
    fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1108
    with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1109
      by (auto elim: eventually_elim1 simp: subset_eq)
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1110
  }
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1111
  with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1112
    by (intro exI[of _ A]) (auto simp: tendsto_def)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1113
qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1114
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1115
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1116
  assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1117
  shows "eventually P (inf (nhds a) (principal s))"
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1118
proof (rule ccontr)
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1119
  obtain A :: "nat \<Rightarrow> 'a set" where A:
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1120
    "\<And>i. open (A i)"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1121
    "\<And>i. a \<in> A i"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1122
    "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F ----> a"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1123
    by (rule countable_basis) blast
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1124
  assume "\<not> ?thesis"
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1125
  with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1126
    unfolding eventually_inf_principal eventually_nhds by (intro choice) fastforce
53381
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1127
  then obtain F where F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
355a4cac5440 tuned proofs -- less guessing;
wenzelm
parents: 53374
diff changeset
  1128
    by blast
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1129
  with A have "F ----> a" by auto
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1130
  hence "eventually (\<lambda>n. P (F n)) sequentially"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1131
    using assms F0 by simp
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1132
  thus "False" by (simp add: F3)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1133
qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1134
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1135
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1136
  "eventually P (inf (nhds a) (principal s)) \<longleftrightarrow> 
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1137
    (\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1138
proof (safe intro!: sequentially_imp_eventually_nhds_within)
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1139
  assume "eventually P (inf (nhds a) (principal s))" 
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1140
  then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1141
    by (auto simp: eventually_inf_principal eventually_nhds)
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1142
  moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1143
  ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1144
    by (auto dest!: topological_tendstoD elim: eventually_elim1)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1145
qed
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1146
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1147
lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1148
  "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1149
  using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1150
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1151
lemma tendsto_at_iff_sequentially:
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1152
  fixes f :: "'a :: first_countable_topology \<Rightarrow> _"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1153
  shows "(f ---> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X ----> x \<longrightarrow> ((f \<circ> X) ----> a))"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1154
  unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1155
  by metis
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1156
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1157
subsection \<open>Function limit at a point\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1158
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1159
abbreviation
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1160
  LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1161
        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1162
  "f -- a --> L \<equiv> (f ---> L) (at a)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1163
51481
ef949192e5d6 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents: 51480
diff changeset
  1164
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1165
  unfolding tendsto_def by (simp add: at_within_open[where S=S])
51481
ef949192e5d6 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl
parents: 51480
diff changeset
  1166
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1167
lemma LIM_const_not_eq[tendsto_intros]:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1168
  fixes a :: "'a::perfect_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1169
  fixes k L :: "'b::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1170
  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1171
  by (simp add: tendsto_const_iff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1172
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1173
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1174
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1175
lemma LIM_const_eq:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1176
  fixes a :: "'a::perfect_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1177
  fixes k L :: "'b::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1178
  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1179
  by (simp add: tendsto_const_iff)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1180
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1181
lemma LIM_unique:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1182
  fixes a :: "'a::perfect_space" and L M :: "'b::t2_space"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1183
  shows "f -- a --> L \<Longrightarrow> f -- a --> M \<Longrightarrow> L = M"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1184
  using at_neq_bot by (rule tendsto_unique)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1185
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1186
text \<open>Limits are equal for functions equal except at limit point\<close>
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1187
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1188
lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- a --> l)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1189
  unfolding tendsto_def eventually_at_topological by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1190
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1191
lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- b --> m)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1192
  by (simp add: LIM_equal)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1193
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1194
lemma LIM_cong_limit: "f -- x --> L \<Longrightarrow> K = L \<Longrightarrow> f -- x --> K"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1195
  by simp
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1196
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1197
lemma tendsto_at_iff_tendsto_nhds:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1198
  "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1199
  unfolding tendsto_def eventually_at_filter
51471
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1200
  by (intro ext all_cong imp_cong) (auto elim!: eventually_elim1)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1201
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1202
lemma tendsto_compose:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1203
  "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1204
  unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1205
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1206
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1207
  unfolding o_def by (rule tendsto_compose)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1208
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1209
lemma tendsto_compose_eventually:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1210
  "g -- l --> m \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1211
  by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1212
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1213
lemma LIM_compose_eventually:
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1214
  assumes f: "f -- a --> b"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1215
  assumes g: "g -- b --> c"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1216
  assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1217
  shows "(\<lambda>x. g (f x)) -- a --> c"
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1218
  using g f inj by (rule tendsto_compose_eventually)
cad22a3cc09c move topological_space to its own theory
hoelzl
parents:
diff changeset
  1219
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1220
lemma tendsto_compose_filtermap: "((g \<circ> f) ---> T) F \<longleftrightarrow> (g ---> T) (filtermap f F)"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1221
  by (simp add: filterlim_def filtermap_filtermap comp_def)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1222
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1223
subsubsection \<open>Relation of LIM and LIMSEQ\<close>
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1224
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1225
lemma (in first_countable_topology) sequentially_imp_eventually_within:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1226
  "(\<forall>f. (\<forall>n. f n \<in> s \<and> f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow>
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1227
    eventually P (at a within s)"
51641
cd05e9fcc63d remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents: 51518
diff changeset
  1228
  unfolding at_within_def
51473
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1229
  by (intro sequentially_imp_eventually_nhds_within) auto
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1230
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1231
lemma (in first_countable_topology) sequentially_imp_eventually_at:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1232
  "(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1233
  using assms sequentially_imp_eventually_within [where s=UNIV] by simp
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1234
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1235
lemma LIMSEQ_SEQ_conv1:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1236
  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1237
  assumes f: "f -- a --> l"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1238
  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1239
  using tendsto_compose_eventually [OF f, where F=sequentially] by simp
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1240
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1241
lemma LIMSEQ_SEQ_conv2:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1242
  fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1243
  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. f (S n)) ----> l"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1244
  shows "f -- a --> l"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1245
  using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1246
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1247
lemma LIMSEQ_SEQ_conv:
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1248
  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1249
   (X -- a --> (L::'b::topological_space))"
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1250
  using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
1210309fddab move first_countable_topology to the HOL image
hoelzl
parents: 51471
diff changeset
  1251
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1252
lemma sequentially_imp_eventually_at_left:
60172
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 60150
diff changeset
  1253
  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1254
  assumes b[simp]: "b < a"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1255
  assumes *: "\<And>f. (\<And>n. b < f n) \<Longrightarrow> (\<And>n. f n < a) \<Longrightarrow> incseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1256
  shows "eventually P (at_left a)"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1257
proof (safe intro!: sequentially_imp_eventually_within)
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1258
  fix X assume X: "\<forall>n. X n \<in> {..< a} \<and> X n \<noteq> a" "X ----> a"
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1259
  show "eventually (\<lambda>n. P (X n)) sequentially"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1260
  proof (rule ccontr)
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1261
    assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1262
    have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> b < X (s n)) \<and> (X (s n) \<le> X (s (Suc n)) \<and> Suc (s n) \<le> s (Suc n))"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1263
    proof (rule dependent_nat_choice)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1264
      have "\<not> eventually (\<lambda>n. b < X n \<longrightarrow> P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1265
        by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b])
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1266
      then show "\<exists>x. \<not> P (X x) \<and> b < X x"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1267
        by (auto dest!: not_eventuallyD)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1268
    next
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1269
      fix x n
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1270
      have "\<not> eventually (\<lambda>n. Suc x \<le> n \<longrightarrow> b < X n \<longrightarrow> X x < X n \<longrightarrow> P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1271
        using X by (intro not_eventually_impI order_tendstoD(1)[OF X(2)] eventually_ge_at_top neg) auto
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1272
      then show "\<exists>n. (\<not> P (X n) \<and> b < X n) \<and> (X x \<le> X n \<and> Suc x \<le> n)"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1273
        by (auto dest!: not_eventuallyD)
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1274
    qed
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1275
    then guess s ..
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1276
    then have "\<And>n. b < X (s n)" "\<And>n. X (s n) < a" "incseq (\<lambda>n. X (s n))" "(\<lambda>n. X (s n)) ----> a" "\<And>n. \<not> P (X (s n))"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60720
diff changeset
  1277
      using X by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X ----> a\<close>, unfolded comp_def])
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1278
    from *[OF this(1,2,3,4)] this(5) show False by auto
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1279
  qed
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1280
qed
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1281
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1282
lemma tendsto_at_left_sequentially:
60172
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 60150
diff changeset
  1283
  fixes a :: "_ :: {linorder_topology, first_countable_topology}"
57025
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1284
  assumes "b < a"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1285
  assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S ----> a \<Longrightarrow> (\<lambda>n. X (S n)) ----> L"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1286
  shows "(X ---> L) (at_left a)"
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1287
  using assms unfolding tendsto_def [where l=L]
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1288
  by (simp add: sequentially_imp_eventually_at_left)
e7fd64f82876 add various lemmas
hoelzl
parents: 56949
diff changeset
  1289
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1290
lemma sequentially_imp_eventually_at_right:
60172
423273355b55 rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
hoelzl
parents: 60150
diff changeset
  1291
  fixes a :: "'a :: {linorder_topology, first_countable_topology}"
57447
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1292
  assumes b[simp]: "a < b"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1293
  assumes *: "\<And>f. (\<And>n. a < f n) \<Longrightarrow> (\<And>n. f n < b) \<Longrightarrow> decseq f \<Longrightarrow> f ----> a \<Longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1294
  shows "eventually P (at_right a)"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1295
proof (safe intro!: sequentially_imp_eventually_within)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1296
  fix X assume X: "\<forall>n. X n \<in> {a <..} \<and> X n \<noteq> a" "X ----> a"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1297
  show "eventually (\<lambda>n. P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1298
  proof (rule ccontr)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1299
    assume neg: "\<not> eventually (\<lambda>n. P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1300
    have "\<exists>s. \<forall>n. (\<not> P (X (s n)) \<and> X (s n) < b) \<and> (X (s (Suc n)) \<le> X (s n) \<and> Suc (s n) \<le> s (Suc n))"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1301
    proof (rule dependent_nat_choice)
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1302
      have "\<not> eventually (\<lambda>n. X n < b \<longrightarrow> P (X n)) sequentially"
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents: 57276
diff changeset
  1303
        by (intro not_eventually_impI neg order_tendstoD(2) [OF X(2) b])
87429bdecad5 import more stuff from the CLT proof; base the lborel measure on interval