# Theory Topological_Spaces

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

section ‹Topological Spaces›

theory Topological_Spaces
imports Main
begin

named_theorems continuous_intros "structural introduction rules for continuity"

subsection ‹Topological space›

class "open" =
fixes "open" :: "'a set ⇒ bool"

class topological_space = "open" +
assumes open_UNIV [simp, intro]: "open UNIV"
assumes open_Int [intro]: "open S ⟹ open T ⟹ open (S ∩ T)"
assumes open_Union [intro]: "∀S∈K. open S ⟹ open (⋃K)"
begin

definition closed :: "'a set ⇒ bool"
where "closed S ⟷ open (- S)"

lemma open_empty [continuous_intros, intro, simp]: "open {}"
using open_Union [of "{}"] by simp

lemma open_Un [continuous_intros, intro]: "open S ⟹ open T ⟹ open (S ∪ T)"
using open_Union [of "{S, T}"] by simp

lemma open_UN [continuous_intros, intro]: "∀x∈A. open (B x) ⟹ open (⋃x∈A. B x)"
using open_Union [of "B ` A"] by simp

lemma open_Inter [continuous_intros, intro]: "finite S ⟹ ∀T∈S. open T ⟹ open (⋂S)"
by (induction set: finite) auto

lemma open_INT [continuous_intros, intro]: "finite A ⟹ ∀x∈A. open (B x) ⟹ open (⋂x∈A. B x)"
using open_Inter [of "B ` A"] by simp

lemma openI:
assumes "⋀x. x ∈ S ⟹ ∃T. open T ∧ x ∈ T ∧ T ⊆ S"
shows "open S"
proof -
have "open (⋃{T. open T ∧ T ⊆ S})" by auto
moreover have "⋃{T. open T ∧ T ⊆ S} = S" by (auto dest!: assms)
ultimately show "open S" by simp
qed

lemma open_subopen: "open S ⟷ (∀x∈S. ∃T. open T ∧ x ∈ T ∧ T ⊆ S)"
by (auto intro: openI)

lemma closed_empty [continuous_intros, intro, simp]: "closed {}"
unfolding closed_def by simp

lemma closed_Un [continuous_intros, intro]: "closed S ⟹ closed T ⟹ closed (S ∪ T)"
unfolding closed_def by auto

lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV"
unfolding closed_def by simp

lemma closed_Int [continuous_intros, intro]: "closed S ⟹ closed T ⟹ closed (S ∩ T)"
unfolding closed_def by auto

lemma closed_INT [continuous_intros, intro]: "∀x∈A. closed (B x) ⟹ closed (⋂x∈A. B x)"
unfolding closed_def by auto

lemma closed_Inter [continuous_intros, intro]: "∀S∈K. closed S ⟹ closed (⋂K)"
unfolding closed_def uminus_Inf by auto

lemma closed_Union [continuous_intros, intro]: "finite S ⟹ ∀T∈S. closed T ⟹ closed (⋃S)"
by (induct set: finite) auto

lemma closed_UN [continuous_intros, intro]:
"finite A ⟹ ∀x∈A. closed (B x) ⟹ closed (⋃x∈A. B x)"
using closed_Union [of "B ` A"] by simp

lemma open_closed: "open S ⟷ closed (- S)"

lemma closed_open: "closed S ⟷ open (- S)"
by (rule closed_def)

lemma open_Diff [continuous_intros, intro]: "open S ⟹ closed T ⟹ open (S - T)"
by (simp add: closed_open Diff_eq open_Int)

lemma closed_Diff [continuous_intros, intro]: "closed S ⟹ open T ⟹ closed (S - T)"
by (simp add: open_closed Diff_eq closed_Int)

lemma open_Compl [continuous_intros, intro]: "closed S ⟹ open (- S)"

lemma closed_Compl [continuous_intros, intro]: "open S ⟹ closed (- S)"

lemma open_Collect_neg: "closed {x. P x} ⟹ open {x. ¬ P x}"
unfolding Collect_neg_eq by (rule open_Compl)

lemma open_Collect_conj:
assumes "open {x. P x}" "open {x. Q x}"
shows "open {x. P x ∧ Q x}"
using open_Int[OF assms] by (simp add: Int_def)

lemma open_Collect_disj:
assumes "open {x. P x}" "open {x. Q x}"
shows "open {x. P x ∨ Q x}"
using open_Un[OF assms] by (simp add: Un_def)

lemma open_Collect_ex: "(⋀i. open {x. P i x}) ⟹ open {x. ∃i. P i x}"
using open_UN[of UNIV "λi. {x. P i x}"] unfolding Collect_ex_eq by simp

lemma open_Collect_imp: "closed {x. P x} ⟹ open {x. Q x} ⟹ open {x. P x ⟶ Q x}"
unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)

lemma open_Collect_const: "open {x. P}"
by (cases P) auto

lemma closed_Collect_neg: "open {x. P x} ⟹ closed {x. ¬ P x}"
unfolding Collect_neg_eq by (rule closed_Compl)

lemma closed_Collect_conj:
assumes "closed {x. P x}" "closed {x. Q x}"
shows "closed {x. P x ∧ Q x}"
using closed_Int[OF assms] by (simp add: Int_def)

lemma closed_Collect_disj:
assumes "closed {x. P x}" "closed {x. Q x}"
shows "closed {x. P x ∨ Q x}"
using closed_Un[OF assms] by (simp add: Un_def)

lemma closed_Collect_all: "(⋀i. closed {x. P i x}) ⟹ closed {x. ∀i. P i x}"
using closed_INT[of UNIV "λi. {x. P i x}"] by (simp add: Collect_all_eq)

lemma closed_Collect_imp: "open {x. P x} ⟹ closed {x. Q x} ⟹ closed {x. P x ⟶ Q x}"
unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)

lemma closed_Collect_const: "closed {x. P}"
by (cases P) auto

end

subsection ‹Hausdorff and other separation properties›

class t0_space = topological_space +
assumes t0_space: "x ≠ y ⟹ ∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U)"

class t1_space = topological_space +
assumes t1_space: "x ≠ y ⟹ ∃U. open U ∧ x ∈ U ∧ y ∉ U"

instance t1_space ⊆ t0_space
by standard (fast dest: t1_space)

context t1_space begin

lemma separation_t1: "x ≠ y ⟷ (∃U. open U ∧ x ∈ U ∧ y ∉ U)"
using t1_space[of x y] by blast

lemma closed_singleton [iff]: "closed {a}"
proof -
let ?T = "⋃{S. open S ∧ a ∉ S}"
have "open ?T"
also have "?T = - {a}"
by (auto simp add: set_eq_iff separation_t1)
finally show "closed {a}"
by (simp only: closed_def)
qed

lemma closed_insert [continuous_intros, simp]:
assumes "closed S"
shows "closed (insert a S)"
proof -
from closed_singleton assms have "closed ({a} ∪ S)"
by (rule closed_Un)
then show "closed (insert a S)"
by simp
qed

lemma finite_imp_closed: "finite S ⟹ closed S"
by (induct pred: finite) simp_all

end

text ‹T2 spaces are also known as Hausdorff spaces.›

class t2_space = topological_space +
assumes hausdorff: "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"

instance t2_space ⊆ t1_space
by standard (fast dest: hausdorff)

lemma (in t2_space) separation_t2: "x ≠ y ⟷ (∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {})"
using hausdorff [of x y] by blast

lemma (in t0_space) separation_t0: "x ≠ y ⟷ (∃U. open U ∧ ¬ (x ∈ U ⟷ y ∈ U))"
using t0_space [of x y] by blast

text ‹A classical separation axiom for topological space, the T3 axiom -- also called regularity:
if a point is not in a closed set, then there are open sets separating them.›

class t3_space = t2_space +
assumes t3_space: "closed S ⟹ y ∉ S ⟹ ∃U V. open U ∧ open V ∧ y ∈ U ∧ S ⊆ V ∧ U ∩ V = {}"

text ‹A classical separation axiom for topological space, the T4 axiom -- also called normality:
if two closed sets are disjoint, then there are open sets separating them.›

class t4_space = t2_space +
assumes t4_space: "closed S ⟹ closed T ⟹ S ∩ T = {} ⟹ ∃U V. open U ∧ open V ∧ S ⊆ U ∧ T ⊆ V ∧ U ∩ V = {}"

text ‹T4 is stronger than T3, and weaker than metric.›

instance t4_space ⊆ t3_space
proof
fix S and y::'a assume "closed S" "y ∉ S"
then show "∃U V. open U ∧ open V ∧ y ∈ U ∧ S ⊆ V ∧ U ∩ V = {}"
using t4_space[of "{y}" S] by auto
qed

text ‹A perfect space is a topological space with no isolated points.›

class perfect_space = topological_space +
assumes not_open_singleton: "¬ open {x}"

lemma (in perfect_space) UNIV_not_singleton: "UNIV ≠ {x}"
for x::'a
by (metis (no_types) open_UNIV not_open_singleton)

subsection ‹Generators for toplogies›

inductive generate_topology :: "'a set set ⇒ 'a set ⇒ bool" for S :: "'a set set"
where
UNIV: "generate_topology S UNIV"
| Int: "generate_topology S (a ∩ b)" if "generate_topology S a" and "generate_topology S b"
| UN: "generate_topology S (⋃K)" if "(⋀k. k ∈ K ⟹ generate_topology S k)"
| Basis: "generate_topology S s" if "s ∈ S"

hide_fact (open) UNIV Int UN Basis

lemma generate_topology_Union:
"(⋀k. k ∈ I ⟹ generate_topology S (K k)) ⟹ generate_topology S (⋃k∈I. K k)"
using generate_topology.UN [of "K ` I"] by auto

lemma topological_space_generate_topology: "class.topological_space (generate_topology S)"
by standard (auto intro: generate_topology.intros)

subsection ‹Order topologies›

class order_topology = order + "open" +
assumes open_generated_order: "open = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"
begin

subclass topological_space
unfolding open_generated_order
by (rule topological_space_generate_topology)

lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_lessThan [continuous_intros, simp]: "open {..< a}"
unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}"
unfolding greaterThanLessThan_eq by (simp add: open_Int)

end

class linorder_topology = linorder + order_topology

lemma closed_atMost [continuous_intros, simp]: "closed {..a}"
for a :: "'a::linorder_topology"

lemma closed_atLeast [continuous_intros, simp]: "closed {a..}"
for a :: "'a::linorder_topology"

lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}"
for a b :: "'a::linorder_topology"
proof -
have "{a .. b} = {a ..} ∩ {.. b}"
by auto
then show ?thesis
qed

lemma (in order) less_separate:
assumes "x < y"
shows "∃a b. x ∈ {..< a} ∧ y ∈ {b <..} ∧ {..< a} ∩ {b <..} = {}"
proof (cases "∃z. x < z ∧ z < y")
case True
then obtain z where "x < z ∧ z < y" ..
then have "x ∈ {..< z} ∧ y ∈ {z <..} ∧ {z <..} ∩ {..< z} = {}"
by auto
then show ?thesis by blast
next
case False
with ‹x < y› have "x ∈ {..< y}" "y ∈ {x <..}" "{x <..} ∩ {..< y} = {}"
by auto
then show ?thesis by blast
qed

instance linorder_topology ⊆ t2_space
proof
fix x y :: 'a
show "x ≠ y ⟹ ∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
using less_separate [of x y] less_separate [of y x]
by (elim neqE; metis open_lessThan open_greaterThan Int_commute)
qed

lemma (in linorder_topology) open_right:
assumes "open S" "x ∈ S"
and gt_ex: "x < y"
shows "∃b>x. {x ..< b} ⊆ S"
using assms unfolding open_generated_order
proof induct
case UNIV
then show ?case by blast
next
case (Int A B)
then obtain a b where "a > x" "{x ..< a} ⊆ A"  "b > x" "{x ..< b} ⊆ B"
by auto
then show ?case
by (auto intro!: exI[of _ "min a b"])
next
case UN
then show ?case by blast
next
case Basis
then show ?case
by (fastforce intro: exI[of _ y] gt_ex)
qed

lemma (in linorder_topology) open_left:
assumes "open S" "x ∈ S"
and lt_ex: "y < x"
shows "∃b<x. {b <.. x} ⊆ S"
using assms unfolding open_generated_order
proof induction
case UNIV
then show ?case by blast
next
case (Int A B)
then obtain a b where "a < x" "{a <.. x} ⊆ A"  "b < x" "{b <.. x} ⊆ B"
by auto
then show ?case
by (auto intro!: exI[of _ "max a b"])
next
case UN
then show ?case by blast
next
case Basis
then show ?case
by (fastforce intro: exI[of _ y] lt_ex)
qed

subsection ‹Setup some topologies›

subsubsection ‹Boolean is an order topology›

class discrete_topology = topological_space +
assumes open_discrete: "⋀A. open A"

instance discrete_topology < t2_space
proof
fix x y :: 'a
assume "x ≠ y"
then show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
qed

instantiation bool :: linorder_topology
begin

definition open_bool :: "bool set ⇒ bool"
where "open_bool = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"

instance
by standard (rule open_bool_def)

end

instance bool :: discrete_topology
proof
fix A :: "bool set"
have *: "{False <..} = {True}" "{..< True} = {False}"
by auto
have "A = UNIV ∨ A = {} ∨ A = {False <..} ∨ A = {..< True}"
using subset_UNIV[of A] unfolding UNIV_bool * by blast
then show "open A"
by auto
qed

instantiation nat :: linorder_topology
begin

definition open_nat :: "nat set ⇒ bool"
where "open_nat = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"

instance
by standard (rule open_nat_def)

end

instance nat :: discrete_topology
proof
fix A :: "nat set"
have "open {n}" for n :: nat
proof (cases n)
case 0
moreover have "{0} = {..<1::nat}"
by auto
ultimately show ?thesis
by auto
next
case (Suc n')
then have "{n} = {..<Suc n} ∩ {n' <..}"
by auto
with Suc show ?thesis
by (auto intro: open_lessThan open_greaterThan)
qed
then have "open (⋃a∈A. {a})"
by (intro open_UN) auto
then show "open A"
by simp
qed

instantiation int :: linorder_topology
begin

definition open_int :: "int set ⇒ bool"
where "open_int = generate_topology (range (λa. {..< a}) ∪ range (λa. {a <..}))"

instance
by standard (rule open_int_def)

end

instance int :: discrete_topology
proof
fix A :: "int set"
have "{..<i + 1} ∩ {i-1 <..} = {i}" for i :: int
by auto
then have "open {i}" for i :: int
using open_Int[OF open_lessThan[of "i + 1"] open_greaterThan[of "i - 1"]] by auto
then have "open (⋃a∈A. {a})"
by (intro open_UN) auto
then show "open A"
by simp
qed

subsubsection ‹Topological filters›

definition (in topological_space) nhds :: "'a ⇒ 'a filter"
where "nhds a = (INF S∈{S. open S ∧ a ∈ S}. principal S)"

definition (in topological_space) at_within :: "'a ⇒ 'a set ⇒ 'a filter"
("at (_)/ within (_)" [1000, 60] 60)
where "at a within s = inf (nhds a) (principal (s - {a}))"

abbreviation (in topological_space) at :: "'a ⇒ 'a filter"  ("at")
where "at x ≡ at x within (CONST UNIV)"

abbreviation (in order_topology) at_right :: "'a ⇒ 'a filter"
where "at_right x ≡ at x within {x <..}"

abbreviation (in order_topology) at_left :: "'a ⇒ 'a filter"
where "at_left x ≡ at x within {..< x}"

lemma (in topological_space) nhds_generated_topology:
"open = generate_topology T ⟹ nhds x = (INF S∈{S∈T. x ∈ S}. principal S)"
unfolding nhds_def
proof (safe intro!: antisym INF_greatest)
fix S
assume "generate_topology T S" "x ∈ S"
then show "(INF S∈{S ∈ T. x ∈ S}. principal S) ≤ principal S"
by induct
(auto intro: INF_lower order_trans simp: inf_principal[symmetric] simp del: inf_principal)
qed (auto intro!: INF_lower intro: generate_topology.intros)

lemma (in topological_space) eventually_nhds:
"eventually P (nhds a) ⟷ (∃S. open S ∧ a ∈ S ∧ (∀x∈S. P x))"
unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)

lemma eventually_eventually:
"eventually (λy. eventually P (nhds y)) (nhds x) = eventually P (nhds x)"
by (auto simp: eventually_nhds)

lemma (in topological_space) eventually_nhds_in_open:
"open s ⟹ x ∈ s ⟹ eventually (λy. y ∈ s) (nhds x)"
by (subst eventually_nhds) blast

lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) ⟹ P x"
by (subst (asm) eventually_nhds) blast

lemma (in topological_space) nhds_neq_bot [simp]: "nhds a ≠ bot"

lemma (in t1_space) t1_space_nhds: "x ≠ y ⟹ (∀⇩F x in nhds x. x ≠ y)"
by (drule t1_space) (auto simp: eventually_nhds)

lemma (in topological_space) nhds_discrete_open: "open {x} ⟹ nhds x = principal {x}"
by (auto simp: nhds_def intro!: antisym INF_greatest INF_lower2[of "{x}"])

lemma (in discrete_topology) nhds_discrete: "nhds x = principal {x}"

lemma (in discrete_topology) at_discrete: "at x within S = bot"
unfolding at_within_def nhds_discrete by simp

lemma (in discrete_topology) tendsto_discrete:
"filterlim (f :: 'b ⇒ 'a) (nhds y) F ⟷ eventually (λx. f x = y) F"
by (auto simp: nhds_discrete filterlim_principal)

lemma (in topological_space) at_within_eq:
"at x within s = (INF S∈{S. open S ∧ x ∈ S}. principal (S ∩ s - {x}))"
unfolding nhds_def at_within_def
by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)

lemma (in topological_space) eventually_at_filter:
"eventually P (at a within s) ⟷ eventually (λx. x ≠ a ⟶ x ∈ s ⟶ P x) (nhds a)"
by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)

lemma (in topological_space) at_le: "s ⊆ t ⟹ at x within s ≤ at x within t"
unfolding at_within_def by (intro inf_mono) auto

lemma (in topological_space) eventually_at_topological:
"eventually P (at a within s) ⟷ (∃S. open S ∧ a ∈ S ∧ (∀x∈S. x ≠ a ⟶ x ∈ s ⟶ P x))"

lemma eventually_nhds_conv_at:
"eventually P (nhds x) ⟷ eventually P (at x) ∧ P x"
unfolding eventually_at_topological eventually_nhds by fast

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

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

lemma (in topological_space) at_within_open: "a ∈ S ⟹ open S ⟹ at a within S = at a"
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)

lemma (in topological_space) at_within_open_NO_MATCH:
"a ∈ s ⟹ open s ⟹ NO_MATCH UNIV s ⟹ at a within s = at a"
by (simp only: at_within_open)

lemma (in topological_space) at_within_open_subset:
"a ∈ S ⟹ open S ⟹ S ⊆ T ⟹ at a within T = at a"
by (metis at_le at_within_open dual_order.antisym subset_UNIV)

lemma (in topological_space) at_within_nhd:
assumes "x ∈ S" "open S" "T ∩ S - {x} = U ∩ S - {x}"
shows "at x within T = at x within U"
unfolding filter_eq_iff eventually_at_filter
proof (intro allI eventually_subst)
have "eventually (λx. x ∈ S) (nhds x)"
using ‹x ∈ S› ‹open S› by (auto simp: eventually_nhds)
then show "∀⇩F n in nhds x. (n ≠ x ⟶ n ∈ T ⟶ P n) = (n ≠ x ⟶ n ∈ U ⟶ P n)" for P
by eventually_elim (insert ‹T ∩ S - {x} = U ∩ S - {x}›, blast)
qed

lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
unfolding at_within_def by simp

lemma (in topological_space) at_within_union:
"at x within (S ∪ T) = sup (at x within S) (at x within T)"
unfolding filter_eq_iff eventually_sup eventually_at_filter
by (auto elim!: eventually_rev_mp)

lemma (in topological_space) at_eq_bot_iff: "at a = bot ⟷ open {a}"
unfolding trivial_limit_def eventually_at_topological
by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff)

lemma (in t1_space) eventually_neq_at_within:
"eventually (λw. w ≠ x) (at z within A)"
by (smt (verit, ccfv_threshold) eventually_True eventually_at_topological separation_t1)

lemma (in perfect_space) at_neq_bot [simp]: "at a ≠ bot"

lemma (in order_topology) nhds_order:
"nhds x = inf (INF a∈{x <..}. principal {..< a}) (INF a∈{..< x}. principal {a <..})"
proof -
have 1: "{S ∈ range lessThan ∪ range greaterThan. x ∈ S} =
(λa. {..< a}) ` {x <..} ∪ (λa. {a <..}) ` {..< x}"
by auto
show ?thesis
by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
qed

lemma (in topological_space) filterlim_at_within_If:
assumes "filterlim f G (at x within (A ∩ {x. P x}))"
and "filterlim g G (at x within (A ∩ {x. ¬P x}))"
shows "filterlim (λx. if P x then f x else g x) G (at x within A)"
proof (rule filterlim_If)
note assms(1)
also have "at x within (A ∩ {x. P x}) = inf (nhds x) (principal (A ∩ Collect P - {x}))"
also have "A ∩ Collect P - {x} = (A - {x}) ∩ Collect P"
by blast
also have "inf (nhds x) (principal …) = inf (at x within A) (principal (Collect P))"
finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" .
next
note assms(2)
also have "at x within (A ∩ {x. ¬ P x}) = inf (nhds x) (principal (A ∩ {x. ¬ P x} - {x}))"
also have "A ∩ {x. ¬ P x} - {x} = (A - {x}) ∩ {x. ¬ P x}"
by blast
also have "inf (nhds x) (principal …) = inf (at x within A) (principal {x. ¬ P x})"
finally show "filterlim g G (inf (at x within A) (principal {x. ¬ P x}))" .
qed

lemma (in topological_space) filterlim_at_If:
assumes "filterlim f G (at x within {x. P x})"
and "filterlim g G (at x within {x. ¬P x})"
shows "filterlim (λx. if P x then f x else g x) G (at x)"
using assms by (intro filterlim_at_within_If) simp_all
lemma (in linorder_topology) at_within_order:
assumes "UNIV ≠ {x}"
shows "at x within s =
inf (INF a∈{x <..}. principal ({..< a} ∩ s - {x}))
(INF a∈{..< x}. principal ({a <..} ∩ s - {x}))"
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split])
case True_True
have "UNIV = {..< x} ∪ {x} ∪ {x <..}"
by auto
with assms True_True show ?thesis
by auto
qed (auto simp del: inf_principal simp: at_within_def nhds_order Int_Diff
inf_principal[symmetric] INF_inf_const2 inf_sup_aci[where 'a="'a filter"])

lemma (in linorder_topology) at_left_eq:
"y < x ⟹ at_left x = (INF a∈{..< x}. principal {a <..< x})"
by (subst at_within_order)
(auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
intro!: INF_lower2 inf_absorb2)

lemma (in linorder_topology) eventually_at_left:
"y < x ⟹ eventually P (at_left x) ⟷ (∃b<x. ∀y>b. y < x ⟶ P y)"
unfolding at_left_eq
by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)

lemma (in linorder_topology) at_right_eq:
"x < y ⟹ at_right x = (INF a∈{x <..}. principal {x <..< a})"
by (subst at_within_order)
(auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
intro!: INF_lower2 inf_absorb1)

lemma (in linorder_topology) eventually_at_right:
"x < y ⟹ eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y < b ⟶ P y)"
unfolding at_right_eq
by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)

lemma eventually_at_right_less: "∀⇩F y in at_right (x::'a::{linorder_topology, no_top}). x < y"
using gt_ex[of x] eventually_at_right[of x] by auto

lemma trivial_limit_at_right_top: "at_right (top::_::{order_top,linorder_topology}) = bot"
by (auto simp: filter_eq_iff eventually_at_topological)

lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot,linorder_topology}) = bot"
by (auto simp: filter_eq_iff eventually_at_topological)

lemma trivial_limit_at_left_real [simp]: "¬ trivial_limit (at_left x)"
for x :: "'a::{no_bot,dense_order,linorder_topology}"
using lt_ex [of x]
by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)

lemma trivial_limit_at_right_real [simp]: "¬ trivial_limit (at_right x)"
for x :: "'a::{no_top,dense_order,linorder_topology}"
using gt_ex[of x]
by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)

lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
elim: eventually_elim2 eventually_mono)

lemma (in linorder_topology) eventually_at_split:
"eventually P (at x) ⟷ eventually P (at_left x) ∧ eventually P (at_right x)"
by (subst at_eq_sup_left_right) (simp add: eventually_sup)

lemma (in order_topology) eventually_at_leftI:
assumes "⋀x. x ∈ {a<..<b} ⟹ P x" "a < b"
shows   "eventually P (at_left b)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto

lemma (in order_topology) eventually_at_rightI:
assumes "⋀x. x ∈ {a<..<b} ⟹ P x" "a < b"
shows   "eventually P (at_right a)"
using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto

lemma eventually_filtercomap_nhds:
"eventually P (filtercomap f (nhds x)) ⟷ (∃S. open S ∧ x ∈ S ∧ (∀x. f x ∈ S ⟶ P x))"
unfolding eventually_filtercomap eventually_nhds by auto

lemma eventually_filtercomap_at_topological:
"eventually P (filtercomap f (at A within B)) ⟷
(∃S. open S ∧ A ∈ S ∧ (∀x. f x ∈ S ∩ B - {A} ⟶ P x))" (is "?lhs = ?rhs")
unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal
eventually_filtercomap_nhds eventually_principal by blast

lemma eventually_at_right_field:
"eventually P (at_right x) ⟷ (∃b>x. ∀y>x. y < b ⟶ P y)"
for x :: "'a::{linordered_field, linorder_topology}"
using linordered_field_no_ub[rule_format, of x]
by (auto simp: eventually_at_right)

lemma eventually_at_left_field:
"eventually P (at_left x) ⟷ (∃b<x. ∀y>b. y < x ⟶ P y)"
for x :: "'a::{linordered_field, linorder_topology}"
using linordered_field_no_lb[rule_format, of x]
by (auto simp: eventually_at_left)

lemma filtermap_nhds_eq_imp_filtermap_at_eq:
assumes "filtermap f (nhds z) = nhds (f z)"
assumes "eventually (λx. f x = f z ⟶ x = z) (at z)"
shows   "filtermap f (at z) = at (f z)"
proof (rule filter_eqI)
fix P :: "'a ⇒ bool"
have "eventually P (filtermap f (at z)) ⟷ (∀⇩F x in nhds z. x ≠ z ⟶ P (f x))"
also have "… ⟷ (∀⇩F x in nhds z. f x ≠ f z ⟶ P (f x))"
by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
also have "… ⟷ (∀⇩F x in filtermap f (nhds z). x ≠ f z ⟶ P x)"
also have "filtermap f (nhds z) = nhds (f z)"
by (rule assms)
also have "(∀⇩F x in nhds (f z). x ≠ f z ⟶ P x) ⟷ (∀⇩F x in at (f z). P x)"
finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
qed

subsubsection ‹Tendsto›

abbreviation (in topological_space)
tendsto :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b filter ⇒ bool"  (infixr "⤏" 55)
where "(f ⤏ l) F ≡ filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter ⇒ ('f ⇒ 'a) ⇒ 'a"
where "Lim A f = (THE l. (f ⤏ l) A)"

lemma (in topological_space) tendsto_eq_rhs: "(f ⤏ x) F ⟹ x = y ⟹ (f ⤏ y) F"
by simp

named_theorems tendsto_intros "introduction rules for tendsto"
setup ‹
fn context =>
Named_Theorems.get (Context.proof_of context) \<^named_theorems>‹tendsto_intros›
|> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
›

context topological_space begin

lemma tendsto_def:
"(f ⤏ l) F ⟷ (∀S. open S ⟶ l ∈ S ⟶ eventually (λx. f x ∈ S) F)"
unfolding nhds_def filterlim_INF filterlim_principal by auto

lemma tendsto_cong: "(f ⤏ c) F ⟷ (g ⤏ c) F" if "eventually (λx. f x = g x) F"
by (rule filterlim_cong [OF refl refl that])

lemma tendsto_mono: "F ≤ F' ⟹ (f ⤏ l) F' ⟹ (f ⤏ l) F"
unfolding tendsto_def le_filter_def by fast

lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((λx. x) ⤏ a) (at a within s)"
by (auto simp: tendsto_def eventually_at_topological)

lemma tendsto_const [tendsto_intros, simp, intro]: "((λx. k) ⤏ k) F"

lemma filterlim_at:
"(LIM x F. f x :> at b within s) ⟷ eventually (λx. f x ∈ s ∧ f x ≠ b) F ∧ (f ⤏ b) F"
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)

lemma (in -)
assumes "filterlim f (nhds L) F"
shows tendsto_imp_filterlim_at_right:
"eventually (λx. f x > L) F ⟹ filterlim f (at_right L) F"
and tendsto_imp_filterlim_at_left:
"eventually (λx. f x < L) F ⟹ filterlim f (at_left L) F"
using assms by (auto simp: filterlim_at elim: eventually_mono)

lemma  filterlim_at_withinI:
assumes "filterlim f (nhds c) F"
assumes "eventually (λx. f x ∈ A - {c}) F"
shows   "filterlim f (at c within A) F"
using assms by (simp add: filterlim_at)

lemma filterlim_atI:
assumes "filterlim f (nhds c) F"
assumes "eventually (λx. f x ≠ c) F"
shows   "filterlim f (at c) F"
using assms by (intro filterlim_at_withinI) simp_all

lemma topological_tendstoI:
"(⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F) ⟹ (f ⤏ l) F"
by (auto simp: tendsto_def)

lemma topological_tendstoD:
"(f ⤏ l) F ⟹ open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F"
by (auto simp: tendsto_def)

lemma tendsto_bot [simp]: "(f ⤏ a) bot"

lemma tendsto_eventually: "eventually (λx. f x = l) net ⟹ ((λx. f x) ⤏ l) net"
by (rule topological_tendstoI) (auto elim: eventually_mono)

(* Contributed by Dominique Unruh *)
lemma tendsto_principal_singleton[simp]:
shows "(f ⤏ f x) (principal {x})"
unfolding tendsto_def eventually_principal by simp

end

lemma (in topological_space) filterlim_within_subset:
"filterlim f l (at x within S) ⟹ T ⊆ S ⟹ filterlim f l (at x within T)"
by (blast intro: filterlim_mono at_le)

lemmas tendsto_within_subset = filterlim_within_subset

lemma (in order_topology) order_tendsto_iff:
"(f ⤏ x) F ⟷ (∀l<x. eventually (λx. l < f x) F) ∧ (∀u>x. eventually (λx. f x < u) F)"
by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)

lemma (in order_topology) order_tendstoI:
"(⋀a. a < y ⟹ eventually (λx. a < f x) F) ⟹ (⋀a. y < a ⟹ eventually (λx. f x < a) F) ⟹
(f ⤏ y) F"
by (auto simp: order_tendsto_iff)

lemma (in order_topology) order_tendstoD:
assumes "(f ⤏ y) F"
shows "a < y ⟹ eventually (λx. a < f x) F"
and "y < a ⟹ eventually (λx. f x < a) F"
using assms by (auto simp: order_tendsto_iff)

lemma (in linorder_topology) tendsto_max[tendsto_intros]:
assumes X: "(X ⤏ x) net"
and Y: "(Y ⤏ y) net"
shows "((λx. max (X x) (Y x)) ⤏ max x y) net"
proof (rule order_tendstoI)
fix a
assume "a < max x y"
then show "eventually (λx. a < max (X x) (Y x)) net"
using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
by (auto simp: less_max_iff_disj elim: eventually_mono)
next
fix a
assume "max x y < a"
then show "eventually (λx. max (X x) (Y x) < a) net"
using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
by (auto simp: eventually_conj_iff)
qed

lemma (in linorder_topology) tendsto_min[tendsto_intros]:
assumes X: "(X ⤏ x) net"
and Y: "(Y ⤏ y) net"
shows "((λx. min (X x) (Y x)) ⤏ min x y) net"
proof (rule order_tendstoI)
fix a
assume "a < min x y"
then show "eventually (λx. a < min (X x) (Y x)) net"
using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
by (auto simp: eventually_conj_iff)
next
fix a
assume "min x y < a"
then show "eventually (λx. min (X x) (Y x) < a) net"
using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
by (auto simp: min_less_iff_disj elim: eventually_mono)
qed

lemma (in order_topology)
assumes "a < b"
shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
by (auto intro!: order_class.order_antisym filter_leI
simp: eventually_at_filter less_le
elim: eventually_elim2)

lemma (in order_topology)
shows at_within_Ici_at_right: "at a within {a..} = at_right a"
and at_within_Iic_at_left:  "at a within {..a} = at_left a"
using order_tendstoD(2)[OF tendsto_ident_at [where s = "{a<..}"]]
using order_tendstoD(1)[OF tendsto_ident_at[where s = "{..<a}"]]
by (auto intro!: order_class.order_antisym filter_leI
simp: eventually_at_filter less_le
elim: eventually_elim2)

lemma (in order_topology) at_within_Icc_at: "a < x ⟹ x < b ⟹ at x within {a..b} = at x"
by (rule at_within_open_subset[where S="{a<..<b}"]) auto

lemma (in t2_space) tendsto_unique:
assumes "F ≠ bot"
and "(f ⤏ a) F"
and "(f ⤏ b) F"
shows "a = b"
proof (rule ccontr)
assume "a ≠ b"
obtain U V where "open U" "open V" "a ∈ U" "b ∈ V" "U ∩ V = {}"
using hausdorff [OF ‹a ≠ b›] by fast
have "eventually (λx. f x ∈ U) F"
using ‹(f ⤏ a) F› ‹open U› ‹a ∈ U› by (rule topological_tendstoD)
moreover
have "eventually (λx. f x ∈ V) F"
using ‹(f ⤏ b) F› ‹open V› ‹b ∈ V› by (rule topological_tendstoD)
ultimately
have "eventually (λx. False) F"
proof eventually_elim
case (elim x)
then have "f x ∈ U ∩ V" by simp
with ‹U ∩ V = {}› show ?case by simp
qed
with ‹¬ trivial_limit F› show "False"
qed

lemma (in t2_space) tendsto_const_iff:
fixes a b :: 'a
assumes "¬ trivial_limit F"
shows "((λx. a) ⤏ b) F ⟷ a = b"
by (auto intro!: tendsto_unique [OF assms tendsto_const])

lemma (in t2_space) tendsto_unique':
assumes "F ≠ bot"
shows "∃⇩≤⇩1l. (f ⤏ l) F"
using Uniq_def assms local.tendsto_unique by fastforce

lemma Lim_in_closed_set:
assumes "closed S" "eventually (λx. f(x) ∈ S) F" "F ≠ bot" "(f ⤏ l) F"
shows "l ∈ S"
proof (rule ccontr)
assume "l ∉ S"
with ‹closed S› have "open (- S)" "l ∈ - S"
with assms(4) have "eventually (λx. f x ∈ - S) F"
by (rule topological_tendstoD)
with assms(2) have "eventually (λx. False) F"
by (rule eventually_elim2) simp
with assms(3) show "False"
qed

lemma (in t3_space) nhds_closed:
assumes "x ∈ A" and "open A"
shows   "∃A'. x ∈ A' ∧ closed A' ∧ A' ⊆ A ∧ eventually (λy. y ∈ A') (nhds x)"
proof -
from assms have "∃U V. open U ∧ open V ∧ x ∈ U ∧ - A ⊆ V ∧ U ∩ V = {}"
by (intro t3_space) auto
then obtain U V where UV: "open U" "open V" "x ∈ U" "-A ⊆ V" "U ∩ V = {}"
by auto
have "eventually (λy. y ∈ U) (nhds x)"
using ‹open U› and ‹x ∈ U› by (intro eventually_nhds_in_open)
hence "eventually (λy. y ∈ -V) (nhds x)"
by eventually_elim (use UV in auto)
with UV show ?thesis by (intro exI[of _ "-V"]) auto
qed

lemma (in order_topology) increasing_tendsto:
assumes bdd: "eventually (λn. f n ≤ l) F"
and en: "⋀x. x < l ⟹ eventually (λn. x < f n) F"
shows "(f ⤏ l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)

lemma (in order_topology) decreasing_tendsto:
assumes bdd: "eventually (λn. l ≤ f n) F"
and en: "⋀x. l < x ⟹ eventually (λn. f n < x) F"
shows "(f ⤏ l) F"
using assms by (intro order_tendstoI) (auto elim!: eventually_mono)

lemma (in order_topology) tendsto_sandwich:
assumes ev: "eventually (λn. f n ≤ g n) net" "eventually (λn. g n ≤ h n) net"
assumes lim: "(f ⤏ c) net" "(h ⤏ c) net"
shows "(g ⤏ c) net"
proof (rule order_tendstoI)
fix a
show "a < c ⟹ eventually (λx. a < g x) net"
using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
next
fix a
show "c < a ⟹ eventually (λx. g x < a) net"
using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed

lemma (in t1_space) limit_frequently_eq:
assumes "F ≠ bot"
and "frequently (λx. f x = c) F"
and "(f ⤏ d) F"
shows "d = c"
proof (rule ccontr)
assume "d ≠ c"
from t1_space[OF this] obtain U where "open U" "d ∈ U" "c ∉ U"
by blast
with assms have "eventually (λx. f x ∈ U) F"
unfolding tendsto_def by blast
then have "eventually (λx. f x ≠ c) F"
by eventually_elim (insert ‹c ∉ U›, blast)
with assms(2) show False
qed

lemma (in t1_space) tendsto_imp_eventually_ne:
assumes  "(f ⤏ c) F" "c ≠ c'"
shows "eventually (λz. f z ≠ c') F"
proof (cases "F=bot")
case True
thus ?thesis by auto
next
case False
show ?thesis
proof (rule ccontr)
assume "¬ eventually (λz. f z ≠ c') F"
then have "frequently (λz. f z = c') F"
from limit_frequently_eq[OF False this ‹(f ⤏ c) F›] and ‹c ≠ c'› show False
qed
qed

lemma (in linorder_topology) tendsto_le:
assumes F: "¬ trivial_limit F"
and x: "(f ⤏ x) F"
and y: "(g ⤏ y) F"
and ev: "eventually (λx. g x ≤ f x) F"
shows "y ≤ x"
proof (rule ccontr)
assume "¬ y ≤ x"
with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a} ∩ {b<..} = {}"
by (auto simp: not_le)
then have "eventually (λx. f x < a) F" "eventually (λx. b < g x) F"
using x y by (auto intro: order_tendstoD)
with ev have "eventually (λx. False) F"
by eventually_elim (insert xy, fastforce)
with F show False
qed

lemma (in linorder_topology) tendsto_lowerbound:
assumes x: "(f ⤏ x) F"
and ev: "eventually (λi. a ≤ f i) F"
and F: "¬ trivial_limit F"
shows "a ≤ x"
using F x tendsto_const ev by (rule tendsto_le)

lemma (in linorder_topology) tendsto_upperbound:
assumes x: "(f ⤏ x) F"
and ev: "eventually (λi. a ≥ f i) F"
and F: "¬ trivial_limit F"
shows "a ≥ x"
by (rule tendsto_le [OF F tendsto_const x ev])

lemma filterlim_at_within_not_equal:
fixes f::"'a ⇒ 'b::t2_space"
assumes "filterlim f (at a within s) F"
shows "eventually (λw. f w∈s ∧ f w ≠b) F"
proof (cases "a=b")
case True
then show ?thesis using assms by (simp add: filterlim_at)
next
case False
from hausdorff[OF this] obtain U V where UV:"open U" "open V" "a ∈ U" "b ∈ V" "U ∩ V = {}"
by auto
have "(f ⤏ a) F" using assms filterlim_at by auto
then have "∀⇩F x in F. f x ∈ U" using UV unfolding tendsto_def by auto
moreover have  "∀⇩F x in F. f x ∈ s ∧ f x≠a" using assms filterlim_at by auto
ultimately show ?thesis
apply eventually_elim
using UV by auto
qed

lemma tendsto_Lim: "¬ trivial_limit net ⟹ (f ⤏ l) net ⟹ Lim net f = l"
unfolding Lim_def using tendsto_unique [of net f] by auto

lemma Lim_ident_at: "¬ trivial_limit (at x within s) ⟹ Lim (at x within s) (λx. x) = x"

lemma Lim_cong:
assumes "∀⇩F x in F. f x = g x" "F = G"
shows "Lim F f = Lim F g"
unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce

lemma eventually_Lim_ident_at:
"(∀⇩F y in at x within X. P (Lim (at x within X) (λx. x)) y) ⟷
(∀⇩F y in at x within X. P x y)" for x::"'a::t2_space"
by (cases "at x within X = bot") (auto simp: Lim_ident_at)

lemma filterlim_at_bot_at_right:
fixes f :: "'a::linorder_topology ⇒ 'b::linorder"
assumes mono: "⋀x y. Q x ⟹ Q y ⟹ x ≤ y ⟹ f x ≤ f y"
and bij: "⋀x. P x ⟹ f (g x) = x" "⋀x. P x ⟹ Q (g x)"
and Q: "eventually Q (at_right a)"
and bound: "⋀b. Q b ⟹ a < b"
and P: "eventually P at_bot"
shows "filterlim f at_bot (at_right a)"
proof -
from P obtain x where x: "⋀y. y ≤ x ⟹ P y"
unfolding eventually_at_bot_linorder by auto
show ?thesis
proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
fix z
assume "z ≤ x"
with x have "P z" by auto
have "eventually (λx. x ≤ g z) (at_right a)"
using bound[OF bij(2)[OF ‹P z›]]
unfolding eventually_at_right[OF bound[OF bij(2)[OF ‹P z›]]]
by (auto intro!: exI[of _ "g z"])
with Q show "eventually (λx. f x ≤ z) (at_right a)"
by eventually_elim (metis bij ‹P z› mono)
qed
qed

lemma filterlim_at_top_at_left:
fixes f :: "'a::linorder_topology ⇒ 'b::linorder"
assumes mono: "⋀x y. Q x ⟹ Q y ⟹ x ≤ y ⟹ f x ≤ f y"
and bij: "⋀x. P x ⟹ f (g x) = x" "⋀x. P x ⟹ Q (g x)"
and Q: "eventually Q (at_left a)"
and bound: "⋀b. Q b ⟹ b < a"
and P: "eventually P at_top"
shows "filterlim f at_top (at_left a)"
proof -
from P obtain x where x: "⋀y. x ≤ y ⟹ P y"
unfolding eventually_at_top_linorder by auto
show ?thesis
proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
fix z
assume "x ≤ z"
with x have "P z" by auto
have "eventually (λx. g z ≤ x) (at_left a)"
using bound[OF bij(2)[OF ‹P z›]]
unfolding eventually_at_left[OF bound[OF bij(2)[OF ‹P z›]]]
by (auto intro!: exI[of _ "g z"])
with Q show "eventually (λx. z ≤ f x) (at_left a)"
by eventually_elim (metis bij ‹P z› mono)
qed
qed

lemma filterlim_split_at:
"filterlim f F (at_left x) ⟹ filterlim f F (at_right x) ⟹
filterlim f F (at x)"
for x :: "'a::linorder_topology"
by (subst at_eq_sup_left_right) (rule filterlim_sup)

lemma filterlim_at_split:
"filterlim f F (at x) ⟷ filterlim f F (at_left x) ∧ filterlim f F (at_right x)"
for x :: "'a::linorder_topology"
by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)

lemma eventually_nhds_top:
fixes P :: "'a :: {order_top,linorder_topology} ⇒ bool"
and b :: 'a
assumes "b < top"
shows "eventually P (nhds top) ⟷ (∃b<top. (∀z. b < z ⟶ P z))"
unfolding eventually_nhds
proof safe
fix S :: "'a set"
assume "open S" "top ∈ S"
note open_left[OF this ‹b < top›]
moreover assume "∀s∈S. P s"
ultimately show "∃b<top. ∀z>b. P z"
by (auto simp: subset_eq Ball_def)
next
fix b
assume "b < top" "∀z>b. P z"
then show "∃S. open S ∧ top ∈ S ∧ (∀xa∈S. P xa)"
by (intro exI[of _ "{b <..}"]) auto
qed

lemma tendsto_at_within_iff_tendsto_nhds:
"(g ⤏ g l) (at l within S) ⟷ (g ⤏ g l) (inf (nhds l) (principal S))"
unfolding tendsto_def eventually_at_filter eventually_inf_principal
by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)

subsection ‹Limits on sequences›

abbreviation (in topological_space)
LIMSEQ :: "[nat ⇒ 'a, 'a] ⇒ bool"  ("((_)/ ⇢ (_))" [60, 60] 60)
where "X ⇢ L ≡ (X ⤏ L) sequentially"

abbreviation (in t2_space) lim :: "(nat ⇒ 'a) ⇒ 'a"
where "lim X ≡ Lim sequentially X"

definition (in topological_space) convergent :: "(nat ⇒ 'a) ⇒ bool"
where "convergent X = (∃L. X ⇢ L)"

lemma lim_def: "lim X = (THE L. X ⇢ L)"
unfolding Lim_def ..

lemma lim_explicit:
"f ⇢ f0 ⟷ (∀S. open S ⟶ f0 ∈ S ⟶ (∃N. ∀n≥N. f n ∈ S))"
unfolding tendsto_def eventually_sequentially by auto

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

subsection ‹Monotone sequences and subsequences›

text ‹
Definition of monotonicity.
The use of disjunction here complicates proofs considerably.
One alternative is to add a Boolean argument to indicate the direction.
Another is to develop the notions of increasing and decreasing first.
›
definition monoseq :: "(nat ⇒ 'a::order) ⇒ bool"
where "monoseq X ⟷ (∀m. ∀n≥m. X m ≤ X n) ∨ (∀m. ∀n≥m. X n ≤ X m)"

abbreviation incseq :: "(nat ⇒ 'a::order) ⇒ bool"
where "incseq X ≡ mono X"

lemma incseq_def: "incseq X ⟷ (∀m. ∀n≥m. X n ≥ X m)"
unfolding mono_def ..

abbreviation decseq :: "(nat ⇒ 'a::order) ⇒ bool"
where "decseq X ≡ antimono X"

lemma decseq_def: "decseq X ⟷ (∀m. ∀n≥m. X n ≤ X m)"
unfolding antimono_def ..

subsubsection ‹Definition of subsequence.›

(* For compatibility with the old "subseq" *)
lemma strict_mono_leD: "strict_mono r ⟹ m ≤ n ⟹ r m ≤ r n"
by (erule (1) monoD [OF strict_mono_mono])

lemma strict_mono_id: "strict_mono id"

lemma incseq_SucI: "(⋀n. X n ≤ X (Suc n)) ⟹ incseq X"

lemma incseqD: "incseq f ⟹ i ≤ j ⟹ f i ≤ f j"
by (auto simp: incseq_def)

lemma incseq_SucD: "incseq A ⟹ A i ≤ A (Suc i)"
using incseqD[of A i "Suc i"] by auto

lemma incseq_Suc_iff: "incseq f ⟷ (∀n. f n ≤ f (Suc n))"
by (auto intro: incseq_SucI dest: incseq_SucD)

lemma incseq_const[simp, intro]: "incseq (λx. k)"
unfolding incseq_def by auto

lemma decseq_SucI: "(⋀n. X (Suc n) ≤ X n) ⟹ decseq X"

lemma decseqD: "decseq f ⟹ i ≤ j ⟹ f j ≤ f i"
by (auto simp: decseq_def)

lemma decseq_SucD: "decseq A ⟹ A (Suc i) ≤ A i"
using decseqD[of A i "Suc i"] by auto

lemma decseq_Suc_iff: "decseq f ⟷ (∀n. f (Suc n) ≤ f n)"
by (auto intro: decseq_SucI dest: decseq_SucD)

lemma decseq_const[simp, intro]: "decseq (λx. k)"
unfolding decseq_def by auto

lemma monoseq_iff: "monoseq X ⟷ incseq X ∨ decseq X"
unfolding monoseq_def incseq_def decseq_def ..

lemma monoseq_Suc: "monoseq X ⟷ (∀n. X n ≤ X (Suc n)) ∨ (∀n. X (Suc n) ≤ X n)"
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..

lemma monoI1: "∀m. ∀n ≥ m. X m ≤ X n ⟹ monoseq X"

lemma monoI2: "∀m. ∀n ≥ m. X n ≤ X m ⟹ monoseq X"

lemma mono_SucI1: "∀n. X n ≤ X (Suc n) ⟹ monoseq X"

lemma mono_SucI2: "∀n. X (Suc n) ≤ X n ⟹ monoseq X"

lemma monoseq_minus:
fixes a :: "nat ⇒ 'a::ordered_ab_group_add"
assumes "monoseq a"
shows "monoseq (λ n. - a n)"
proof (cases "∀m. ∀n ≥ m. a m ≤ a n")
case True
then have "∀m. ∀n ≥ m. - a n ≤ - a m" by auto
then show ?thesis by (rule monoI2)
next
case False
then have "∀m. ∀n ≥ m. - a m ≤ - a n"
using ‹monoseq a›[unfolded monoseq_def] by auto
then show ?thesis by (rule monoI1)
qed

subsubsection ‹Subsequence (alternative definition, (e.g. Hoskins)›

text ‹For any sequence, there is a monotonic subsequence.›
lemma seq_monosub:
fixes s :: "nat ⇒ 'a::linorder"
shows "∃f. strict_mono f ∧ monoseq (λn. (s (f n)))"
proof (cases "∀n. ∃p>n. ∀m≥p. s m ≤ s p")
case True
then have "∃f. ∀n. (∀m≥f n. s m ≤ s (f n)) ∧ f n < f (Suc n)"
by (intro dependent_nat_choice) (auto simp: conj_commute)
then obtain f :: "nat ⇒ nat"
where f: "strict_mono f" and mono: "⋀n m. f n ≤ m ⟹ s m ≤ s (f n)"
by (auto simp: strict_mono_Suc_iff)
then have "incseq f"
unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
then have "monoseq (λn. s (f n))"
by (auto simp add: incseq_def intro!: mono monoI2)
with f show ?thesis
by auto
next
case False
then obtain N where N: "p > N ⟹ ∃m>p. s p < s m" for p
by (force simp: not_le le_less)
have "∃f. ∀n. N < f n ∧ f n < f (Suc n) ∧ s (f n) ≤ s (f (Suc n))"
proof (intro dependent_nat_choice)
fix x
assume "N < x" with N[of x]
show "∃y>N. x < y ∧ s x ≤ s y"
by (auto intro: less_trans)
qed auto
then show ?thesis
by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff)
qed

lemma seq_suble:
assumes sf: "strict_mono (f :: nat ⇒ nat)"
shows "n ≤ f n"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)"
by arith
then show ?case by arith
qed

lemma eventually_subseq:
"strict_mono r ⟹ eventually P sequentially ⟹ eventually (λn. P (r n)) sequentially"
unfolding eventually_sequentially by (metis seq_suble le_trans)

lemma not_eventually_sequentiallyD:
assumes "¬ eventually P sequentially"
shows "∃r::nat⇒nat. strict_mono r ∧ (∀n. ¬ P (r n))"
proof -
from assms have "∀n. ∃m≥n. ¬ P m"
unfolding eventually_sequentially by (simp add: not_less)
then obtain r where "⋀n. r n ≥ n" "⋀n. ¬ P (r n)"
by (auto simp: choice_iff)
then show ?thesis
by (auto intro!: exI[of _ "λn. r (((Suc ∘ r) ^^ Suc n) 0)"]
simp: less_eq_Suc_le strict_mono_Suc_iff)
qed

lemma sequentially_offset:
assumes "eventually (λi. P i) sequentially"
shows "eventually (λi. P (i + k)) sequentially"
using assms by (rule eventually_sequentially_seg [THEN iffD2])

lemma seq_offset_neg:
"(f ⤏ l) sequentially ⟹ ((λi. f(i - k)) ⤏ l) sequentially"
apply (erule filterlim_compose)
apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially, arith)
done

lemma filterlim_subseq: "strict_mono f ⟹ filterlim f sequentially sequentially"
unfolding filterlim_iff by (metis eventually_subseq)

lemma strict_mono_o: "strict_mono r ⟹ strict_mono s ⟹ strict_mono (r ∘ s)"
unfolding strict_mono_def by simp

lemma strict_mono_compose: "strict_mono r ⟹ strict_mono s ⟹ strict_mono (λx. r (s x))"
using strict_mono_o[of r s] by (simp add: o_def)

lemma incseq_imp_monoseq:  "incseq X ⟹ monoseq X"

lemma decseq_imp_monoseq:  "decseq X ⟹ monoseq X"

lemma decseq_eq_incseq: "decseq X = incseq (λn. - X n)"
for X :: "nat ⇒ 'a::ordered_ab_group_add"

lemma INT_decseq_offset:
assumes "decseq F"
shows "(⋂i. F i) = (⋂i∈{n..}. F i)"
proof safe
fix x i
assume x: "x ∈ (⋂i∈{n..}. F i)"
show "x ∈ F i"
proof cases
from x have "x ∈ F n" by auto
also assume "i ≤ n" with ‹decseq F› have "F n ⊆ F i"
unfolding decseq_def by simp
finally show ?thesis .
qed (insert x, ```