src/HOL/Topological_Spaces.thy

A few new theorems

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

section \<open>Topological Spaces\<close>

theory Topological_Spaces
  imports Main
begin

named_theorems continuous_intros "structural introduction rules for continuity"

subsection \<open>Topological space\<close>

class "open" =
  fixes "open" :: "'a set \<Rightarrow> bool"

class topological_space = "open" +
  assumes open_UNIV [simp, intro]: "open UNIV"
  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"
  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union>K)"
begin

definition closed :: "'a set \<Rightarrow> bool"
  where "closed S \<longleftrightarrow> open (- S)"

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

lemma open_Un [continuous_intros, intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"
  using open_Union [of "{S, T}"] by simp

lemma open_UN [continuous_intros, intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
  using open_Union [of "B ` A"] by simp

lemma open_Inter [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
  by (induction set: finite) auto

lemma open_INT [continuous_intros, intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
  using open_Inter [of "B ` A"] by simp

lemma openI:
  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"
  shows "open S"
proof -
  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto
  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)
  ultimately show "open S" by simp
qed

lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> 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 \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> 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 \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"
  unfolding closed_def by auto

lemma closed_INT [continuous_intros, intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
  unfolding closed_def by auto

lemma closed_Inter [continuous_intros, intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter>K)"
  unfolding closed_def uminus_Inf by auto

lemma closed_Union [continuous_intros, intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
  by (induct set: finite) auto

lemma closed_UN [continuous_intros, intro]:
  "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
  using closed_Union [of "B ` A"] by simp

lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
  by (simp add: closed_def)

lemma closed_open: "closed S \<longleftrightarrow> open (- S)"
  by (rule closed_def)

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

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

lemma open_Compl [continuous_intros, intro]: "closed S \<Longrightarrow> open (- S)"
  by (simp add: closed_open)

lemma closed_Compl [continuous_intros, intro]: "open S \<Longrightarrow> closed (- S)"
  by (simp add: open_closed)

lemma open_Collect_neg: "closed {x. P x} \<Longrightarrow> open {x. \<not> 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 \<and> 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 \<or> Q x}"
  using open_Un[OF assms] by (simp add: Un_def)

lemma open_Collect_ex: "(\<And>i. open {x. P i x}) \<Longrightarrow> open {x. \<exists>i. P i x}"
  using open_UN[of UNIV "\<lambda>i. {x. P i x}"] unfolding Collect_ex_eq by simp

lemma open_Collect_imp: "closed {x. P x} \<Longrightarrow> open {x. Q x} \<Longrightarrow> open {x. P x \<longrightarrow> 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} \<Longrightarrow> closed {x. \<not> 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 \<and> 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 \<or> Q x}"
  using closed_Un[OF assms] by (simp add: Un_def)

lemma closed_Collect_all: "(\<And>i. closed {x. P i x}) \<Longrightarrow> closed {x. \<forall>i. P i x}"
  using closed_INT[of UNIV "\<lambda>i. {x. P i x}"] by (simp add: Collect_all_eq)

lemma closed_Collect_imp: "open {x. P x} \<Longrightarrow> closed {x. Q x} \<Longrightarrow> closed {x. P x \<longrightarrow> Q x}"
  unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)

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

end


subsection \<open>Hausdorff and other separation properties\<close>

class t0_space = topological_space +
  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"

class t1_space = topological_space +
  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"

instance t1_space \<subseteq> t0_space
  by standard (fast dest: t1_space)

context t1_space begin

lemma separation_t1: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"
  using t1_space[of x y] by blast

lemma closed_singleton [iff]: "closed {a}"
proof -
  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
  have "open ?T"
    by (simp add: open_Union)
  also have "?T = - {a}"
    by (auto simp add: set_eq_iff separation_t1)
  finally show "closed {a}"
    by (simp only: closed_def)
qed

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

lemma finite_imp_closed: "finite S \<Longrightarrow> closed S"
  by (induct pred: finite) simp_all

end

text \<open>T2 spaces are also known as Hausdorff spaces.\<close>

class t2_space = topological_space +
  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"

instance t2_space \<subseteq> t1_space
  by standard (fast dest: hausdorff)

lemma (in t2_space) separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
  using hausdorff [of x y] by blast

lemma (in t0_space) separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U))"
  using t0_space [of x y] by blast


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

class t3_space = t2_space +
  assumes t3_space: "closed S \<Longrightarrow> y \<notin> S \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"

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

class t4_space = t2_space +
  assumes t4_space: "closed S \<Longrightarrow> closed T \<Longrightarrow> S \<inter> T = {} \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"

text \<open>T4 is stronger than T3, and weaker than metric.\<close>

instance t4_space \<subseteq> t3_space
proof
  fix S and y::'a assume "closed S" "y \<notin> S"
  then show "\<exists>U V. open U \<and> open V \<and> y \<in> U \<and> S \<subseteq> V \<and> U \<inter> V = {}"
    using t4_space[of "{y}" S] by auto
qed

text \<open>A perfect space is a topological space with no isolated points.\<close>

class perfect_space = topological_space +
  assumes not_open_singleton: "\<not> open {x}"

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


subsection \<open>Generators for toplogies\<close>

inductive generate_topology :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" for S :: "'a set set"
  where
    UNIV: "generate_topology S UNIV"
  | Int: "generate_topology S (a \<inter> b)" if "generate_topology S a" and "generate_topology S b"
  | UN: "generate_topology S (\<Union>K)" if "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k)"
  | Basis: "generate_topology S s" if "s \<in> S"

hide_fact (open) UNIV Int UN Basis

lemma generate_topology_Union:
  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"
  using generate_topology.UN [of "K ` I"] by auto

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


subsection \<open>Order topologies\<close>

class order_topology = order + "open" +
  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"
begin

subclass topological_space
  unfolding open_generated_order
  by (rule topological_space_generate_topology)

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

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

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

end

class linorder_topology = linorder + order_topology

lemma closed_atMost [continuous_intros, simp]: "closed {..a}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeast [continuous_intros, simp]: "closed {a..}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}"
  for a b :: "'a::linorder_topology"
proof -
  have "{a .. b} = {a ..} \<inter> {.. b}"
    by auto
  then show ?thesis
    by (simp add: closed_Int)
qed

lemma (in order) less_separate:
  assumes "x < y"
  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
proof (cases "\<exists>z. x < z \<and> z < y")
  case True
  then obtain z where "x < z \<and> z < y" ..
  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"
    by auto
  then show ?thesis by blast
next
  case False
  with \<open>x < y\<close> have "x \<in> {..< y}" "y \<in> {x <..}" "{x <..} \<inter> {..< y} = {}"
    by auto
  then show ?thesis by blast
qed

instance linorder_topology \<subseteq> t2_space
proof
  fix x y :: 'a
  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> 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 \<in> S"
    and gt_ex: "x < y"
  shows "\<exists>b>x. {x ..< b} \<subseteq> 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} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> 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 \<in> S"
    and lt_ex: "y < x"
  shows "\<exists>b<x. {b <.. x} \<subseteq> 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} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B"
    by auto
  then show ?case
    by (auto intro!: exI[of _ "max a b"])
next
  case UN
  then show ?case by blast
next
  case Basis
  then show ?case
    by (fastforce intro: exI[of _ y] lt_ex)
qed


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

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

class discrete_topology = topological_space +
  assumes open_discrete: "\<And>A. open A"

instance discrete_topology < t2_space
proof
  fix x y :: 'a
  assume "x \<noteq> y"
  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
    by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
qed

instantiation bool :: linorder_topology
begin

definition open_bool :: "bool set \<Rightarrow> bool"
  where "open_bool = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>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 \<or> A = {} \<or> A = {False <..} \<or> 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 \<Rightarrow> bool"
  where "open_nat = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>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} \<inter> {n' <..}"
      by auto
    with Suc show ?thesis
      by (auto intro: open_lessThan open_greaterThan)
  qed
  then have "open (\<Union>a\<in>A. {a})"
    by (intro open_UN) auto
  then show "open A"
    by simp
qed

instantiation int :: linorder_topology
begin

definition open_int :: "int set \<Rightarrow> bool"
  where "open_int = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"

instance
  by standard (rule open_int_def)

end

instance int :: discrete_topology
proof
  fix A :: "int set"
  have "{..<i + 1} \<inter> {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 (\<Union>a\<in>A. {a})"
    by (intro open_UN) auto
  then show "open A"
    by simp
qed


subsubsection \<open>Topological filters\<close>

definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
  where "nhds a = (INF S\<in>{S. open S \<and> a \<in> S}. principal S)"

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

abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter"  ("at")
  where "at x \<equiv> at x within (CONST UNIV)"

abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter"
  where "at_right x \<equiv> at x within {x <..}"

abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter"
  where "at_left x \<equiv> at x within {..< x}"

lemma (in topological_space) nhds_generated_topology:
  "open = generate_topology T \<Longrightarrow> nhds x = (INF S\<in>{S\<in>T. x \<in> S}. principal S)"
  unfolding nhds_def
proof (safe intro!: antisym INF_greatest)
  fix S
  assume "generate_topology T S" "x \<in> S"
  then show "(INF S\<in>{S \<in> T. x \<in> S}. principal S) \<le> 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) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
  unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)

lemma eventually_eventually:
  "eventually (\<lambda>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 \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
  by (subst eventually_nhds) blast

lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x) \<Longrightarrow> P x"
  by (subst (asm) eventually_nhds) blast

lemma (in topological_space) nhds_neq_bot [simp]: "nhds a \<noteq> bot"
  by (simp add: trivial_limit_def eventually_nhds)

lemma (in t1_space) t1_space_nhds: "x \<noteq> y \<Longrightarrow> (\<forall>\<^sub>F x in nhds x. x \<noteq> y)"
  by (drule t1_space) (auto simp: eventually_nhds)

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

lemma (in discrete_topology) nhds_discrete: "nhds x = principal {x}"
  by (simp add: nhds_discrete_open open_discrete)

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

lemma (in discrete_topology) tendsto_discrete:
  "filterlim (f :: 'b \<Rightarrow> 'a) (nhds y) F \<longleftrightarrow> eventually (\<lambda>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\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> 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) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> 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 \<subseteq> t \<Longrightarrow> at x within s \<le> 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) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
  by (simp add: eventually_nhds eventually_at_filter)

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

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

lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> 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 \<in> s \<Longrightarrow> open s \<Longrightarrow> NO_MATCH UNIV s \<Longrightarrow> at a within s = at a"
  by (simp only: at_within_open)

lemma (in topological_space) at_within_open_subset:
  "a \<in> S \<Longrightarrow> open S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> 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 \<in> S" "open S" "T \<inter> S - {x} = U \<inter> 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 (\<lambda>x. x \<in> S) (nhds x)"
    using \<open>x \<in> S\<close> \<open>open S\<close> by (auto simp: eventually_nhds)
  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
    by eventually_elim (insert \<open>T \<inter> S - {x} = U \<inter> S - {x}\<close>, blast)
qed

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

lemma (in topological_space) at_within_union:
  "at x within (S \<union> 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 \<longleftrightarrow> 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 (\<lambda>w. w \<noteq> 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 \<noteq> bot"
  by (simp add: at_eq_bot_iff not_open_singleton)

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

lemma (in topological_space) filterlim_at_within_If:
  assumes "filterlim f G (at x within (A \<inter> {x. P x}))"
    and "filterlim g G (at x within (A \<inter> {x. \<not>P x}))"
  shows "filterlim (\<lambda>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 \<inter> {x. P x}) = inf (nhds x) (principal (A \<inter> Collect P - {x}))"
    by (simp add: at_within_def)
  also have "A \<inter> Collect P - {x} = (A - {x}) \<inter> Collect P"
    by blast
  also have "inf (nhds x) (principal \<dots>) = inf (at x within A) (principal (Collect P))"
    by (simp add: at_within_def inf_assoc)
  finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" .
next
  note assms(2)
  also have "at x within (A \<inter> {x. \<not> P x}) = inf (nhds x) (principal (A \<inter> {x. \<not> P x} - {x}))"
    by (simp add: at_within_def)
  also have "A \<inter> {x. \<not> P x} - {x} = (A - {x}) \<inter> {x. \<not> P x}"
    by blast
  also have "inf (nhds x) (principal \<dots>) = inf (at x within A) (principal {x. \<not> P x})"
    by (simp add: at_within_def inf_assoc)
  finally show "filterlim g G (inf (at x within A) (principal {x. \<not> 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. \<not>P x})"
  shows "filterlim (\<lambda>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 \<noteq> {x}"
  shows "at x within s =
    inf (INF a\<in>{x <..}. principal ({..< a} \<inter> s - {x}))
        (INF a\<in>{..< x}. principal ({a <..} \<inter> s - {x}))"
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split])
  case True_True
  have "UNIV = {..< x} \<union> {x} \<union> {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 \<Longrightarrow> at_left x = (INF a\<in>{..< 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 \<Longrightarrow> eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> 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 \<Longrightarrow> at_right x = (INF a\<in>{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 \<Longrightarrow> eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
  unfolding at_right_eq
  by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)

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

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

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

lemma trivial_limit_at_left_real [simp]: "\<not> 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]: "\<not> 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) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"
  by (subst at_eq_sup_left_right) (simp add: eventually_sup)

lemma (in order_topology) eventually_at_leftI:
  assumes "\<And>x. x \<in> {a<..<b} \<Longrightarrow> 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 "\<And>x. x \<in> {a<..<b} \<Longrightarrow> 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)) \<longleftrightarrow> (\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x. f x \<in> S \<longrightarrow> P x))"
  unfolding eventually_filtercomap eventually_nhds by auto

lemma eventually_filtercomap_at_topological:
  "eventually P (filtercomap f (at A within B)) \<longleftrightarrow> 
     (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
  unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
          eventually_filtercomap_nhds eventually_principal by blast

lemma eventually_at_right_field:
  "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> 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) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> 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 (\<lambda>x. f x = f z \<longrightarrow> x = z) (at z)"
  shows   "filtermap f (at z) = at (f z)"
proof (rule filter_eqI)
  fix P :: "'a \<Rightarrow> bool"
  have "eventually P (filtermap f (at z)) \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> P (f x))"
    by (simp add: eventually_filtermap eventually_at_filter)
  also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. f x \<noteq> f z \<longrightarrow> P (f x))"
    by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
  also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in filtermap f (nhds z). x \<noteq> f z \<longrightarrow> P x)"
    by (simp add: eventually_filtermap)
  also have "filtermap f (nhds z) = nhds (f z)"
    by (rule assms)
  also have "(\<forall>\<^sub>F x in nhds (f z). x \<noteq> f z \<longrightarrow> P x) \<longleftrightarrow> (\<forall>\<^sub>F x in at (f z). P x)"
    by (simp add: eventually_at_filter)
  finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
qed

subsubsection \<open>Tendsto\<close>

abbreviation (in topological_space)
  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool"  (infixr "\<longlongrightarrow>" 55)
  where "(f \<longlongrightarrow> l) F \<equiv> filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
  where "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"

lemma (in topological_space) tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
  by simp

named_theorems tendsto_intros "introduction rules for tendsto"
setup \<open>
  Global_Theory.add_thms_dynamic (\<^binding>\<open>tendsto_eq_intros\<close>,
    fn context =>
      Named_Theorems.get (Context.proof_of context) \<^named_theorems>\<open>tendsto_intros\<close>
      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
\<close>

context topological_space begin

lemma tendsto_def:
   "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   unfolding nhds_def filterlim_INF filterlim_principal by auto

lemma tendsto_cong: "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F" if "eventually (\<lambda>x. f x = g x) F"
  by (rule filterlim_cong [OF refl refl that])

lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"