Theory Topological_Spaces
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)"
by (simp add: closed_def)
lemma closed_open: "closed S ⟷ open (- S)"
by (rule closed_def)
lemma open_Diff [continuous_intros, intro]: "open S ⟹ closed T ⟹ open (S - T)"
by (simp add: closed_open Diff_eq open_Int)
lemma closed_Diff [continuous_intros, intro]: "closed S ⟹ open T ⟹ closed (S - T)"
by (simp add: open_closed Diff_eq closed_Int)
lemma open_Compl [continuous_intros, intro]: "closed S ⟹ open (- S)"
by (simp add: closed_open)
lemma closed_Compl [continuous_intros, intro]: "open S ⟹ closed (- S)"
by (simp add: open_closed)
lemma open_Collect_neg: "closed {x. P x} ⟹ open {x. ¬ P x}"
unfolding Collect_neg_eq by (rule open_Compl)
lemma open_Collect_conj:
assumes "open {x. P x}" "open {x. Q x}"
shows "open {x. P x ∧ Q x}"
using open_Int[OF assms] by (simp add: Int_def)
lemma open_Collect_disj:
assumes "open {x. P x}" "open {x. Q x}"
shows "open {x. P x ∨ Q x}"
using open_Un[OF assms] by (simp add: Un_def)
lemma open_Collect_ex: "(⋀i. open {x. P i x}) ⟹ open {x. ∃i. P i x}"
using open_UN[of UNIV "λi. {x. P i x}"] unfolding Collect_ex_eq by simp
lemma open_Collect_imp: "closed {x. P x} ⟹ open {x. Q x} ⟹ open {x. P x ⟶ Q x}"
unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)
lemma open_Collect_const: "open {x. P}"
by (cases P) auto
lemma closed_Collect_neg: "open {x. P x} ⟹ closed {x. ¬ P x}"
unfolding Collect_neg_eq by (rule closed_Compl)
lemma closed_Collect_conj:
assumes "closed {x. P x}" "closed {x. Q x}"
shows "closed {x. P x ∧ Q x}"
using closed_Int[OF assms] by (simp add: Int_def)
lemma closed_Collect_disj:
assumes "closed {x. P x}" "closed {x. Q x}"
shows "closed {x. P x ∨ Q x}"
using closed_Un[OF assms] by (simp add: Un_def)
lemma closed_Collect_all: "(⋀i. closed {x. P i x}) ⟹ closed {x. ∀i. P i x}"
using closed_INT[of UNIV "λi. {x. P i x}"] by (simp add: Collect_all_eq)
lemma closed_Collect_imp: "open {x. P x} ⟹ closed {x. Q x} ⟹ closed {x. P x ⟶ Q x}"
unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)
lemma closed_Collect_const: "closed {x. P}"
by (cases P) auto
end
subsection ‹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"
by (simp add: open_Union)
also have "?T = - {a}"
by (auto simp add: set_eq_iff separation_t1)
finally show "closed {a}"
by (simp only: closed_def)
qed
lemma closed_insert [continuous_intros, simp]:
assumes "closed S"
shows "closed (insert a S)"
proof -
from closed_singleton assms have "closed ({a} ∪ S)"
by (rule closed_Un)
then show "closed (insert a S)"
by simp
qed
lemma finite_imp_closed: "finite S ⟹ closed S"
by (induct pred: finite) simp_all
end
text ‹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"
by (simp add: closed_open)
lemma closed_atLeast [continuous_intros, simp]: "closed {a..}"
for a :: "'a::linorder_topology"
by (simp add: closed_open)
lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}"
for a b :: "'a::linorder_topology"
proof -
have "{a .. b} = {a ..} ∩ {.. b}"
by auto
then show ?thesis
by (simp add: closed_Int)
qed
lemma (in order) less_separate:
assumes "x < y"
shows "∃a b. x ∈ {..< a} ∧ y ∈ {b <..} ∧ {..< a} ∩ {b <..} = {}"
proof (cases "∃z. x < z ∧ z < y")
case True
then obtain z where "x < z ∧ z < y" ..
then have "x ∈ {..< z} ∧ y ∈ {z <..} ∧ {z <..} ∩ {..< z} = {}"
by auto
then show ?thesis by blast
next
case False
with ‹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"
by (simp add: trivial_limit_def eventually_nhds)
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}"
by (simp add: nhds_discrete_open open_discrete)
lemma (in discrete_topology) at_discrete: "at x within S = bot"
unfolding at_within_def nhds_discrete by simp
lemma (in discrete_topology) tendsto_discrete:
"filterlim (f :: 'b ⇒ 'a) (nhds y) F ⟷ eventually (λx. f x = y) F"
by (auto simp: nhds_discrete filterlim_principal)
lemma (in topological_space) at_within_eq:
"at x within s = (INF S∈{S. open S ∧ x ∈ S}. principal (S ∩ s - {x}))"
unfolding nhds_def at_within_def
by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
lemma (in topological_space) eventually_at_filter:
"eventually P (at a within s) ⟷ eventually (λx. x ≠ a ⟶ x ∈ s ⟶ P x) (nhds a)"
by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)
lemma (in topological_space) at_le: "s ⊆ t ⟹ at x within s ≤ at x within t"
unfolding at_within_def by (intro inf_mono) auto
lemma (in topological_space) eventually_at_topological:
"eventually P (at a within s) ⟷ (∃S. open S ∧ a ∈ S ∧ (∀x∈S. x ≠ a ⟶ x ∈ s ⟶ P x))"
by (simp add: eventually_nhds eventually_at_filter)
lemma eventually_nhds_conv_at:
"eventually P (nhds x) ⟷ eventually P (at x) ∧ P x"
unfolding eventually_at_topological eventually_nhds by fast
lemma eventually_at_in_open:
assumes "open A" "x ∈ A"
shows "eventually (λy. y ∈ A - {x}) (at x)"
using assms eventually_at_topological by blast
lemma eventually_at_in_open':
assumes "open A" "x ∈ A"
shows "eventually (λy. y ∈ A) (at x)"
using assms eventually_at_topological by blast
lemma (in topological_space) at_within_open: "a ∈ S ⟹ open S ⟹ at a within S = at a"
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
lemma (in topological_space) at_within_open_NO_MATCH:
"a ∈ s ⟹ open s ⟹ NO_MATCH UNIV s ⟹ at a within s = at a"
by (simp only: at_within_open)
lemma (in topological_space) at_within_open_subset:
"a ∈ S ⟹ open S ⟹ S ⊆ T ⟹ at a within T = at a"
by (metis at_le at_within_open dual_order.antisym subset_UNIV)
lemma (in topological_space) at_within_nhd:
assumes "x ∈ S" "open S" "T ∩ S - {x} = U ∩ S - {x}"
shows "at x within T = at x within U"
unfolding filter_eq_iff eventually_at_filter
proof (intro allI eventually_subst)
have "eventually (λx. x ∈ S) (nhds x)"
using ‹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"
by (simp add: at_eq_bot_iff not_open_singleton)
lemma (in order_topology) nhds_order:
"nhds x = inf (INF a∈{x <..}. principal {..< a}) (INF a∈{..< x}. principal {a <..})"
proof -
have 1: "{S ∈ range lessThan ∪ range greaterThan. x ∈ S} =
(λ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}))"
by (simp add: at_within_def)
also have "A ∩ Collect P - {x} = (A - {x}) ∩ Collect P"
by blast
also have "inf (nhds x) (principal …) = inf (at x within A) (principal (Collect P))"
by (simp add: at_within_def inf_assoc)
finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" .
next
note assms(2)
also have "at x within (A ∩ {x. ¬ P x}) = inf (nhds x) (principal (A ∩ {x. ¬ P x} - {x}))"
by (simp add: at_within_def)
also have "A ∩ {x. ¬ P x} - {x} = (A - {x}) ∩ {x. ¬ P x}"
by blast
also have "inf (nhds x) (principal …) = inf (at x within A) (principal {x. ¬ P x})"
by (simp add: at_within_def inf_assoc)
finally show "filterlim g G (inf (at x within A) (principal {x. ¬ P x}))" .
qed
lemma (in topological_space) filterlim_at_If:
assumes "filterlim f G (at x within {x. P x})"
and "filterlim g G (at x within {x. ¬P x})"
shows "filterlim (λx. if P x then f x else g x) G (at x)"
using assms by (intro filterlim_at_within_If) simp_all
lemma (in linorder_topology) at_within_order:
assumes "UNIV ≠ {x}"
shows "at x within s =
inf (INF a∈{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))"
by (simp add: eventually_filtermap eventually_at_filter)
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)"
by (simp add: eventually_filtermap)
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)"
by (simp add: eventually_at_filter)
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 ‹
Global_Theory.add_thms_dynamic (\<^binding>‹tendsto_eq_intros›,
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"
by (simp add: tendsto_def)
lemma filterlim_at:
"(LIM x F. f x :> at b within s) ⟷ eventually (λx. f x ∈ s ∧ f x ≠ b) F ∧ (f ⤏ b) F"
by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
lemma (in -)
assumes "filterlim f (nhds L) F"
shows tendsto_imp_filterlim_at_right:
"eventually (λx. f x > L) F ⟹ filterlim f (at_right L) F"
and tendsto_imp_filterlim_at_left:
"eventually (λx. f x < L) F ⟹ filterlim f (at_left L) F"
using assms by (auto simp: filterlim_at elim: eventually_mono)
lemma filterlim_at_withinI:
assumes "filterlim f (nhds c) F"
assumes "eventually (λx. f x ∈ A - {c}) F"
shows "filterlim f (at c within A) F"
using assms by (simp add: filterlim_at)
lemma filterlim_atI:
assumes "filterlim f (nhds c) F"
assumes "eventually (λx. f x ≠ c) F"
shows "filterlim f (at c) F"
using assms by (intro filterlim_at_withinI) simp_all
lemma topological_tendstoI:
"(⋀S. open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F) ⟹ (f ⤏ l) F"
by (auto simp: tendsto_def)
lemma topological_tendstoD:
"(f ⤏ l) F ⟹ open S ⟹ l ∈ S ⟹ eventually (λx. f x ∈ S) F"
by (auto simp: tendsto_def)
lemma tendsto_bot [simp]: "(f ⤏ a) bot"
by (simp add: tendsto_def)
lemma tendsto_eventually: "eventually (λx. f x = l) net ⟹ ((λx. f x) ⤏ l) net"
by (rule topological_tendstoI) (auto elim: eventually_mono)
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) 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"
by (simp add: trivial_limit_def)
qed
lemma (in t2_space) tendsto_const_iff:
fixes a b :: 'a
assumes "¬ trivial_limit F"
shows "((λx. a) ⤏ b) F ⟷ a = b"
by (auto intro!: tendsto_unique [OF assms tendsto_const])
lemma (in t2_space) tendsto_unique':
assumes "F ≠ bot"
shows "∃⇩≤⇩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"
by (simp_all add: open_Compl)
with assms(4) have "eventually (λx. f x ∈ - S) F"
by (rule topological_tendstoD)
with assms(2) have "eventually (λx. False) F"
by (rule eventually_elim2) simp
with assms(3) show "False"
by (simp add: eventually_False)
qed
lemma (in t3_space) nhds_closed:
assumes "x ∈ A" and "open A"
shows "∃A'. x ∈ A' ∧ closed A' ∧ A' ⊆ A ∧ eventually (λy. y ∈ A') (nhds x)"
proof -
from assms have "∃U V. open U ∧ open V ∧ x ∈ U ∧ - A ⊆ V ∧ U ∩ V = {}"
by (intro t3_space) auto
then obtain U V where UV: "open U" "open V" "x ∈ U" "-A ⊆ V" "U ∩ V = {}"
by auto
have "eventually (λy. y ∈ U) (nhds x)"
using ‹open 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
unfolding frequently_def by contradiction
qed
lemma (in t1_space) tendsto_imp_eventually_ne:
assumes "(f ⤏ c) F" "c ≠ c'"
shows "eventually (λz. f z ≠ c') F"
proof (cases "F=bot")
case True
thus ?thesis by auto
next
case False
show ?thesis
proof (rule ccontr)
assume "¬ eventually (λz. f z ≠ c') F"
then have "frequently (λz. f z = c') F"
by (simp add: frequently_def)
from limit_frequently_eq[OF False this ‹(f ⤏ c) F›] and ‹c ≠ c'› show False
by contradiction
qed
qed
lemma (in linorder_topology) tendsto_le:
assumes F: "¬ trivial_limit F"
and x: "(f ⤏ x) F"
and y: "(g ⤏ y) F"
and ev: "eventually (λx. g x ≤ f x) F"
shows "y ≤ x"
proof (rule ccontr)
assume "¬ y ≤ x"
with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<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
by (simp add: eventually_False)
qed
lemma (in linorder_topology) tendsto_lowerbound:
assumes x: "(f ⤏ x) F"
and ev: "eventually (λi. a ≤ f i) F"
and F: "¬ trivial_limit F"
shows "a ≤ x"
using F x tendsto_const ev by (rule tendsto_le)
lemma (in linorder_topology) tendsto_upperbound:
assumes x: "(f ⤏ x) F"
and ev: "eventually (λi. a ≥ f i) F"
and F: "¬ trivial_limit F"
shows "a ≥ x"
by (rule tendsto_le [OF F tendsto_const x ev])
lemma filterlim_at_within_not_equal:
fixes f::"'a ⇒ 'b::t2_space"
assumes "filterlim f (at a within s) F"
shows "eventually (λw. f w∈s ∧ f w ≠b) F"
proof (cases "a=b")
case True
then show ?thesis using assms by (simp add: filterlim_at)
next
case False
from hausdorff[OF this] obtain U V where UV:"open U" "open V" "a ∈ U" "b ∈ V" "U ∩ V = {}"
by auto
have "(f ⤏ a) F" using assms filterlim_at by auto
then have "∀⇩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
subsubsection ‹Rules about \<^const>‹Lim››
lemma tendsto_Lim: "¬ trivial_limit net ⟹ (f ⤏ l) net ⟹ Lim net f = l"
unfolding Lim_def using tendsto_unique [of net f] by auto
lemma Lim_ident_at: "¬ trivial_limit (at x within s) ⟹ Lim (at x within s) (λx. x) = x"
by (simp add: tendsto_Lim)
lemma Lim_cong:
assumes "∀⇩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.›
lemma strict_mono_leD: "strict_mono r ⟹ m ≤ n ⟹ r m ≤ r n"
by (erule (1) monoD [OF strict_mono_mono])
lemma strict_mono_id: "strict_mono id"
by (simp add: strict_mono_def)
lemma incseq_SucI: "(⋀n. X n ≤ X (Suc n)) ⟹ incseq X"
using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
lemma incseqD: "incseq f ⟹ i ≤ j ⟹ f i ≤ f j"
by (auto simp: incseq_def)
lemma incseq_SucD: "incseq A ⟹ A i ≤ A (Suc i)"
using incseqD[of A i "Suc i"] by auto
lemma incseq_Suc_iff: "incseq f ⟷ (∀n. f n ≤ f (Suc n))"
by (auto intro: incseq_SucI dest: incseq_SucD)
lemma incseq_const[simp, intro]: "incseq (λx. k)"
unfolding incseq_def by auto
lemma decseq_SucI: "(⋀n. X (Suc n) ≤ X n) ⟹ decseq X"
using order.lift_Suc_mono_le[OF dual_order, of X] by (auto simp: decseq_def)
lemma decseqD: "decseq f ⟹ i ≤ j ⟹ f j ≤ f i"
by (auto simp: decseq_def)
lemma decseq_SucD: "decseq A ⟹ A (Suc i) ≤ A i"
using decseqD[of A i "Suc i"] by auto
lemma decseq_Suc_iff: "decseq f ⟷ (∀n. f (Suc n) ≤ f n)"
by (auto intro: decseq_SucI dest: decseq_SucD)
lemma decseq_const[simp, intro]: "decseq (λx. k)"
unfolding decseq_def by auto
lemma monoseq_iff: "monoseq X ⟷ incseq X ∨ decseq X"
unfolding monoseq_def incseq_def decseq_def ..
lemma monoseq_Suc: "monoseq X ⟷ (∀n. X n ≤ X (Suc n)) ∨ (∀n. X (Suc n) ≤ X n)"
unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
lemma monoI1: "∀m. ∀n ≥ m. X m ≤ X n ⟹ monoseq X"
by (simp add: monoseq_def)
lemma monoI2: "∀m. ∀n ≥ m. X n ≤ X m ⟹ monoseq X"
by (simp add: monoseq_def)
lemma mono_SucI1: "∀n. X n ≤ X (Suc n) ⟹ monoseq X"
by (simp add: monoseq_Suc)
lemma mono_SucI2: "∀n. X (Suc n) ≤ X n ⟹ monoseq X"
by (simp add: monoseq_Suc)
lemma monoseq_minus:
fixes a :: "nat ⇒ 'a::ordered_ab_group_add"
assumes "monoseq a"
shows "monoseq (λ n. - a n)"
proof (cases "∀m. ∀n ≥ m. a m ≤ a n")
case True
then have "∀m. ∀n ≥ m. - a n ≤ - a m" by auto
then show ?thesis by (rule monoI2)
next
case False
then have "∀m. ∀n ≥ m. - a m ≤ - a n"
using ‹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"
by (simp add: incseq_def monoseq_def)
lemma decseq_imp_monoseq: "decseq X ⟹ monoseq X"
by (simp add: decseq_def monoseq_def)
lemma decseq_eq_incseq: "decseq X = incseq (λn. - X n)"
for X :: "nat ⇒ 'a::ordered_ab_group_add"
by (simp add: decseq_def incseq_def)
lemma INT_decseq_offset:
assumes "decseq F"
shows "(⋂i. F i) = (⋂i∈{n..}. F i)"
proof safe
fix x i
assume x: "x ∈ (⋂i∈{n..}. F i)"
show "x ∈ F i"
proof cases
from x have "x ∈ F n" by auto
also assume "i ≤ n" with ‹decseq F› have "F n ⊆ F i"
unfolding decseq_def by simp
finally show ?thesis .
qed (insert x, simp)
qed auto
lemma LIMSEQ_const_iff: "(λn. k) ⇢ l ⟷ k = l"
for k l :: "'a::t2_space"
using trivial_limit_sequentially by (rule tendsto_const_iff)
lemma LIMSEQ_SUP: "incseq X ⟹ X ⇢ (SUP i. X i :: 'a::{complete_linorder,linorder_topology})"
by (intro increasing_tendsto)
(auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
lemma LIMSEQ_INF: "decseq X ⟹ X ⇢ (INF i. X i :: 'a::{complete_linorder,linorder_topology})"
by (intro decreasing_tendsto)
(auto simp: INF_lower INF_less_iff decseq_def eventually_sequentially intro: le_less_trans)
lemma LIMSEQ_ignore_initial_segment: "f ⇢ a ⟹ (λn. f (n + k)) ⇢ a"
unfolding tendsto_def by (subst eventually_sequentially_seg[where k=k])
lemma LIMSEQ_offset: "(λn. f (n + k)) ⇢ a ⟹ f ⇢ a"
unfolding tendsto_def
by (subst (asm) eventually_sequentially_seg[where k=k])
lemma LIMSEQ_Suc: "f ⇢ l ⟹ (λn. f (Suc n)) ⇢ l"
by (drule LIMSEQ_ignore_initial_segment [where k="Suc 0"]) simp
lemma LIMSEQ_imp_Suc: "(λn. f (Suc n)) ⇢ l ⟹ f ⇢ l"
by (rule LIMSEQ_offset [where k="Suc 0"]) simp
lemma LIMSEQ_lessThan_iff_atMost:
shows "(λn. f {..<n}) ⇢ x ⟷ (λn. f {..n}) ⇢ x"
apply (subst filterlim_sequentially_Suc [symmetric])
apply (simp only: lessThan_Suc_atMost)
done
lemma (in t2_space) LIMSEQ_Uniq: "∃⇩≤⇩1l. X ⇢ l"
by (simp add: tendsto_unique')
lemma (in t2_space) LIMSEQ_unique: "X ⇢ a ⟹ X ⇢ b ⟹ a = b"
using trivial_limit_sequentially by (rule tendsto_unique)
lemma LIMSEQ_le_const: "X ⇢ x ⟹ ∃N. ∀n≥N. a ≤ X n ⟹ a ≤ x"
for a x :: "'a::linorder_topology"
by (simp add: eventually_at_top_linorder tendsto_lowerbound)
lemma LIMSEQ_le: "X ⇢ x ⟹ Y ⇢ y ⟹ ∃N. ∀n≥N. X n ≤ Y n ⟹ x ≤ y"
for x y :: "'a::linorder_topology"
using tendsto_le[of sequentially Y y X x] by (simp add: eventually_sequentially)
lemma LIMSEQ_le_const2: "X ⇢ x ⟹ ∃N. ∀n≥N. X n ≤ a ⟹ x ≤ a"
for a x :: "'a::linorder_topology"
by (rule LIMSEQ_le[of X x "λn. a"]) auto
lemma Lim_bounded: "f ⇢ l ⟹ ∀n≥M. f n ≤ C ⟹ l ≤ C"
for l :: "'a::linorder_topology"
by (intro LIMSEQ_le_const2) auto
lemma Lim_bounded2:
fixes f :: "nat ⇒ 'a::linorder_topology"
assumes lim:"f ⇢ l" and ge: "∀n≥N. f n ≥ C"
shows "l ≥ C"
using ge
by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
(auto simp: eventually_sequentially)
lemma lim_mono:
fixes X Y :: "nat ⇒ 'a::linorder_topology"
assumes "⋀n. N ≤ n ⟹ X n ≤ Y n"
and "X ⇢ x"
and "Y ⇢ y"
shows "x ≤ y"
using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
lemma Sup_lim:
fixes a :: "'a::{complete_linorder,linorder_topology}"
assumes "⋀n. b n ∈ s"
and "b ⇢ a"
shows "a ≤ Sup s"
by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
lemma Inf_lim:
fixes a :: "'a::{complete_linorder,linorder_topology}"
assumes "⋀n. b n ∈ s"
and "b ⇢ a"
shows "Inf s ≤ a"
by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
lemma SUP_Lim:
fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
assumes inc: "incseq X"
and l: "X ⇢ l"
shows "(SUP n. X n) = l"
using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
by simp
lemma INF_Lim:
fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
assumes dec: "decseq X"
and l: "X ⇢ l"
shows "(INF n. X n) = l"
using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
by simp
lemma convergentD: "convergent X ⟹ ∃L. X ⇢ L"
by (simp add: convergent_def)
lemma convergentI: "X ⇢ L ⟹ convergent X"
by (auto simp add: convergent_def)
lemma convergent_LIMSEQ_iff: "convergent X ⟷ X ⇢ lim X"
by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def)
lemma convergent_const: "convergent (λn. c)"
by (rule convergentI) (rule tendsto_const)
lemma monoseq_le:
"monoseq a ⟹ a ⇢ x ⟹
(∀n. a n ≤ x) ∧ (∀m. ∀n≥m. a m ≤ a n) ∨
(∀n. x ≤ a n) ∧ (∀m. ∀n≥m. a n ≤ a m)"
for x :: "'a::linorder_topology"
by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
lemma LIMSEQ_subseq_LIMSEQ: "X ⇢ L ⟹ strict_mono f ⟹ (X ∘ f) ⇢ L"
unfolding comp_def by (rule filterlim_compose [of X, OF _ filterlim_subseq])
lemma convergent_subseq_convergent: "convergent X ⟹ strict_mono f ⟹ convergent (X ∘ f)"
by (auto simp: convergent_def intro: LIMSEQ_subseq_LIMSEQ)
lemma limI: "X ⇢ L ⟹ lim X = L"
by (rule tendsto_Lim) (rule trivial_limit_sequentially)
lemma lim_le: "convergent f ⟹ (⋀n. f n ≤ x) ⟹ lim f ≤ x"
for x :: "'a::linorder_topology"
using LIMSEQ_le_const2[of f "lim f" x] by (simp add: convergent_LIMSEQ_iff)
lemma lim_const [simp]: "lim (λm. a) = a"
by (simp add: limI)
subsubsection ‹Increasing and Decreasing Series›
lemma incseq_le: "incseq X ⟹ X ⇢ L ⟹ X n ≤ L"
for L :: "'a::linorder_topology"
by (metis incseq_def LIMSEQ_le_const)
lemma decseq_ge: "decseq X ⟹ X ⇢ L ⟹ L ≤ X n"
for L :: "'a::linorder_topology"
by (metis decseq_def LIMSEQ_le_const2)
subsection ‹First countable topologies›
class first_countable_topology = topological_space +
assumes first_countable_basis:
"∃A::nat ⇒ 'a set. (∀i. x ∈ A i ∧ open (A i)) ∧ (∀S. open S ∧ x ∈ S ⟶ (∃i. A i ⊆ S))"
lemma (in first_countable_topology) countable_basis_at_decseq:
obtains A :: "nat ⇒ 'a set" where
"⋀i. open (A i)" "⋀i. x ∈ (A i)"
"⋀S. open S ⟹ x ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially"
proof atomize_elim
from first_countable_basis[of x] obtain A :: "nat ⇒ 'a set"
where nhds: "⋀i. open (A i)" "⋀i. x ∈ A i"
and incl: "⋀S. open S ⟹ x ∈ S ⟹ ∃i. A i ⊆ S"
by auto
define F where "F n = (⋂i≤n. A i)" for n
show "∃A. (∀i. open (A i)) ∧ (∀i. x ∈ A i) ∧
(∀S. open S ⟶ x ∈ S ⟶ eventually (λi. A i ⊆ S) sequentially)"
proof (safe intro!: exI[of _ F])
fix i
show "open (F i)"
using nhds(1) by (auto simp: F_def)
show "x ∈ F i"
using nhds(2) by (auto simp: F_def)
next
fix S
assume "open S" "x ∈ S"
from incl[OF this] obtain i where "F i ⊆ S"
unfolding F_def by auto
moreover have "⋀j. i ≤ j ⟹ F j ⊆ F i"
by (simp add: Inf_superset_mono F_def image_mono)
ultimately show "eventually (λi. F i ⊆ S) sequentially"
by (auto simp: eventually_sequentially)
qed
qed
lemma (in first_countable_topology) nhds_countable:
obtains X :: "nat ⇒ 'a set"
where "decseq X" "⋀n. open (X n)" "⋀n. x ∈ X n" "nhds x = (INF n. principal (X n))"
proof -
from first_countable_basis obtain A :: "nat ⇒ 'a set"
where *: "⋀n. x ∈ A n" "⋀n. open (A n)" "⋀S. open S ⟹ x ∈ S ⟹ ∃i. A i ⊆ S"
by metis
show thesis
proof
show "decseq (λn. ⋂i≤n. A i)"
by (simp add: antimono_iff_le_Suc atMost_Suc)
show "x ∈ (⋂i≤n. A i)" "⋀n. open (⋂i≤n. A i)" for n
using * by auto
with * show "nhds x = (INF n. principal (⋂i≤n. A i))"
unfolding nhds_def
apply (intro INF_eq)
apply fastforce
apply blast
done
qed
qed
lemma (in first_countable_topology) countable_basis:
obtains A :: "nat ⇒ 'a set" where
"⋀i. open (A i)" "⋀i. x ∈ A i"
"⋀F. (∀n. F n ∈ A n) ⟹ F ⇢ x"
proof atomize_elim
obtain A :: "nat ⇒ 'a set" where *:
"⋀i. open (A i)"
"⋀i. x ∈ A i"
"⋀S. open S ⟹ x ∈ S ⟹ eventually (λi. A i ⊆ S) sequentially"
by (rule countable_basis_at_decseq) blast
have "eventually (λn. F n ∈ S) sequentially"
if "∀n. F n ∈ A n" "open S" "x ∈ S" for F S
using *(3)[of S] that by (auto elim: eventually_mono simp: subset_eq)
with * show "∃A. (∀i. open (A i)) ∧ (∀i. x ∈ A i) ∧ (∀F. (∀n. F n ∈ A n) ⟶ F ⇢ x)"
by (intro exI[of _ A]) (auto simp: tendsto_def)
qed
lemma (in first_countable_topology) sequentially_imp_eventually_nhds_within:
assumes "∀f. (∀n. f n ∈ s) ∧ f ⇢ a ⟶ eventually (λn. P (f n)) sequentially"
shows "eventually P (inf (nhds a) (principal s))"
proof (rule ccontr)
obtain A :: "nat ⇒ 'a set" where *:
"⋀i. open (A i)"
"⋀i. a ∈ A i"
"⋀F. ∀n. F n ∈ A n ⟹ F ⇢ a"
by (rule countable_basis) blast
assume "¬ ?thesis"
with * have "∃F. ∀n. F n ∈ s ∧ F n ∈ A n ∧ ¬ P (F n)"
unfolding eventually_inf_principal eventually_nhds
by (intro choice) fastforce
then obtain F where F: "∀n. F n ∈ s" and "∀n. F n ∈ A n" and F': "∀n. ¬ P (F n)"
by blast
with * have "F ⇢ a"
by auto
then have "eventually (λn. P (F n)) sequentially"
using assms F by simp
then show False
by (simp add: F')
qed
lemma (in first_countable_topology) eventually_nhds_within_iff_sequentially:
"eventually P (inf (nhds a) (principal s)) ⟷
(∀f. (∀n. f n ∈ s) ∧ f ⇢ a ⟶ eventually (λn. P (f n)) sequentially)"
proof (safe intro!: sequentially_imp_eventually_nhds_within)
assume "eventually P (inf (nhds a) (principal s))"
then obtain S where "open S" "a ∈ S" "∀x∈S. x ∈ s ⟶ P x"
by (auto simp: eventually_inf_principal eventually_nhds)
moreover
fix f
assume "∀n. f n ∈ s" "f ⇢ a"
ultimately show "eventually (λn. P (f n)) sequentially"
by (auto dest!: topological_tendstoD elim: eventually_mono)
qed
lemma (in first_countable_topology) eventually_nhds_iff_sequentially:
"eventually P (nhds a) ⟷ (∀f. f ⇢ a ⟶ eventually (λn. P (f n)) sequentially)"
using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
lemma Inf_as_limit:
fixes A::"'a::{linorder_topology, first_countable_topology, complete_linorder} set"
assumes "A ≠ {}"
shows "∃u. (∀n. u n ∈ A) ∧ u ⇢ Inf A"
proof (cases "Inf A ∈ A")
case True
show ?thesis
by (rule exI[of _ "λn. Inf A"], auto simp add: True)
next
case False
obtain y where "y ∈ A" using assms by auto
then have "Inf A < y" using False Inf_lower less_le by auto
obtain F :: "nat ⇒ 'a set" where F: "⋀i. open (F i)" "⋀i. Inf A ∈ F i"
"⋀u. (∀n. u n ∈ F n) ⟹ u ⇢ Inf A"
by (metis first_countable_topology_class.countable_basis)
define u where "u = (λn. SOME z. z ∈ F n ∧ z ∈ A)"
have "∃z. z ∈ U ∧ z ∈ A" if "Inf A ∈ U" "open U" for U
proof -
obtain b where "b > Inf A" "{Inf A ..<b} ⊆ U"
using open_right[OF ‹open U› ‹Inf A ∈ U› ‹Inf A < y›] by auto
obtain z where "z < b" "z ∈ A"
using ‹Inf A < b› Inf_less_iff by auto
then have "z ∈ {Inf A ..<b}"
by (simp add: Inf_lower)
then show ?thesis using ‹z ∈ A› ‹{Inf A ..<b} ⊆ U› by auto
qed
then have *: "u n ∈ F n ∧ u n ∈ A" for n
using ‹Inf A ∈ F n› ‹open (F n)› unfolding u_def by (metis (no_types, lifting) someI_ex)
then have "u ⇢ Inf A" using F(3) by simp
then show ?thesis using * by auto
qed
lemma tendsto_at_iff_sequentially:
"(f ⤏ a) (at x within s) ⟷ (∀X. (∀i. X i ∈ s - {x}) ⟶ X ⇢ x ⟶ ((f ∘ X) ⇢ a))"
for f :: "'a::first_countable_topology ⇒ _"
unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap
at_within_def eventually_nhds_within_iff_sequentially comp_def
by metis
lemma approx_from_above_dense_linorder:
fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
assumes "x < y"
shows "∃u. (∀n. u n > x) ∧ (u ⇢ x)"
proof -
obtain A :: "nat ⇒ 'a set" where A: "⋀i. open (A i)" "⋀i. x ∈ A i"
"⋀F. (∀n. F n ∈ A n) ⟹ F ⇢ x"
by (metis first_countable_topology_class.countable_basis)
define u where "u = (λn. SOME z. z ∈ A n ∧ z > x)"
have "∃z. z ∈ U ∧ x < z" if "x ∈ U" "open U" for U
using open_right[OF ‹open U› ‹x ∈ U› ‹x < y›]
by (meson atLeastLessThan_iff dense less_imp_le subset_eq)
then have *: "u n ∈ A n ∧ x < u n" for n
using ‹x ∈ A n› ‹open (A n)› unfolding u_def by (metis (no_types, lifting) someI_ex)
then have "u ⇢ x" using A(3) by simp
then show ?thesis using * by auto
qed
lemma approx_from_below_dense_linorder:
fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
assumes "x > y"
shows "∃u. (∀n. u n < x) ∧ (u ⇢ x)"
proof -
obtain A :: "nat ⇒ 'a set" where A: "⋀i. open (A i)" "⋀i. x ∈ A i"
"⋀F. (∀n. F n ∈ A n) ⟹ F ⇢ x"
by (metis first_countable_topology_class.countable_basis)
define u where "u = (λn. SOME z. z ∈ A n ∧ z < x)"
have "∃z. z ∈ U ∧ z < x" if "x ∈ U" "open U" for U
using open_left[OF ‹open U› ‹x ∈ U› ‹x > y›]
by (meson dense greaterThanAtMost_iff less_imp_le subset_eq)
then have *: "u n ∈ A n ∧ u n < x" for n
using ‹x ∈ A n› ‹open (A n)› unfolding u_def by (metis (no_types, lifting) someI_ex)
then have "u ⇢ x" using A(3) by simp
then show ?thesis using * by auto
qed
subsection ‹Function limit at a point›
abbreviation LIM :: "('a::topological_space ⇒ 'b::topological_space) ⇒ 'a ⇒ 'b ⇒ bool"
("((_)/ ─(_)/→ (_))" [60, 0, 60] 60)
where "f ─a→ L ≡ (f ⤏ L) (at a)"
lemma tendsto_within_open: "a ∈ S ⟹ open S ⟹ (f ⤏ l) (at a within S) ⟷ (f ─a→ l)"
by (simp add: tendsto_def at_within_open[where S = S])
lemma tendsto_within_open_NO_MATCH:
"a ∈ S ⟹ NO_MATCH UNIV S ⟹ open S ⟹ (f ⤏ l)(at a within S) ⟷ (f ⤏ l)(at a)"
for f :: "'a::topological_space ⇒ 'b::topological_space"
using tendsto_within_open by blast
lemma LIM_const_not_eq[tendsto_intros]: "k ≠ L ⟹ ¬ (λx. k) ─a→ L"
for a :: "'a::perfect_space" and k L :: "'b::t2_space"
by (simp add: tendsto_const_iff)
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
lemma LIM_const_eq: "(λx. k) ─a→ L ⟹ k = L"
for a :: "'a::perfect_space" and k L :: "'b::t2_space"
by (simp add: tendsto_const_iff)
lemma LIM_unique: "f ─a→ L ⟹ f ─a→ M ⟹ L = M"
for a :: "'a::perfect_space" and L M :: "'b::t2_space"
using at_neq_bot by (rule tendsto_unique)
lemma LIM_Uniq: "∃⇩≤⇩1L::'b::t2_space. f ─a→ L"
for a :: "'a::perfect_space"
by (auto simp add: Uniq_def LIM_unique)
text ‹Limits are equal for functions equal except at limit point.›
lemma LIM_equal: "∀x. x ≠ a ⟶ f x = g x ⟹ (f ─a→ l) ⟷ (g ─a→ l)"
by (simp add: tendsto_def eventually_at_topological)
lemma LIM_cong: "a = b ⟹ (⋀x. x ≠ b ⟹ f x = g x) ⟹ l = m ⟹ (f ─a→ l) ⟷ (g ─b→ m)"
by (simp add: LIM_equal)
lemma tendsto_cong_limit: "(f ⤏ l) F ⟹ k = l ⟹ (f ⤏ k) F"
by simp
lemma tendsto_at_iff_tendsto_nhds: "g ─l→ g l ⟷ (g ⤏ g l) (nhds l)"
unfolding tendsto_def eventually_at_filter
by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
lemma tendsto_compose: "g ─l→ g l ⟹ (f ⤏ l) F ⟹ ((λx. g (f x)) ⤏ g l) F"
unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
lemma tendsto_compose_eventually:
"g ─l→ m ⟹ (f ⤏ l) F ⟹ eventually (λx. f x ≠ l) F ⟹ ((λx. g (f x)) ⤏ m) F"
by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
lemma LIM_compose_eventually:
assumes "f ─a→ b"
and "g ─b→ c"
and "eventually (λx. f x ≠ b) (at a)"
shows "(λx. g (f x)) ─a→ c"
using assms(2,1,3) by (rule tendsto_compose_eventually)
lemma tendsto_compose_filtermap: "((g ∘ f) ⤏ T) F ⟷ (g ⤏ T) (filtermap f F)"
by (simp add: filterlim_def filtermap_filtermap comp_def)
lemma tendsto_compose_at:
assumes f: "(f ⤏ y) F" and g: "(g ⤏ z) (at y)" and fg: "eventually (λw. f w = y ⟶ g y = z) F"
shows "((g ∘ f) ⤏ z) F"
proof -
have "(∀⇩F a in F. f a ≠ y) ∨ g y = z"
using fg by force
moreover have "(g ⤏ z) (filtermap f F) ∨ ¬ (∀⇩F a in F. f a ≠ y)"
by (metis (no_types) filterlim_atI filterlim_def tendsto_mono f g)
ultimately show ?thesis
by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap)
qed
lemma tendsto_nhds_iff: "(f ⤏ (c :: 'a :: t1_space)) (nhds x) ⟷ f ─x→ c ∧ f x = c"
proof safe
assume lim: "(f ⤏ c) (nhds x)"
show "f x = c"
proof (rule ccontr)
assume "f x ≠ c"
hence "c ≠ f x"
by auto
then obtain A where A: "open A" "c ∈ A" "f x ∉ A"
by (subst (asm) separation_t1) auto
with lim obtain B where "open B" "x ∈ B" "⋀x. x ∈ B ⟹ f x ∈ A"
unfolding tendsto_def eventually_nhds by metis
with ‹f x ∉ A› show False
by blast
qed
show "(f ⤏ c) (at x)"
using lim by (rule filterlim_mono) (auto simp: at_within_def)
next
assume "f ─x→ f x" "c = f x"
thus "(f ⤏ f x) (nhds x)"
unfolding tendsto_def eventually_at_filter by (fast elim: eventually_mono)
qed
subsubsection ‹Relation of ‹LIM› and ‹LIMSEQ››
lemma (in first_countable_topology) sequentially_imp_eventually_within:
"(∀f. (∀n. f n ∈ s ∧ f n ≠ a) ∧ f ⇢ a ⟶ eventually (λn. P (f n)) sequentially) ⟹
eventually P (at a within s)"
unfolding at_within_def
by (intro sequentially_imp_eventually_nhds_within) auto
lemma (in first_countable_topology) sequentially_imp_eventually_at:
"(∀f. (∀n. f n ≠ a) ∧ f ⇢ a ⟶ eventually (λn. P (f n)) sequentially) ⟹ eventually P (at a)"
using sequentially_imp_eventually_within [where s=UNIV] by simp
lemma LIMSEQ_SEQ_conv:
"(∀S. (∀n. S n ≠ a) ∧ S ⇢ a ⟶ (λn. X (S n)) ⇢ L) ⟷ X ─a→ L" (is "?lhs=?rhs")
for a :: "'a::first_countable_topology" and L :: "'b::topological_space"
proof
assume ?lhs then show ?rhs
by (simp add: sequentially_imp_eventually_within tendsto_def)
next
assume ?rhs then show ?lhs
using tendsto_compose_eventually eventuallyI by blast
qed
lemma sequentially_imp_eventually_at_left:
fixes a :: "'a::{linorder_topology,first_countable_topology}"
assumes b[simp]: "b < a"
and *: "⋀f. (⋀n. b < f n) ⟹ (⋀n. f n < a) ⟹ incseq f ⟹ f ⇢ a ⟹
eventually (λn. P (f n)) sequentially"
shows "eventually P (at_left a)"
proof (safe intro!: sequentially_imp_eventually_within)
fix X
assume X: "∀n. X n ∈ {..< a} ∧ X n ≠ a" "X ⇢ a"
show "eventually (λn. P (X n)) sequentially"
proof (rule ccontr)
assume neg: "¬ ?thesis"
have "∃s. ∀n. (¬ P (X (s n)) ∧ b < X (s n)) ∧ (X (s n) ≤ X (s (Suc n)) ∧ Suc (s n) ≤ s (Suc n))"
(is "∃s. ?P s")
proof (rule dependent_nat_choice)
have "¬ eventually (λn. b < X n ⟶ P (X n)) sequentially"
by (intro not_eventually_impI neg order_tendstoD(1) [OF X(2) b])
then show "∃x. ¬ P (X x) ∧ b < X x"
by (auto dest!: not_eventuallyD)
next
fix x n
have "¬ eventually (λn. Suc x ≤ n ⟶ b < X n ⟶ X x < X n ⟶ P (X n)) sequentially"
using X
by (intro not_eventually_impI order_tendstoD(1)[OF X(2)] eventually_ge_at_top neg) auto
then show "∃n. (¬ P (X n) ∧ b < X n) ∧ (X x ≤ X n ∧ Suc x ≤ n)"
by (auto dest!: not_eventuallyD)
qed
then obtain s where "?P s" ..
with X have "b < X (s n)"
and "X (s n) < a"
and "incseq (λn. X (s n))"
and "(λn. X (s n)) ⇢ a"
and "¬ P (X (s n))"
for n
by (auto simp: strict_mono_Suc_iff Suc_le_eq incseq_Suc_iff
intro!: LIMSEQ_subseq_LIMSEQ[OF ‹X ⇢ a›, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False
by auto
qed
qed
lemma tendsto_at_left_sequentially:
fixes a b :: "'b::{linorder_topology,first_countable_topology}"
assumes "b < a"
assumes *: "⋀S. (⋀n. S n < a) ⟹ (⋀n. b < S n) ⟹ incseq S ⟹ S ⇢ a ⟹
(λn. X (S n)) ⇢ L"
shows "(X ⤏ L) (at_left a)"
using assms by (simp add: tendsto_def [where l=L] sequentially_imp_eventually_at_left)
lemma sequentially_imp_eventually_at_right:
fixes a b :: "'a::{linorder_topology,first_countable_topology}"
assumes b[simp]: "a < b"
assumes *: "⋀f. (⋀n. a < f n) ⟹ (⋀n. f n < b) ⟹ decseq f ⟹ f ⇢ a ⟹
eventually (λn. P (f n)) sequentially"
shows "eventually P (at_right a)"
proof (safe intro!: sequentially_imp_eventually_within)
fix X
assume X: "∀n. X n ∈ {a <..} ∧ X n ≠ a" "X ⇢ a"
show "eventually (λn. P (X n)) sequentially"
proof (rule ccontr)
assume neg: "¬ ?thesis"
have "∃s. ∀n. (¬ P (X (s n)) ∧ X (s n) < b) ∧ (X (s (Suc n)) ≤ X (s n) ∧ Suc (s n) ≤ s (Suc n))"
(is "∃s. ?P s")
proof (rule dependent_nat_choice)
have "¬ eventually (λn. X n < b ⟶ P (X n)) sequentially"
by (intro not_eventually_impI neg order_tendstoD(2) [OF X(2) b])
then show "∃x. ¬ P (X x) ∧ X x < b"
by (auto dest!: not_eventuallyD)
next
fix x n
have "¬ eventually (λn. Suc x ≤ n ⟶ X n < b ⟶ X n < X x ⟶ P (X n)) sequentially"
using X
by (intro not_eventually_impI order_tendstoD(2)[OF X(2)] eventually_ge_at_top neg) auto
then show "∃n. (¬ P (X n) ∧ X n < b) ∧ (X n ≤ X x ∧ Suc x ≤ n)"
by (auto dest!: not_eventuallyD)
qed
then obtain s where "?P s" ..
with X have "a < X (s n)"
and "X (s n) < b"
and "decseq (λn. X (s n))"
and "(λn. X (s n)) ⇢ a"
and "¬ P (X (s n))"
for n
by (auto simp: strict_mono_Suc_iff Suc_le_eq decseq_Suc_iff
intro!: LIMSEQ_subseq_LIMSEQ[OF ‹X ⇢ a›, unfolded comp_def])
from *[OF this(1,2,3,4)] this(5) show False
by auto
qed
qed
lemma tendsto_at_right_sequentially:
fixes a :: "_ :: {linorder_topology, first_countable_topology}"
assumes "a < b"
and *: "⋀S. (⋀n. a < S n) ⟹ (⋀n. S n < b) ⟹ decseq S ⟹ S ⇢ a ⟹
(λn. X (S n)) ⇢ L"
shows "(X ⤏ L) (at_right a)"
using assms by (simp add: tendsto_def [where l=L] sequentially_imp_eventually_at_right)
subsection ‹Continuity›
subsubsection ‹Continuity on a set›
definition continuous_on :: "'a set ⇒ ('a::topological_space ⇒ 'b::topological_space) ⇒ bool"
where "continuous_on s f ⟷ (∀x∈s. (f ⤏ f x) (at x within s))"
lemma continuous_on_cong [cong]:
"s = t ⟹ (⋀x. x ∈ t ⟹ f x = g x) ⟹ continuous_on s f ⟷ continuous_on t g"
unfolding continuous_on_def
by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
lemma continuous_on_cong_simp:
"s = t ⟹ (⋀x. x ∈ t =simp=> f x = g x) ⟹ continuous_on s f ⟷ continuous_on t g"
unfolding simp_implies_def by (rule continuous_on_cong)
lemma continuous_on_topological:
"continuous_on s f ⟷
(∀x∈s. ∀B. open B ⟶ f x ∈ B ⟶ (∃A. open A ∧ x ∈ A ∧ (∀y∈s. y ∈ A ⟶ f y ∈ B)))"
unfolding continuous_on_def tendsto_def eventually_at_topological by metis
lemma continuous_on_open_invariant:
"continuous_on s f ⟷ (∀B. open B ⟶ (∃A. open A ∧ A ∩ s = f -` B ∩ s))"
proof safe
fix B :: "'b set"
assume "continuous_on s f" "open B"
then have "∀x∈f -` B ∩ s. (∃A. open A ∧ x ∈ A ∧ s ∩ A ⊆ f -` B)"
by (auto simp: continuous_on_topological subset_eq Ball_def imp_conjL)
then obtain A where "∀x∈f -` B ∩ s. open (A x) ∧ x ∈ A x ∧ s ∩ A x ⊆ f -` B"
unfolding bchoice_iff ..
then show "∃A. open A ∧ A ∩ s = f -` B ∩ s"
by (intro exI[of _ "⋃x∈f -` B ∩ s. A x"]) auto
next
assume B: "∀B. open B ⟶ (∃A. open A ∧ A ∩ s = f -` B ∩ s)"
show "continuous_on s f"
unfolding continuous_on_topological
proof safe
fix x B
assume "x ∈ s" "open B" "f x ∈ B"
with B obtain A where A: "open A" "A ∩ s = f -` B ∩ s"
by auto
with ‹x ∈ s› ‹f x ∈ B› show "∃A. open A ∧ x ∈ A ∧ (∀y∈s. y ∈ A ⟶ f y ∈ B)"
by (intro exI[of _ A]) auto
qed
qed
lemma continuous_on_open_vimage:
"open s ⟹ continuous_on s f ⟷ (∀B. open B ⟶ open (f -` B ∩ s))"
unfolding continuous_on_open_invariant
by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
corollary continuous_imp_open_vimage:
assumes "continuous_on s f" "open s" "open B" "f -` B ⊆ s"
shows "open (f -` B)"
by (metis assms continuous_on_open_vimage le_iff_inf)
corollary open_vimage[continuous_intros]:
assumes "open s"
and "continuous_on UNIV f"
shows "open (f -` s)"
using assms by (simp add: continuous_on_open_vimage [OF open_UNIV])
lemma continuous_on_closed_invariant:
"continuous_on s f ⟷ (∀B. closed B ⟶ (∃A. closed A ∧ A ∩ s = f -` B ∩ s))"
proof -
have *: "(⋀A. P A ⟷ Q (- A)) ⟹ (∀A. P A) ⟷ (∀A. Q A)"
for P Q :: "'b set ⇒ bool"
by (metis double_compl)
show ?thesis
unfolding continuous_on_open_invariant
by (intro *) (auto simp: open_closed[symmetric])
qed
lemma continuous_on_closed_vimage:
"closed s ⟹ continuous_on s f ⟷ (∀B. closed B ⟶ closed (f -` B ∩ s))"
unfolding continuous_on_closed_invariant
by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
corollary closed_vimage_Int[continuous_intros]:
assumes "closed s"
and "continuous_on t f"
and t: "closed t"
shows "closed (f -` s ∩ t)"
using assms by (simp add: continuous_on_closed_vimage [OF t])
corollary closed_vimage[continuous_intros]:
assumes "closed s"
and "continuous_on UNIV f"
shows "closed (f -` s)"
using closed_vimage_Int [OF assms] by simp
lemma continuous_on_empty [simp]: "continuous_on {} f"
by (simp add: continuous_on_def)
lemma continuous_on_sing [simp]: "continuous_on {x} f"
by (simp add: continuous_on_def at_within_def)
lemma continuous_on_open_Union:
"(⋀s. s ∈ S ⟹ open s) ⟹ (⋀s. s ∈ S ⟹ continuous_on s f) ⟹ continuous_on (⋃S) f"
unfolding continuous_on_def
by safe (metis open_Union at_within_open UnionI)
lemma continuous_on_open_UN:
"(⋀s. s ∈ S ⟹ open (A s)) ⟹ (⋀s. s ∈ S ⟹ continuous_on (A s) f) ⟹
continuous_on (⋃s∈S. A s) f"
by (rule continuous_on_open_Union) auto
lemma continuous_on_open_Un:
"open s ⟹ open t ⟹ continuous_on s f ⟹ continuous_on t f ⟹ continuous_on (s ∪ t) f"
using continuous_on_open_Union [of "{s,t}"] by auto
lemma continuous_on_closed_Un:
"closed s ⟹ closed t ⟹ continuous_on s f ⟹ continuous_on t f ⟹ continuous_on (s ∪ t) f"
by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
lemma continuous_on_closed_Union:
assumes "finite I"
"⋀i. i ∈ I ⟹ closed (U i)"
"⋀i. i ∈ I ⟹ continuous_on (U i) f"
shows "continuous_on (⋃ i ∈ I. U i) f"
using assms
by (induction I) (auto intro!: continuous_on_closed_Un)
lemma continuous_on_If:
assumes closed: "closed s" "closed t"
and cont: "continuous_on s f" "continuous_on t g"
and P: "⋀x. x ∈ s ⟹ ¬ P x ⟹ f x = g x" "⋀x. x ∈ t ⟹ P x ⟹ f x = g x"
shows "continuous_on (s ∪ t) (λx. if P x then f x else g x)"
(is "continuous_on _ ?h")
proof-
from P have "∀x∈s. f x = ?h x" "∀x∈t. g x = ?h x"
by auto
with cont have "continuous_on s ?h" "continuous_on t ?h"
by simp_all
with closed show ?thesis
by (rule continuous_on_closed_Un)
qed
lemma continuous_on_cases:
"closed s ⟹ closed t ⟹ continuous_on s f ⟹ continuous_on t g ⟹
∀x. (x∈s ∧ ¬ P x) ∨ (x ∈ t ∧ P x) ⟶ f x = g x ⟹
continuous_on (s ∪ t) (λx. if P x then f x else g x)"
by (rule continuous_on_If) auto
lemma continuous_on_id[continuous_intros,simp]: "continuous_on s (λx. x)"
unfolding continuous_on_def by fast
lemma continuous_on_id'[continuous_intros,simp]: "continuous_on s id"
unfolding continuous_on_def id_def by fast
lemma continuous_on_const[continuous_intros,simp]: "continuous_on s (λx. c)"
unfolding continuous_on_def by auto
lemma continuous_on_subset: "continuous_on s f ⟹ t ⊆ s ⟹ continuous_on t f"
unfolding continuous_on_def
by (metis subset_eq tendsto_within_subset)
lemma continuous_on_compose[continuous_intros]:
"continuous_on s f ⟹ continuous_on (f ` s) g ⟹ continuous_on s (g ∘ f)"
unfolding continuous_on_topological by simp metis
lemma continuous_on_compose2:
"continuous_on t g ⟹ continuous_on s f ⟹ f ` s ⊆ t ⟹ continuous_on s (λx. g (f x))"
using continuous_on_compose[of s f g] continuous_on_subset by (force simp add: comp_def)
lemma continuous_on_generate_topology:
assumes *: "open = generate_topology X"
and **: "⋀B. B ∈ X ⟹ ∃C. open C ∧ C ∩ A = f -` B ∩ A"
shows "continuous_on A f"
unfolding continuous_on_open_invariant
proof safe
fix B :: "'a set"
assume "open B"
then show "∃C. open C ∧ C ∩ A = f -` B ∩ A"
unfolding *
proof induct
case (UN K)
then obtain C where "⋀k. k ∈ K ⟹ open (C k)" "⋀k. k ∈ K ⟹ C k ∩ A = f -` k ∩ A"
by metis
then show ?case
by (intro exI[of _ "⋃k∈K. C k"]) blast
qed (auto intro: **)
qed
lemma continuous_onI_mono:
fixes f :: "'a::linorder_topology ⇒ 'b::{dense_order,linorder_topology}"
assumes "open (f`A)"
and mono: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≤ y ⟹ f x ≤ f y"
shows "continuous_on A f"
proof (rule continuous_on_generate_topology[OF open_generated_order], safe)
have monoD: "⋀x y. x ∈ A ⟹ y ∈ A ⟹ f x < f y ⟹ x < y"
by (auto simp: not_le[symmetric] mono)
have "∃x. x ∈ A ∧ f x < b ∧ a < x" if a: "a ∈ A" and fa: "f a < b" for a b
proof -
obtain y where "f a < y" "{f a ..< y} ⊆ f`A"
using open_right[OF ‹open (f`A)›, of "f a" b] a fa
by auto
obtain z where z: "f a < z" "z < min b y"
using dense[of "f a" "min b y"] ‹f a < y› ‹f a < b› by auto
then obtain c where "z = f c" "c ∈ A"
using ‹{f a ..< y} ⊆ f`A›[THEN subsetD, of z] by (auto simp: less_imp_le)
with a z show ?thesis
by (auto intro!: exI[of _ c] simp: monoD)
qed
then show "∃C. open C ∧ C ∩ A = f -` {..<b} ∩ A" for b
by (intro exI[of _ "(⋃x∈{x∈A. f x < b}. {..< x})"])
(auto intro: le_less_trans[OF mono] less_imp_le)
have "∃x. x ∈ A ∧ b < f x ∧ x < a" if a: "a ∈ A" and fa: "b < f a" for a b
proof -
note a fa
moreover
obtain y where "y < f a" "{y <.. f a} ⊆ f`A"
using open_left[OF ‹open (f`A)›, of "f a" b] a fa
by auto
then obtain z where z: "max b y < z" "z < f a"
using dense[of "max b y" "f a"] ‹y < f a› ‹b < f a› by auto
then obtain c where "z = f c" "c ∈ A"
using ‹{y <.. f a} ⊆ f`A›[THEN subsetD, of z] by (auto simp: less_imp_le)
with a z show ?thesis
by (auto intro!: exI[of _ c] simp: monoD)
qed
then show "∃C. open C ∧ C ∩ A = f -` {b <..} ∩ A" for b
by (intro exI[of _ "(⋃x∈{x∈A. b < f x}. {x <..})"])
(auto intro: less_le_trans[OF _ mono] less_imp_le)
qed
lemma continuous_on_IccI:
"⟦(f ⤏ f a) (at_right a);
(f ⤏ f b) (at_left b);
(⋀x. a < x ⟹ x < b ⟹ f ─x→ f x); a < b⟧ ⟹
continuous_on {a .. b} f"
for a::"'a::linorder_topology"
using at_within_open[of _ "{a<..<b}"]
by (auto simp: continuous_on_def at_within_Icc_at_right at_within_Icc_at_left le_less
at_within_Icc_at)
lemma
fixes a b::"'a::linorder_topology"
assumes "continuous_on {a .. b} f" "a < b"
shows continuous_on_Icc_at_rightD: "(f ⤏ f a) (at_right a)"
and continuous_on_Icc_at_leftD: "(f ⤏ f b) (at_left b)"
using assms
by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
dest: bspec[where x=a] bspec[where x=b])
lemma continuous_on_discrete [simp]:
"continuous_on A (f :: 'a :: discrete_topology ⇒ _)"
by (auto simp: continuous_on_def at_discrete)
lemma continuous_on_of_nat [continuous_intros]:
assumes "continuous_on A f"
shows "continuous_on A (λn. of_nat (f n))"
using continuous_on_compose[OF assms continuous_on_discrete[of _ of_nat]]
by (simp add: o_def)
lemma continuous_on_of_int [continuous_intros]:
assumes "continuous_on A f"
shows "continuous_on A (λn. of_int (f n))"
using continuous_on_compose[OF assms continuous_on_discrete[of _ of_int]]
by (simp add: o_def)
subsubsection ‹Continuity at a point›
definition continuous :: "'a::t2_space filter ⇒ ('a ⇒ 'b::topological_space) ⇒ bool"
where "continuous F f ⟷ (f ⤏ f (Lim F (λx. x))) F"
lemma continuous_bot[continuous_intros, simp]: "continuous bot f"
unfolding continuous_def by auto
lemma continuous_trivial_limit: "trivial_limit net ⟹ continuous net f"
by simp
lemma continuous_within: "continuous (at x within s) f ⟷ (f ⤏ f x) (at x within s)"
by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def)
lemma continuous_within_topological:
"continuous (at x within s) f ⟷
(∀B. open B ⟶ f x ∈ B ⟶ (∃A. open A ∧ x ∈ A ∧ (∀y∈s. y ∈ A ⟶ f y ∈ B)))"
unfolding continuous_within tendsto_def eventually_at_topological by metis
lemma continuous_within_compose[continuous_intros]:
"continuous (at x within s) f ⟹ continuous (at (f x) within f ` s) g ⟹
continuous (at x within s) (g ∘ f)"
by (simp add: continuous_within_topological) metis
lemma continuous_within_compose2:
"continuous (at x within s) f ⟹ continuous (at (f x) within f ` s) g ⟹
continuous (at x within s) (λx. g (f x))"
using continuous_within_compose[of x s f g] by (simp add: comp_def)
lemma continuous_at: "continuous (at x) f ⟷ f ─x→ f x"
using continuous_within[of x UNIV f] by simp
lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (λx. x)"
unfolding continuous_within by (rule tendsto_ident_at)
lemma continuous_id[continuous_intros, simp]: "continuous (at x within S) id"
by (simp add: id_def)
lemma continuous_const[continuous_intros, simp]: "continuous F (λx. c)"
unfolding continuous_def by (rule tendsto_const)
lemma continuous_on_eq_continuous_within:
"continuous_on s f ⟷ (∀x∈s. continuous (at x within s) f)"
unfolding continuous_on_def continuous_within ..
lemma continuous_discrete [simp]:
"continuous (at x within A) (f :: 'a :: discrete_topology ⇒ _)"
by (auto simp: continuous_def at_discrete)
abbreviation isCont :: "('a::t2_space ⇒ 'b::topological_space) ⇒ 'a ⇒ bool"
where "isCont f a ≡ continuous (at a) f"
lemma isCont_def: "isCont f a ⟷ f ─a→ f a"
by (rule continuous_at)
lemma isContD: "isCont f x ⟹ f ─x→ f x"
by (simp add: isCont_def)
lemma isCont_cong:
assumes "eventually (λx. f x = g x) (nhds x)"
shows "isCont f x ⟷ isCont g x"
proof -
from assms have [simp]: "f x = g x"
by (rule eventually_nhds_x_imp_x)
from assms have "eventually (λx. f x = g x) (at x)"
by (auto simp: eventually_at_filter elim!: eventually_mono)
with assms have "isCont f x ⟷ isCont g x" unfolding isCont_def
by (intro filterlim_cong) (auto elim!: eventually_mono)
with assms show ?thesis by simp
qed
lemma continuous_at_imp_continuous_at_within: "isCont f x ⟹ continuous (at x within s) f"
by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
lemma continuous_on_eq_continuous_at: "open s ⟹ continuous_on s f ⟷ (∀x∈s. isCont f x)"
by (simp add: continuous_on_def continuous_at at_within_open[of _ s])
lemma continuous_within_open: "a ∈ A ⟹ open A ⟹ continuous (at a within A) f ⟷ isCont f a"
by (simp add: at_within_open_NO_MATCH)
lemma continuous_at_imp_continuous_on: "∀x∈s. isCont f x ⟹ continuous_on s f"
by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
lemma isCont_o2: "isCont f a ⟹ isCont g (f a) ⟹ isCont (λx. g (f x)) a"
unfolding isCont_def by (rule tendsto_compose)
lemma continuous_at_compose[continuous_intros]: "isCont f a ⟹ isCont g (f a) ⟹ isCont (g ∘ f) a"
unfolding o_def by (rule isCont_o2)
lemma isCont_tendsto_compose: "isCont g l ⟹ (f ⤏ l) F ⟹ ((λx. g (f x)) ⤏ g l) F"
unfolding isCont_def by (rule tendsto_compose)
lemma continuous_on_tendsto_compose:
assumes f_cont: "continuous_on s f"
and g: "(g ⤏ l) F"
and l: "l ∈ s"
and ev: "∀⇩Fx in F. g x ∈ s"
shows "((λx. f (g x)) ⤏ f l) F"
proof -
from f_cont l have f: "(f ⤏ f l) (at l within s)"
by (simp add: continuous_on_def)
have i: "((λx. if g x = l then f l else f (g x)) ⤏ f l) F"
by (rule filterlim_If)
(auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g]
simp: filterlim_at eventually_inf_principal eventually_mono[OF ev])
show ?thesis
by (rule filterlim_cong[THEN iffD1[OF _ i]]) auto
qed
lemma continuous_within_compose3:
"isCont g (f x) ⟹ continuous (at x within s) f ⟹ continuous (at x within s) (λx. g (f x))"
using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
lemma at_within_isCont_imp_nhds:
fixes f:: "'a:: {t2_space,perfect_space} ⇒ 'b:: t2_space"
assumes "∀⇩F w in at z. f w = g w" "isCont f z" "isCont g z"
shows "∀⇩F w in nhds z. f w = g w"
proof -
have "g ─z→ f z"
using assms isContD tendsto_cong by blast
moreover have "g ─z→ g z" using ‹isCont g z› using isCont_def by blast
ultimately have "f z=g z" using LIM_unique by auto
moreover have "∀⇩F x in nhds z. x ≠ z ⟶ f x = g x"
using assms unfolding eventually_at_filter by auto
ultimately show ?thesis
by (auto elim:eventually_mono)
qed
lemma filtermap_nhds_open_map':
assumes cont: "isCont f a"
and "open A" "a ∈ A"
and open_map: "⋀S. open S ⟹ S ⊆ A ⟹ open (f ` S)"
shows "filtermap f (nhds a) = nhds (f a)"
unfolding filter_eq_iff
proof safe
fix P
assume "eventually P (filtermap f (nhds a))"
then obtain S where S: "open S" "a ∈ S" "∀x∈S. P (f x)"
by (auto simp: eventually_filtermap eventually_nhds)
show "eventually P (nhds (f a))"
unfolding eventually_nhds
proof (rule exI [of _ "f ` (A ∩ S)"], safe)
show "open (f ` (A ∩ S))"
using S by (intro open_Int assms) auto
show "f a ∈ f ` (A ∩ S)"
using assms S by auto
show "P (f x)" if "x ∈ A" "x ∈ S" for x
using S that by auto
qed
qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
lemma filtermap_nhds_open_map:
assumes cont: "isCont f a"
and open_map: "⋀S. open S ⟹ open (f`S)"
shows "filtermap f (nhds a) = nhds (f a)"
using cont filtermap_nhds_open_map' open_map by blast
lemma continuous_at_split:
"continuous (at x) f ⟷ continuous (at_left x) f ∧ continuous (at_right x) f"
for x :: "'a::linorder_topology"
by (simp add: continuous_within filterlim_at_split)
lemma continuous_on_max [continuous_intros]:
fixes f g :: "'a::topological_space ⇒ 'b::linorder_topology"
shows "continuous_on A f ⟹ continuous_on A g ⟹ continuous_on A (λx. max (f x) (g x))"
by (auto simp: continuous_on_def intro!: tendsto_max)
lemma continuous_on_min [continuous_intros]:
fixes f g :: "'a::topological_space ⇒ 'b::linorder_topology"
shows "continuous_on A f ⟹ continuous_on A g ⟹ continuous_on A (λx. min (f x) (g x))"
by (auto simp: continuous_on_def intro!: tendsto_min)
lemma continuous_max [continuous_intros]:
fixes f :: "'a::t2_space ⇒ 'b::linorder_topology"
shows "⟦continuous F f; continuous F g⟧ ⟹ continuous F (λx. (max (f x) (g x)))"
by (simp add: tendsto_max continuous_def)
lemma continuous_min [continuous_intros]:
fixes f :: "'a::t2_space ⇒ 'b::linorder_topology"
shows "⟦continuous F f; continuous F g⟧ ⟹ continuous F (λx. (min (f x) (g x)))"
by (simp add: tendsto_min continuous_def)
text ‹
The following open/closed Collect lemmas are ported from
Sébastien Gouëzel's ‹Ergodic_Theory›.
›
lemma open_Collect_neq:
fixes f g :: "'a::topological_space ⇒ 'b::t2_space"
assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
shows "open {x. f x ≠ g x}"
proof (rule openI)
fix t
assume "t ∈ {x. f x ≠ g x}"
then obtain U V where *: "open U" "open V" "f t ∈ U" "g t ∈ V" "U ∩ V = {}"
by (auto simp add: separation_t2)
with open_vimage[OF ‹open U› f] open_vimage[OF ‹open V› g]
show "∃T. open T ∧ t ∈ T ∧ T ⊆ {x. f x ≠ g x}"
by (intro exI[of _ "f -` U ∩ g -` V"]) auto
qed
lemma closed_Collect_eq:
fixes f g :: "'a::topological_space ⇒ 'b::t2_space"
assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
shows "closed {x. f x = g x}"
using open_Collect_neq[OF f g] by (simp add: closed_def Collect_neg_eq)
lemma open_Collect_less:
fixes f g :: "'a::topological_space ⇒ 'b::linorder_topology"
assumes f: "continuous_on UNIV f" and g: "continuous_on UNIV g"
shows "open {x. f x < g x}"
proof (rule openI)
fix t
assume t: "t ∈ {x. f x < g x}"
show "∃T. open T ∧ t ∈ T ∧ T ⊆ {x. f x < g x}"
proof (cases "∃z. f t < z ∧ z < g t")
case True
then obtain z where "f t < z ∧ z < g t" by blast
then show ?thesis
using open_vimage[OF _ f, of "{..< z}"] open_vimage[OF _ g, of "{z <..}"]
by (intro exI[of _ "f -` {..<z} ∩ g -` {z<..}"]) auto
next
case False
then have *: "{g t ..} = {f t <..}" "{..< g t} = {.. f t}"
using t by (auto intro: leI)
show ?thesis
using open_vimage[OF _ f, of "{..< g t}"] open_vimage[OF _ g, of "{f t <..}"] t
apply (intro exI[of _ "f -` {..< g t} ∩ g -` {f t<..}"])
apply (simp add: open_Int)
apply (auto simp add: *)
done
qed
qed
lemma closed_Collect_le:
fixes f g :: "'a :: topological_space ⇒ 'b::linorder_topology"
assumes f: "continuous_on UNIV f"
and g: "continuous_on UNIV g"
shows "closed {x. f x ≤ g x}"
using open_Collect_less [OF g f]
by (simp add: closed_def Collect_neg_eq[symmetric] not_le)
subsubsection ‹Open-cover compactness›
context topological_space
begin
definition compact :: "'a set ⇒ bool" where
compact_eq_Heine_Borel:
"compact S ⟷ (∀C. (∀c∈C. open c) ∧ S ⊆ ⋃C ⟶ (∃D⊆C. finite D ∧ S ⊆ ⋃D))"
lemma compactI:
assumes "⋀C. ∀t∈C. open t ⟹ s ⊆ ⋃C ⟹ ∃C'. C' ⊆ C ∧ finite C' ∧ s ⊆ ⋃C'"
shows "compact s"
unfolding compact_eq_Heine_Borel using assms by metis
lemma compact_empty[simp]: "compact {}"
by (auto intro!: compactI)
lemma compactE:
assumes "compact S" "S ⊆ ⋃𝒯" "⋀B. B ∈ 𝒯 ⟹ open B"
obtains 𝒯' where "𝒯' ⊆ 𝒯" "finite 𝒯'" "S ⊆ ⋃𝒯'"
by (meson assms compact_eq_Heine_Borel)
lemma compactE_image:
assumes "compact S"
and opn: "⋀T. T ∈ C ⟹ open (f T)"
and S: "S ⊆ (⋃c∈C. f c)"
obtains C' where "C' ⊆ C" and "finite C'" and "S ⊆ (⋃c∈C'. f c)"
apply (rule compactE[OF ‹compact S› S])
using opn apply force
by (metis finite_subset_image)
lemma compact_Int_closed [intro]:
assumes "compact S"
and "closed T"
shows "compact (S ∩ T)"
proof (rule compactI)
fix C
assume C: "∀c∈C. open c"
assume cover: "S ∩ T ⊆ ⋃C"
from C ‹closed T› have "∀c∈C ∪ {- T}. open c"
by auto
moreover from cover have "S ⊆ ⋃(C ∪ {- T})"
by auto
ultimately have "∃D⊆C ∪ {- T}. finite D ∧ S ⊆ ⋃D"
using ‹compact S› unfolding compact_eq_Heine_Borel by auto
then obtain D where "D ⊆ C ∪ {- T} ∧ finite D ∧ S ⊆ ⋃D" ..
then show "∃D⊆C. finite D ∧ S ∩ T ⊆ ⋃D"
by (intro exI[of _ "D - {-T}"]) auto
qed
lemma compact_diff: "⟦compact S; open T⟧ ⟹ compact(S - T)"
by (simp add: Diff_eq compact_Int_closed open_closed)
lemma inj_setminus: "inj_on uminus (A::'a set set)"
by (auto simp: inj_on_def)
subsection ‹Finite intersection property›
lemma compact_fip:
"compact U ⟷
(∀A. (∀a∈A. closed a) ⟶ (∀B ⊆ A. finite B ⟶ U ∩ ⋂B ≠ {}) ⟶ U ∩ ⋂A ≠ {})"
(is "_ ⟷ ?R")
proof (safe intro!: compact_eq_Heine_Borel[THEN iffD2])
fix A
assume "compact U"
assume A: "∀a∈A. closed a" "U ∩ ⋂A = {}"
assume fin: "∀B ⊆ A. finite B ⟶ U ∩ ⋂B ≠ {}"
from A have "(∀a∈uminus`A. open a) ∧ U ⊆ ⋃(uminus`A)"
by auto
with ‹compact U› obtain B where "B ⊆ A" "finite (uminus`B)" "U ⊆ ⋃(uminus`B)"
unfolding compact_eq_Heine_Borel by (metis subset_image_iff)
with fin[THEN spec, of B] show False
by (auto dest: finite_imageD intro: inj_setminus)
next
fix A
assume ?R
assume "∀a∈A. open a" "U ⊆ ⋃A"
then have "U ∩ ⋂(uminus`A) = {}" "∀a∈uminus`A. closed a"
by auto
with ‹?R› obtain B where "B ⊆ A" "finite (uminus`B)" "U ∩ ⋂(uminus`B) = {}"
by (metis subset_image_iff)
then show "∃T⊆A. finite T ∧ U ⊆ ⋃T"
by (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
qed
lemma compact_imp_fip:
assumes "compact S"
and "⋀T. T ∈ F ⟹ closed T"
and "⋀F'. finite F' ⟹ F' ⊆ F ⟹ S ∩ (⋂F') ≠ {}"
shows "S ∩ (⋂F) ≠ {}"
using assms unfolding compact_fip by auto
lemma compact_imp_fip_image:
assumes "compact s"
and P: "⋀i. i ∈ I ⟹ closed (f i)"
and Q: "⋀I'. finite I' ⟹ I' ⊆ I ⟹ (s ∩ (⋂i∈I'. f i) ≠ {})"
shows "s ∩ (⋂i∈I. f i) ≠ {}"
proof -
from P have "∀i ∈ f ` I. closed i"
by blast
moreover have "∀A. finite A ∧ A ⊆ f ` I ⟶ (s ∩ (⋂A) ≠ {})"
by (metis Q finite_subset_image)
ultimately show "s ∩ (⋂(f ` I)) ≠ {}"
by (metis ‹compact s› compact_imp_fip)
qed
end
lemma (in t2_space) compact_imp_closed:
assumes "compact s"
shows "closed s"
unfolding closed_def
proof (rule openI)
fix y
assume "y ∈ - s"
let ?C = "⋃x∈s. {u. open u ∧ x ∈ u ∧ eventually (λy. y ∉ u) (nhds y)}"
have "s ⊆ ⋃?C"
proof
fix x
assume "x ∈ s"
with ‹y ∈ - s› have "x ≠ y" by clarsimp
then have "∃u v. open u ∧ open v ∧ x ∈ u ∧ y ∈ v ∧ u ∩ v = {}"
by (rule hausdorff)
with ‹x ∈ s› show "x ∈ ⋃?C"
unfolding eventually_nhds by auto
qed
then obtain D where "D ⊆ ?C" and "finite D" and "s ⊆ ⋃D"
by (rule compactE [OF ‹compact s›]) auto
from ‹D ⊆ ?C› have "∀x∈D. eventually (λy. y ∉ x) (nhds y)"
by auto
with ‹finite D› have "eventually (λy. y ∉ ⋃D) (nhds y)"
by (simp add: eventually_ball_finite)
with ‹s ⊆ ⋃D› have "eventually (λy. y ∉ s) (nhds y)"
by (auto elim!: eventually_mono)
then show "∃t. open t ∧ y ∈ t ∧ t ⊆ - s"
by (simp add: eventually_nhds subset_eq)
qed
lemma compact_continuous_image:
assumes f: "continuous_on s f"
and s: "compact s"
shows "compact (f ` s)"
proof (rule compactI)
fix C
assume "∀c∈C. open c" and cover: "f`s ⊆ ⋃C"
with f have "∀c∈C. ∃A. open A ∧ A ∩ s = f -` c ∩ s"
unfolding continuous_on_open_invariant by blast
then obtain A where A: "∀c∈C. open (A c) ∧ A c ∩ s = f -` c ∩ s"
unfolding bchoice_iff ..
with cover have "⋀c. c ∈ C ⟹ open (A c)" "s ⊆ (⋃c∈C. A c)"
by (fastforce simp add: subset_eq set_eq_iff)+
from compactE_image[OF s this] obtain D where "D ⊆ C" "finite D" "s ⊆ (⋃c∈D. A c)" .
with A show "∃D ⊆ C. finite D ∧ f`s ⊆ ⋃D"
by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
qed
lemma continuous_on_inv:
fixes f :: "'a::topological_space ⇒ 'b::t2_space"
assumes "continuous_on s f"
and "compact s"
and "∀x∈s. g (f x) = x"
shows "continuous_on (f ` s) g"
unfolding continuous_on_topological
proof (clarsimp simp add: assms(3))
fix x :: 'a and B :: "'a set"
assume "x ∈ s" and "open B" and "x ∈ B"
have 1: "∀x∈s. f x ∈ f ` (s - B) ⟷ x ∈ s - B"
using assms(3) by (auto, metis)
have "continuous_on (s - B) f"
using ‹continuous_on s f› Diff_subset
by (rule continuous_on_subset)
moreover have "compact (s - B)"
using ‹open B› and ‹compact s›
unfolding Diff_eq by (intro compact_Int_closed closed_Compl)
ultimately have "compact (f ` (s - B))"
by (rule compact_continuous_image)
then have "closed (f ` (s - B))"
by (rule compact_imp_closed)
then have "open (- f ` (s - B))"
by (rule open_Compl)
moreover have "f x ∈ - f ` (s - B)"
using ‹x ∈ s› and ‹x ∈ B› by (simp add: 1)
moreover have "∀y∈s. f y ∈ - f ` (s - B) ⟶ y ∈ B"
by (simp add: 1)
ultimately show "∃A. open A ∧ f x ∈ A ∧ (∀y∈s. f y ∈ A ⟶ y ∈ B)"
by fast
qed
lemma continuous_on_inv_into:
fixes f :: "'a::topological_space ⇒ 'b::t2_space"
assumes s: "continuous_on s f" "compact s"
and f: "inj_on f s"
shows "continuous_on (f ` s) (the_inv_into s f)"
by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
lemma (in linorder_topology) compact_attains_sup:
assumes "compact S" "S ≠ {}"
shows "∃s∈S. ∀t∈S. t ≤ s"
proof (rule classical)
assume "¬ (∃s∈S. ∀t∈S. t ≤ s)"
then obtain t where t: "∀s∈S. t s ∈ S" and "∀s∈S. s < t s"
by (metis not_le)
then have "⋀s. s∈S ⟹ open {..< t s}" "S ⊆ (⋃s∈S. {..< t s})"
by auto
with ‹compact S› obtain C where "C ⊆ S" "finite C" and C: "S ⊆ (⋃s∈C. {..< t s})"
by (metis compactE_image)
with ‹S ≠ {}› have Max: "Max (t`C) ∈ t`C" and "∀s∈t`C. s ≤ Max (t`C)"
by (auto intro!: Max_in)
with C have "S ⊆ {..< Max (t`C)}"
by (auto intro: less_le_trans simp: subset_eq)
with t Max ‹C ⊆ S› show ?thesis
by fastforce
qed
lemma (in linorder_topology) compact_attains_inf:
assumes "compact S" "S ≠ {}"
shows "∃s∈S. ∀t∈S. s ≤ t"
proof (rule classical)
assume "¬ (∃s∈S. ∀t∈S. s ≤ t)"
then obtain t where t: "∀s∈S. t s ∈ S" and "∀s∈S. t s < s"
by (metis not_le)
then have "⋀s. s∈S ⟹ open {t s <..}" "S ⊆ (⋃s∈S. {t s <..})"
by auto
with ‹compact S› obtain C where "C ⊆ S" "finite C" and C: "S ⊆ (⋃s∈C. {t s <..})"
by (metis compactE_image)
with ‹S ≠ {}› have Min: "Min (t`C) ∈ t`C" and "∀s∈t`C. Min (t`C) ≤ s"
by (auto intro!: Min_in)
with C have "S ⊆ {Min (t`C) <..}"
by (auto intro: le_less_trans simp: subset_eq)
with t Min ‹C ⊆ S› show ?thesis
by fastforce
qed
lemma continuous_attains_sup:
fixes f :: "'a::topological_space ⇒ 'b::linorder_topology"
shows "compact s ⟹ s ≠ {} ⟹ continuous_on s f ⟹ (∃x∈s. ∀y∈s. f y ≤ f x)"
using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
lemma continuous_attains_inf:
fixes f :: "'a::topological_space ⇒ 'b::linorder_topology"
shows "compact s ⟹ s ≠ {} ⟹ continuous_on s f ⟹ (∃x∈s. ∀y∈s. f x ≤ f y)"
using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
subsection ‹Connectedness›
context topological_space
begin
definition "connected S ⟷
¬ (∃A B. open A ∧ open B ∧ S ⊆ A ∪ B ∧ A ∩ B ∩ S = {} ∧ A ∩ S ≠ {} ∧ B ∩ S ≠ {})"
lemma connectedI:
"(⋀A B. open A ⟹ open B ⟹ A ∩ U ≠ {} ⟹ B ∩ U ≠ {} ⟹ A ∩ B ∩ U = {} ⟹ U ⊆ A ∪ B ⟹ False)
⟹ connected U"
by (auto simp: connected_def)
lemma connected_empty [simp]: "connected {}"
by (auto intro!: connectedI)
lemma connected_sing [simp]: "connected {x}"
by (auto intro!: connectedI)
lemma connectedD:
"connected A ⟹ open U ⟹ open V ⟹ U ∩ V ∩ A = {} ⟹ A ⊆ U ∪ V ⟹ U ∩ A = {} ∨ V ∩ A = {}"
by (auto simp: connected_def)
end
lemma connected_closed:
"connected s ⟷
¬ (∃A B. closed A ∧ closed B ∧ s ⊆ A ∪ B ∧ A ∩ B ∩ s = {} ∧ A ∩ s ≠ {} ∧ B ∩ s ≠ {})"
apply (simp add: connected_def del: ex_simps, safe)
apply (drule_tac x="-A" in spec)
apply (drule_tac x="-B" in spec)
apply (fastforce simp add: closed_def [symmetric])
apply (drule_tac x="-A" in spec)
apply (drule_tac x="-B" in spec)
apply (fastforce simp add: open_closed [symmetric])
done
lemma connected_closedD:
"⟦connected s; A ∩ B ∩ s = {}; s ⊆ A ∪ B; closed A; closed B⟧ ⟹ A ∩ s = {} ∨ B ∩ s = {}"
by (simp add: connected_closed)
lemma connected_Union:
assumes cs: "⋀s. s ∈ S ⟹ connected s"
and ne: "⋂S ≠ {}"
shows "connected(⋃S)"
proof (rule connectedI)
fix A B
assume A: "open A" and B: "open B" and Alap: "A ∩ ⋃S ≠ {}" and Blap: "B ∩ ⋃S ≠ {}"
and disj: "A ∩ B ∩ ⋃S = {}" and cover: "⋃S ⊆ A ∪ B"
have disjs:"⋀s. s ∈ S ⟹ A ∩ B ∩ s = {}"
using disj by auto
obtain sa where sa: "sa ∈ S" "A ∩ sa ≠ {}"
using Alap by auto
obtain sb where sb: "sb ∈ S" "B ∩ sb ≠ {}"
using Blap by auto
obtain x where x: "⋀s. s ∈ S ⟹ x ∈ s"
using ne by auto
then have "x ∈ ⋃S"
using ‹sa ∈ S› by blast
then have "x ∈ A ∨ x ∈ B"
using cover by auto
then show False
using cs [unfolded connected_def]
by (metis A B IntI Sup_upper sa sb disjs x cover empty_iff subset_trans)
qed
lemma connected_Un: "connected s ⟹ connected t ⟹ s ∩ t ≠ {} ⟹ connected (s ∪ t)"
using connected_Union [of "{s,t}"] by auto
lemma connected_diff_open_from_closed:
assumes st: "s ⊆ t"
and tu: "t ⊆ u"
and s: "open s"
and t: "closed t"
and u: "connected u"
and ts: "connected (t - s)"
shows "connected(u - s)"
proof (rule connectedI)
fix A B
assume AB: "open A" "open B" "A ∩ (u - s) ≠ {}" "B ∩ (u - s) ≠ {}"
and disj: "A ∩ B ∩ (u - s) = {}"
and cover: "u - s ⊆ A ∪ B"
then consider "A ∩ (t - s) = {}" | "B ∩ (t - s) = {}"
using st ts tu connectedD [of "t-s" "A" "B"] by auto
then show False
proof cases
case 1
then have "(A - t) ∩ (B ∪ s) ∩ u = {}"
using disj st by auto
moreover have "u ⊆ (A - t) ∪ (B ∪ s)"
using 1 cover by auto
ultimately show False
using connectedD [of u "A - t" "B ∪ s"] AB s t 1 u by auto
next
case 2
then have "(A ∪ s) ∩ (B - t) ∩ u = {}"
using disj st by auto
moreover have "u ⊆ (A ∪ s) ∪ (B - t)"
using 2 cover by auto
ultimately show False
using connectedD [of u "A ∪ s" "B - t"] AB s t 2 u by auto
qed
qed
lemma connected_iff_const:
fixes S :: "'a::topological_space set"
shows "connected S ⟷ (∀P::'a ⇒ bool. continuous_on S P ⟶ (∃c. ∀s∈S. P s = c))"
proof safe
fix P :: "'a ⇒ bool"
assume "connected S" "continuous_on S P"
then have "⋀b. ∃A. open A ∧ A ∩ S = P -` {b} ∩ S"
unfolding continuous_on_open_invariant by (simp add: open_discrete)
from this[of True] this[of False]
obtain t f where "open t" "open f" and *: "f ∩ S = P -` {False} ∩ S" "t ∩ S = P -` {True} ∩ S"
by meson
then have "t ∩ S = {} ∨ f ∩ S = {}"
by (intro connectedD[OF ‹connected S›]) auto
then show "∃c. ∀s∈S. P s = c"
proof (rule disjE)
assume "t ∩ S = {}"
then show ?thesis
unfolding * by (intro exI[of _ False]) auto
next
assume "f ∩ S = {}"
then show ?thesis
unfolding * by (intro exI[of _ True]) auto
qed
next
assume P: "∀P::'a ⇒ bool. continuous_on S P ⟶ (∃c. ∀s∈S. P s = c)"
show "connected S"
proof (rule connectedI)
fix A B
assume *: "open A" "open B" "A ∩ S ≠ {}" "B ∩ S ≠ {}" "A ∩ B ∩ S = {}" "S ⊆ A ∪ B"
have "continuous_on S (λx. x ∈ A)"
unfolding continuous_on_open_invariant
proof safe
fix C :: "bool set"
have "C = UNIV ∨ C = {True} ∨ C = {False} ∨ C = {}"
using subset_UNIV[of C] unfolding UNIV_bool by auto
with * show "∃T. open T ∧ T ∩ S = (λx. x ∈ A) -` C ∩ S"
by (intro exI[of _ "(if True ∈ C then A else {}) ∪ (if False ∈ C then B else {})"]) auto
qed
from P[rule_format, OF this] obtain c where "⋀s. s ∈ S ⟹ (s ∈ A) = c"
by blast
with * show False
by (cases c) auto
qed
qed
lemma connectedD_const: "connected S ⟹ continuous_on S P ⟹ ∃c. ∀s∈S. P s = c"
for P :: "'a::topological_space ⇒ bool"
by (auto simp: connected_iff_const)
lemma connectedI_const:
"(⋀P::'a::topological_space ⇒ bool. continuous_on S P ⟹ ∃c. ∀s∈S. P s = c) ⟹ connected S"
by (auto simp: connected_iff_const)
lemma connected_local_const:
assumes "connected A" "a ∈ A" "b ∈ A"
and *: "∀a∈A. eventually (λb. f a = f b) (at a within A)"
shows "f a = f b"
proof -
obtain S where S: "⋀a. a ∈ A ⟹ a ∈ S a" "⋀a. a ∈ A ⟹ open (S a)"
"⋀a x. a ∈ A ⟹ x ∈ S a ⟹ x ∈ A ⟹ f a = f x"
using * unfolding eventually_at_topological by metis
let ?P = "⋃b∈{b∈A. f a = f b}. S b" and ?N = "⋃b∈{b∈A. f a ≠ f b}. S b"
have "?P ∩ A = {} ∨ ?N ∩ A = {}"
using ‹connected A› S ‹a∈A›
by (intro connectedD) (auto, metis)
then show "f a = f b"
proof
assume "?N ∩ A = {}"
then have "∀x∈A. f a = f x"
using S(1) by auto
with ‹b∈A› show ?thesis by auto
next
assume "?P ∩ A = {}" then show ?thesis
using ‹a ∈ A› S(1)[of a] by auto
qed
qed
lemma (in linorder_topology) connectedD_interval:
assumes "connected U"
and xy: "x ∈ U" "y ∈ U"
and "x ≤ z" "z ≤ y"
shows "z ∈ U"
proof -
have eq: "{..<z} ∪ {z<..} = - {z}"
by auto
have "¬ connected U" if "z ∉ U" "x < z" "z < y"
using xy that
apply (simp only: connected_def simp_thms)
apply (rule_tac exI[of _ "{..< z}"])
apply (rule_tac exI[of _ "{z <..}"])
apply (auto simp add: eq)
done
with assms show "z ∈ U"
by (metis less_le)
qed
lemma (in linorder_topology) not_in_connected_cases:
assumes conn: "connected S"
assumes nbdd: "x ∉ S"
assumes ne: "S ≠ {}"
obtains "bdd_above S" "⋀y. y ∈ S ⟹ x ≥ y" | "bdd_below S" "⋀y. y ∈ S ⟹ x ≤ y"
proof -
obtain s where "s ∈ S" using ne by blast
{
assume "s ≤ x"
have "False" if "x ≤ y" "y ∈ S" for y
using connectedD_interval[OF conn ‹s ∈ S› ‹y ∈ S› ‹s ≤ x› ‹x ≤ y›] ‹x ∉ S›
by simp
then have wit: "y ∈ S ⟹ x ≥ y" for y
using le_cases by blast
then have "bdd_above S"
by (rule local.bdd_aboveI)
note this wit
} moreover {
assume "x ≤ s"
have "False" if "x ≥ y" "y ∈ S" for y
using connectedD_interval[OF conn ‹y ∈ S› ‹s ∈ S› ‹x ≥ y› ‹s ≥ x› ] ‹x ∉ S›
by simp
then have wit: "y ∈ S ⟹ x ≤ y" for y
using le_cases by blast
then have "bdd_below S"
by (rule bdd_belowI)
note this wit
} ultimately show ?thesis
by (meson le_cases that)
qed
lemma connected_continuous_image:
assumes *: "continuous_on s f"
and "connected s"
shows "connected (f ` s)"
proof (rule connectedI_const)
fix P :: "'b ⇒ bool"
assume "continuous_on (f ` s) P"
then have "continuous_on s (P ∘ f)"
by (rule continuous_on_compose[OF *])
from connectedD_const[OF ‹connected s› this] show "∃c. ∀s∈f ` s. P s = c"
by auto
qed
lemma connected_Un_UN:
assumes "connected A" "⋀X. X ∈ B ⟹ connected X" "⋀X. X ∈ B ⟹ A ∩ X ≠ {}"
shows "connected (A ∪ ⋃B)"
proof (rule connectedI_const)
fix f :: "'a ⇒ bool"
assume f: "continuous_on (A ∪ ⋃B) f"
have "connected A" "continuous_on A f"
by (auto intro: assms continuous_on_subset[OF f(1)])
from connectedD_const[OF this] obtain c where c: "⋀x. x ∈ A ⟹ f x = c"
by metis
have "f x = c" if "x ∈ X" "X ∈ B" for x X
proof -
have "connected X" "continuous_on X f"
using that by (auto intro: assms continuous_on_subset[OF f])
from connectedD_const[OF this] obtain c' where c': "⋀x. x ∈ X ⟹ f x = c'"
by metis
from assms(3) and that obtain y where "y ∈ A ∩ X"
by auto
with c[of y] c'[of y] c'[of x] that show ?thesis
by auto
qed
with c show "∃c. ∀x∈A ∪ ⋃ B. f x = c"
by (intro exI[of _ c]) auto
qed
section ‹Linear Continuum Topologies›
class linear_continuum_topology = linorder_topology + linear_continuum
begin
lemma Inf_notin_open:
assumes A: "open A"
and bnd: "∀a∈A. x < a"
shows "Inf A ∉ A"
proof
assume "Inf A ∈ A"
then obtain b where "b < Inf A" "{b <.. Inf A} ⊆ A"
using open_left[of A "Inf A" x] assms by auto
with dense[of b "Inf A"] obtain c where "c < Inf A" "c ∈ A"
by (auto simp: subset_eq)
then show False
using cInf_lower[OF ‹c ∈ A›] bnd
by (metis not_le less_imp_le bdd_belowI)
qed
lemma Sup_notin_open:
assumes A: "open A"
and bnd: "∀a∈A. a < x"
shows "Sup A ∉ A"
proof
assume "Sup A ∈ A"
with assms obtain b where "Sup A < b" "{Sup A ..< b} ⊆ A"
using open_right[of A "Sup A" x] by auto
with dense[of "Sup A" b] obtain c where "Sup A < c" "c ∈ A"
by (auto simp: subset_eq)
then show False
using cSup_upper[OF ‹c ∈ A›] bnd
by (metis less_imp_le not_le bdd_aboveI)
qed
end
instance linear_continuum_topology ⊆ perfect_space
proof
fix x :: 'a
obtain y where "x < y ∨ y < x"
using ex_gt_or_lt [of x] ..
with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y] show "¬ open {x}"
by auto
qed
lemma connectedI_interval:
fixes U :: "'a :: linear_continuum_topology set"
assumes *: "⋀x y z. x ∈ U ⟹ y ∈ U ⟹ x ≤ z ⟹ z ≤ y ⟹ z ∈ U"
shows "connected U"
proof (rule connectedI)
{
fix A B
assume "open A" "open B" "A ∩ B ∩ U = {}" "U ⊆ A ∪ B"
fix x y
assume "x < y" "x ∈ A" "y ∈ B" "x ∈ U" "y ∈ U"
let ?z = "Inf (B ∩ {x <..})"
have "x ≤ ?z" "?z ≤ y"
using ‹y ∈ B› ‹x < y› by (auto intro: cInf_lower cInf_greatest)
with ‹x ∈ U› ‹y ∈ U› have "?z ∈ U"
by (rule *)
moreover have "?z ∉ B ∩ {x <..}"
using ‹open B› by (intro Inf_notin_open) auto
ultimately have "?z ∈ A"
using ‹x ≤ ?z› ‹A ∩ B ∩ U = {}› ‹x ∈ A› ‹U ⊆ A ∪ B› by auto
have "∃b∈B. b ∈ A ∧ b ∈ U" if "?z < y"
proof -
obtain a where "?z < a" "{?z ..< a} ⊆ A"
using open_right[OF ‹open A› ‹?z ∈ A› ‹?z < y›] by auto
moreover obtain b where "b ∈ B" "x < b" "b < min a y"
using cInf_less_iff[of "B ∩ {x <..}" "min a y"] ‹?z < a› ‹?z < y› ‹x < y› ‹y ∈ B›
by auto
moreover have "?z ≤ b"
using ‹b ∈ B› ‹x < b›
by (intro cInf_lower) auto
moreover have "b ∈ U"
using ‹x ≤ ?z› ‹?z ≤ b› ‹b < min a y›
by (intro *[OF ‹x ∈ U› ‹y ∈ U›]) (auto simp: less_imp_le)
ultimately show ?thesis
by (intro bexI[of _ b]) auto
qed
then have False
using ‹?z ≤ y› ‹?z ∈ A› ‹y ∈ B› ‹y ∈ U› ‹A ∩ B ∩ U = {}›
unfolding le_less by blast
}
note not_disjoint = this
fix A B assume AB: "open A" "open B" "U ⊆ A ∪ B" "A ∩ B ∩ U = {}"
moreover assume "A ∩ U ≠ {}" then obtain x where x: "x ∈ U" "x ∈ A" by auto
moreover assume "B ∩ U ≠ {}" then obtain y where y: "y ∈ U" "y ∈ B" by auto
moreover note not_disjoint[of B A y x] not_disjoint[of A B x y]
ultimately show False
by (cases x y rule: linorder_cases) auto
qed
lemma connected_iff_interval: "connected U ⟷ (∀x∈U. ∀y∈U. ∀z. x ≤ z ⟶ z ≤ y ⟶ z ∈ U)"
for U :: "'a::linear_continuum_topology set"
by (auto intro: connectedI_interval dest: connectedD_interval)
lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
by (simp add: connected_iff_interval)
lemma connected_Ioi[simp]: "connected {a<..}"
for a :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Ici[simp]: "connected {a..}"
for a :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Iio[simp]: "connected {..<a}"
for a :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Iic[simp]: "connected {..a}"
for a :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Ioo[simp]: "connected {a<..<b}"
for a b :: "'a::linear_continuum_topology"
unfolding connected_iff_interval by auto
lemma connected_Ioc[simp]: "connected {a<..b}"
for a b :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Ico[simp]: "connected {a..<b}"
for a b :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_Icc[simp]: "connected {a..b}"
for a b :: "'a::linear_continuum_topology"
by (auto simp: connected_iff_interval)
lemma connected_contains_Ioo:
fixes A :: "'a :: linorder_topology set"
assumes "connected A" "a ∈ A" "b ∈ A" shows "{a <..< b} ⊆ A"
using connectedD_interval[OF assms] by (simp add: subset_eq Ball_def less_imp_le)
lemma connected_contains_Icc:
fixes A :: "'a::linorder_topology set"
assumes "connected A" "a ∈ A" "b ∈ A"
shows "{a..b} ⊆ A"
proof
fix x assume "x ∈ {a..b}"
then have "x = a ∨ x = b ∨ x ∈ {a<..<b}"
by auto
then show "x ∈ A"
using assms connected_contains_Ioo[of A a b] by auto
qed
subsection ‹Intermediate Value Theorem›
lemma IVT':
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
assumes y: "f a ≤ y" "y ≤ f b" "a ≤ b"
and *: "continuous_on {a .. b} f"
shows "∃x. a ≤ x ∧ x ≤ b ∧ f x = y"
proof -
have "connected {a..b}"
unfolding connected_iff_interval by auto
from connected_continuous_image[OF * this, THEN connectedD_interval, of "f a" "f b" y] y
show ?thesis
by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
qed
lemma IVT2':
fixes f :: "'a :: linear_continuum_topology ⇒ 'b :: linorder_topology"
assumes y: "f b ≤ y" "y ≤ f a" "a ≤ b"
and *: "continuous_on {a .. b} f"
shows "∃x. a ≤ x ∧ x ≤ b ∧ f x = y"
proof -
have "connected {a..b}"
unfolding connected_iff_interval by auto
from connected_continuous_image[OF * this, THEN connectedD_interval, of "f b" "f a" y] y
show ?thesis
by (auto simp add: atLeastAtMost_def atLeast_def atMost_def)
qed
lemma IVT:
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
shows "f a ≤ y ⟹ y ≤ f b ⟹ a ≤ b ⟹ (∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x) ⟹
∃x. a ≤ x ∧ x ≤ b ∧ f x = y"
by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
lemma IVT2:
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
shows "f b ≤ y ⟹ y ≤ f a ⟹ a ≤ b ⟹ (∀x. a ≤ x ∧ x ≤ b ⟶ isCont f x) ⟹
∃x. a ≤ x ∧ x ≤ b ∧ f x = y"
by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
lemma continuous_inj_imp_mono:
fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
assumes x: "a < x" "x < b"
and cont: "continuous_on {a..b} f"
and inj: "inj_on f {a..b}"
shows "(f a < f x ∧ f x < f b) ∨ (f b < f x ∧ f x < f a)"
proof -
note I = inj_on_eq_iff[OF inj]
{
assume "f x < f a" "f x < f b"
then obtain s t where "x ≤ s" "s ≤ b" "a ≤ t" "t ≤ x" "f s = f t" "f x < f s"
using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
by (auto simp: continuous_on_subset[OF cont] less_imp_le)
with x I have False by auto
}
moreover
{
assume "f a < f x" "f b < f x"
then obtain s t where "x ≤ s" "s ≤ b" "a ≤ t" "t ≤ x" "f s = f t" "f s < f x"
using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
by (auto simp: continuous_on_subset[OF cont] less_imp_le)
with x I have False by auto
}
ultimately show ?thesis
using I[of a x] I[of x b] x less_trans[OF x]
by (auto simp add: le_less less_imp_neq neq_iff)
qed
lemma continuous_at_Sup_mono:
fixes f :: "'a::{linorder_topology,conditionally_complete_linorder} ⇒
'b::{linorder_topology,conditionally_complete_linorder}"
assumes "mono f"
and cont: "continuous (at_left (Sup S)) f"
and S: "S ≠ {}" "bdd_above S"
shows "f (Sup S) = (SUP s∈S. f s)"
proof (rule antisym)
have f: "(f ⤏ f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
show "f (Sup S) ≤ (SUP s∈S. f s)"
proof cases
assume "Sup S ∈ S"
then show ?thesis
by (rule cSUP_upper) (auto intro: bdd_above_image_mono S ‹mono f›)
next
assume "Sup S ∉ S"
from ‹S ≠ {}› obtain s where "s ∈ S"
by auto
with ‹Sup S ∉ S› S have "s < Sup S"
unfolding less_le by (blast intro: cSup_upper)
show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
with order_tendstoD(1)[OF f, of "SUP s∈S. f s"] obtain b where "b < Sup S"
and *: "⋀y. b < y ⟹ y < Sup S ⟹ (SUP s∈S. f s) < f y"
by (auto simp: not_le eventually_at_left[OF ‹s < Sup S›])
with ‹S ≠ {}› obtain c where "c ∈ S" "b < c"
using less_cSupD[of S b] by auto
with ‹Sup S ∉ S› S have "c < Sup S"
unfolding less_le by (blast intro: cSup_upper)
from *[OF ‹b < c› ‹c < Sup S›] cSUP_upper[OF ‹c ∈ S› bdd_above_image_mono[of f]]
show False
by (auto simp: assms)
qed
qed
qed (intro cSUP_least ‹mono f›[THEN monoD] cSup_upper S)
lemma continuous_at_Sup_antimono:
fixes f :: "'a::{linorder_topology,conditionally_complete_linorder} ⇒
'b::{linorder_topology,conditionally_complete_linorder}"
assumes "antimono f"
and cont: "continuous (at_left (Sup S)) f"
and S: "S ≠ {}" "bdd_above S"
shows "f (Sup S) = (INF s∈S. f s)"
proof (rule antisym)
have f: "(f ⤏ f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
show "(INF s∈S. f s) ≤ f (Sup S)"
proof cases
assume "Sup S ∈ S"
then show ?thesis
by (intro cINF_lower) (auto intro: bdd_below_image_antimono S ‹antimono f›)
next
assume "Sup S ∉ S"
from ‹S ≠ {}› obtain s where "s ∈ S"
by auto
with ‹Sup S ∉ S› S have "s < Sup S"
unfolding less_le by (blast intro: cSup_upper)
show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
with order_tendstoD(2)[OF f, of "INF s∈S. f s"] obtain b where "b < Sup S"
and *: "⋀y. b < y ⟹ y < Sup S ⟹ f y < (INF s∈S. f s)"
by (auto simp: not_le eventually_at_left[OF ‹s < Sup S›])
with ‹S ≠ {}› obtain c where "c ∈ S" "b < c"
using less_cSupD[of S b] by auto
with ‹Sup S ∉ S› S have "c < Sup S"
unfolding less_le by (blast intro: cSup_upper)
from *[OF ‹b < c› ‹c < Sup S›] cINF_lower[OF bdd_below_image_antimono, of f S c] ‹c ∈ S›
show False
by (auto simp: assms)
qed
qed
qed (intro cINF_greatest ‹antimono f›[THEN antimonoD] cSup_upper S)
lemma continuous_at_Inf_mono:
fixes f :: "'a::{linorder_topology,conditionally_complete_linorder} ⇒
'b::{linorder_topology,conditionally_complete_linorder}"
assumes "mono f"
and cont: "continuous (at_right (Inf S)) f"
and S: "S ≠ {}" "bdd_below S"
shows "f (Inf S) = (INF s∈S. f s)"
proof (rule antisym)
have f: "(f ⤏ f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
show "(INF s∈S. f s) ≤ f (Inf S)"
proof cases
assume "Inf S ∈ S"
then show ?thesis
by (rule cINF_lower[rotated]) (auto intro: bdd_below_image_mono S ‹mono f›)
next
assume "Inf S ∉ S"
from ‹S ≠ {}› obtain s where "s ∈ S"
by auto
with ‹Inf S ∉ S› S have "Inf S < s"
unfolding less_le by (blast intro: cInf_lower)
show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
with order_tendstoD(2)[OF f, of "INF s∈S. f s"] obtain b where "Inf S < b"
and *: "⋀y. Inf S < y ⟹ y < b ⟹ f y < (INF s∈S. f s)"
by (auto simp: not_le eventually_at_right[OF ‹Inf S < s›])
with ‹S ≠ {}› obtain c where "c ∈ S" "c < b"
using cInf_lessD[of S b] by auto
with ‹Inf S ∉ S› S have "Inf S < c"
unfolding less_le by (blast intro: cInf_lower)
from *[OF ‹Inf S < c› ‹c < b›] cINF_lower[OF bdd_below_image_mono[of f] ‹c ∈ S›]
show False
by (auto simp: assms)
qed
qed
qed (intro cINF_greatest ‹mono f›[THEN monoD] cInf_lower ‹bdd_below S› ‹S ≠ {}›)
lemma continuous_at_Inf_antimono:
fixes f :: "'a::{linorder_topology,conditionally_complete_linorder} ⇒
'b::{linorder_topology,conditionally_complete_linorder}"
assumes "antimono f"
and cont: "continuous (at_right (Inf S)) f"
and S: "S ≠ {}" "bdd_below S"
shows "f (Inf S) = (SUP s∈S. f s)"
proof (rule antisym)
have f: "(f ⤏ f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
show "f (Inf S) ≤ (SUP s∈S. f s)"
proof cases
assume "Inf S ∈ S"
then show ?thesis
by (rule cSUP_upper) (auto intro: bdd_above_image_antimono S ‹antimono f›)
next
assume "Inf S ∉ S"
from ‹S ≠ {}› obtain s where "s ∈ S"
by auto
with ‹Inf S ∉ S› S have "Inf S < s"
unfolding less_le by (blast intro: cInf_lower)
show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
with order_tendstoD(1)[OF f, of "SUP s∈S. f s"] obtain b where "Inf S < b"
and *: "⋀y. Inf S < y ⟹ y < b ⟹ (SUP s∈S. f s) < f y"
by (auto simp: not_le eventually_at_right[OF ‹Inf S < s›])
with ‹S ≠ {}› obtain c where "c ∈ S" "c < b"
using cInf_lessD[of S b] by auto
with ‹Inf S ∉ S› S have "Inf S < c"
unfolding less_le by (blast intro: cInf_lower)
from *[OF ‹Inf S < c› ‹c < b›] cSUP_upper[OF ‹c ∈ S› bdd_above_image_antimono[of f]]
show False
by (auto simp: assms)
qed
qed
qed (intro cSUP_least ‹antimono f›[THEN antimonoD] cInf_lower S)
subsection ‹Uniform spaces›
class uniformity =
fixes uniformity :: "('a × 'a) filter"
begin
abbreviation uniformity_on :: "'a set ⇒ ('a × 'a) filter"
where "uniformity_on s ≡ inf uniformity (principal (s×s))"
end
lemma uniformity_Abort:
"uniformity =
Filter.abstract_filter (λu. Code.abort (STR ''uniformity is not executable'') (λu. uniformity))"
by simp
class open_uniformity = "open" + uniformity +
assumes open_uniformity:
"⋀U. open U ⟷ (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"
begin
subclass topological_space
by standard (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
end
class uniform_space = open_uniformity +
assumes uniformity_refl: "eventually E uniformity ⟹ E (x, x)"
and uniformity_sym: "eventually E uniformity ⟹ eventually (λ(x, y). E (y, x)) uniformity"
and uniformity_trans:
"eventually E uniformity ⟹
∃D. eventually D uniformity ∧ (∀x y z. D (x, y) ⟶ D (y, z) ⟶ E (x, z))"
begin
lemma uniformity_bot: "uniformity ≠ bot"
using uniformity_refl by auto
lemma uniformity_trans':
"eventually E uniformity ⟹
eventually (λ((x, y), (y', z)). y = y' ⟶ E (x, z)) (uniformity ×⇩F uniformity)"
by (drule uniformity_trans) (auto simp add: eventually_prod_same)
lemma uniformity_transE:
assumes "eventually E uniformity"
obtains D where "eventually D uniformity" "⋀x y z. D (x, y) ⟹ D (y, z) ⟹ E (x, z)"
using uniformity_trans [OF assms] by auto
lemma eventually_nhds_uniformity:
"eventually P (nhds x) ⟷ eventually (λ(x', y). x' = x ⟶ P y) uniformity"
(is "_ ⟷ ?N P x")
unfolding eventually_nhds
proof safe
assume *: "?N P x"
have "?N (?N P) x" if "?N P x" for x
proof -
from that obtain D where ev: "eventually D uniformity"
and D: "D (a, b) ⟹ D (b, c) ⟹ case (a, c) of (x', y) ⇒ x' = x ⟶ P y" for a b c
by (rule uniformity_transE) simp
from ev show ?thesis
by eventually_elim (insert ev D, force elim: eventually_mono split: prod.split)
qed
then have "open {x. ?N P x}"
by (simp add: open_uniformity)
then show "∃S. open S ∧ x ∈ S ∧ (∀x∈S. P x)"
by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
qed (force simp add: open_uniformity elim: eventually_mono)
subsubsection ‹Totally bounded sets›
definition totally_bounded :: "'a set ⇒ bool"
where "totally_bounded S ⟷
(∀E. eventually E uniformity ⟶ (∃X. finite X ∧ (∀s∈S. ∃x∈X. E (x, s))))"
lemma totally_bounded_empty[iff]: "totally_bounded {}"
by (auto simp add: totally_bounded_def)
lemma totally_bounded_subset: "totally_bounded S ⟹ T ⊆ S ⟹ totally_bounded T"
by (fastforce simp add: totally_bounded_def)
lemma totally_bounded_Union[intro]:
assumes M: "finite M" "⋀S. S ∈ M ⟹ totally_bounded S"
shows "totally_bounded (⋃M)"
unfolding totally_bounded_def
proof safe
fix E
assume "eventually E uniformity"
with M obtain X where "∀S∈M. finite (X S) ∧ (∀s∈S. ∃x∈X S. E (x, s))"
by (metis totally_bounded_def)
with ‹finite M› show "∃X. finite X ∧ (∀s∈⋃M. ∃x∈X. E (x, s))"
by (intro exI[of _ "⋃S∈M. X S"]) force
qed
subsubsection ‹Cauchy filter›
definition cauchy_filter :: "'a filter ⇒ bool"
where "cauchy_filter F ⟷ F ×⇩F F ≤ uniformity"
definition Cauchy :: "(nat ⇒ 'a) ⇒ bool"
where Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
lemma Cauchy_uniform_iff:
"Cauchy X ⟷ (∀P. eventually P uniformity ⟶ (∃N. ∀n≥N. ∀m≥N. P (X n, X m)))"
unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
eventually_filtermap eventually_sequentially
proof safe
let ?U = "λP. eventually P uniformity"
{
fix P
assume "?U P" "∀P. ?U P ⟶ (∃Q. (∃N. ∀n≥N. Q (X n)) ∧ (∀x y. Q x ⟶ Q y ⟶ P (x, y)))"
then obtain Q N where "⋀n. n ≥ N ⟹ Q (X n)" "⋀x y. Q x ⟹ Q y ⟹ P (x, y)"
by metis
then show "∃N. ∀n≥N. ∀m≥N. P (X n, X m)"
by blast
next
fix P
assume "?U P" and P: "∀P. ?U P ⟶ (∃N. ∀n≥N. ∀m≥N. P (X n, X m))"
then obtain Q where "?U Q" and Q: "⋀x y z. Q (x, y) ⟹ Q (y, z) ⟹ P (x, z)"
by (auto elim: uniformity_transE)
then have "?U (λx. Q x ∧ (λ(x, y). Q (y, x)) x)"
unfolding eventually_conj_iff by (simp add: uniformity_sym)
from P[rule_format, OF this]
obtain N where N: "⋀n m. n ≥ N ⟹ m ≥ N ⟹ Q (X n, X m) ∧ Q (X m, X n)"
by auto
show "∃Q. (∃N. ∀n≥N. Q (X n)) ∧ (∀x y. Q x ⟶ Q y ⟶ P (x, y))"
proof (safe intro!: exI[of _ "λx. ∀n≥N. Q (x, X n) ∧ Q (X n, x)"] exI[of _ N] N)
fix x y
assume "∀n≥N. Q (x, X n) ∧ Q (X n, x)" "∀n≥N. Q (y, X n) ∧ Q (X n, y)"
then have "Q (x, X N)" "Q (X N, y)" by auto
then show "P (x, y)"
by (rule Q)
qed
}
qed
lemma nhds_imp_cauchy_filter:
assumes *: "F ≤ nhds x"
shows "cauchy_filter F"
proof -
have "F ×⇩F F ≤ nhds x ×⇩F nhds x"
by (intro prod_filter_mono *)
also have "… ≤ uniformity"
unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
proof safe
fix P
assume "eventually P uniformity"
then obtain Ql where ev: "eventually Ql uniformity"
and "Ql (x, y) ⟹ Ql (y, z) ⟹ P (x, z)" for x y z
by (rule uniformity_transE) simp
with ev[THEN uniformity_sym]
show "∃Q. eventually (λ(x', y). x' = x ⟶ Q y) uniformity ∧
(∀x y. Q x ⟶ Q y ⟶ P (x, y))"
by (rule_tac exI[of _ "λy. Ql (y, x) ∧ Ql (x, y)"]) (fastforce elim: eventually_elim2)
qed
finally show ?thesis
by (simp add: cauchy_filter_def)
qed
lemma LIMSEQ_imp_Cauchy: "X ⇢ x ⟹ Cauchy X"
unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
lemma Cauchy_subseq_Cauchy:
assumes "Cauchy X" "strict_mono f"
shows "Cauchy (X ∘ f)"
unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
by (rule order_trans[OF _ ‹Cauchy X›[unfolded Cauchy_uniform cauchy_filter_def]])
(intro prod_filter_mono filtermap_mono filterlim_subseq[OF ‹strict_mono f›, unfolded filterlim_def])
lemma convergent_Cauchy: "convergent X ⟹ Cauchy X"
unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
definition complete :: "'a set ⇒ bool"
where complete_uniform: "complete S ⟷
(∀F ≤ principal S. F ≠ bot ⟶ cauchy_filter F ⟶ (∃x∈S. F ≤ nhds x))"
lemma (in uniform_space) cauchy_filter_complete_converges:
assumes "cauchy_filter F" "complete A" "F ≤ principal A" "F ≠ bot"
shows "∃c. F ≤ nhds c"
using assms unfolding complete_uniform by blast
end
subsubsection ‹Uniformly continuous functions›
definition uniformly_continuous_on :: "'a set ⇒ ('a::uniform_space ⇒ 'b::uniform_space) ⇒ bool"
where uniformly_continuous_on_uniformity: "uniformly_continuous_on s f ⟷
(LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
lemma uniformly_continuous_onD:
"uniformly_continuous_on s f ⟹ eventually E uniformity ⟹
eventually (λ(x, y). x ∈ s ⟶ y ∈ s ⟶ E (f x, f y)) uniformity"
by (simp add: uniformly_continuous_on_uniformity filterlim_iff
eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (λx. c)"
by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (λx. x)"
by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
lemma uniformly_continuous_on_compose:
"uniformly_continuous_on s g ⟹ uniformly_continuous_on (g`s) f ⟹
uniformly_continuous_on s (λx. f (g x))"
using filterlim_compose[of "λ(x, y). (f x, f y)" uniformity
"uniformity_on (g`s)" "λ(x, y). (g x, g y)" "uniformity_on s"]
by (simp add: split_beta' uniformly_continuous_on_uniformity
filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
lemma uniformly_continuous_imp_continuous:
assumes f: "uniformly_continuous_on s f"
shows "continuous_on s f"
by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
section ‹Product Topology›
subsection ‹Product is a topological space›
instantiation prod :: (topological_space, topological_space) topological_space
begin
definition open_prod_def[code del]:
"open (S :: ('a × 'b) set) ⟷
(∀x∈S. ∃A B. open A ∧ open B ∧ x ∈ A × B ∧ A × B ⊆ S)"
lemma open_prod_elim:
assumes "open S" and "x ∈ S"
obtains A B where "open A" and "open B" and "x ∈ A × B" and "A × B ⊆ S"
using assms unfolding open_prod_def by fast
lemma open_prod_intro:
assumes "⋀x. x ∈ S ⟹ ∃A B. open A ∧ open B ∧ x ∈ A × B ∧ A × B ⊆ S"
shows "open S"
using assms unfolding open_prod_def by fast
instance
proof
show "open (UNIV :: ('a × 'b) set)"
unfolding open_prod_def by auto
next
fix S T :: "('a × 'b) set"
assume "open S" "open T"
show "open (S ∩ T)"
proof (rule open_prod_intro)
fix x
assume x: "x ∈ S ∩ T"
from x have "x ∈ S" by simp
obtain Sa Sb where A: "open Sa" "open Sb" "x ∈ Sa × Sb" "Sa × Sb ⊆ S"
using ‹open S› and ‹x ∈ S› by (rule open_prod_elim)
from x have "x ∈ T" by simp
obtain Ta Tb where B: "open Ta" "open Tb" "x ∈ Ta × Tb" "Ta × Tb ⊆ T"
using ‹open T› and ‹x ∈ T› by (rule open_prod_elim)
let ?A = "Sa ∩ Ta" and ?B = "Sb ∩ Tb"
have "open ?A ∧ open ?B ∧ x ∈ ?A × ?B ∧ ?A × ?B ⊆ S ∩ T"
using A B by (auto simp add: open_Int)
then show "∃A B. open A ∧ open B ∧ x ∈ A × B ∧ A × B ⊆ S ∩ T"
by fast
qed
next
fix K :: "('a × 'b) set set"
assume "∀S∈K. open S"
then show "open (⋃K)"
unfolding open_prod_def by fast
qed
end
declare [[code abort: "open :: ('a::topological_space × 'b::topological_space) set ⇒ bool"]]
lemma open_Times: "open S ⟹ open T ⟹ open (S × T)"
unfolding open_prod_def by auto
lemma fst_vimage_eq_Times: "fst -` S = S × UNIV"
by auto
lemma snd_vimage_eq_Times: "snd -` S = UNIV × S"
by auto
lemma open_vimage_fst: "open S ⟹ open (fst -` S)"
by (simp add: fst_vimage_eq_Times open_Times)
lemma open_vimage_snd: "open S ⟹ open (snd -` S)"
by (simp add: snd_vimage_eq_Times open_Times)
lemma closed_vimage_fst: "closed S ⟹ closed (fst -` S)"
unfolding closed_open vimage_Compl [symmetric]
by (rule open_vimage_fst)
lemma closed_vimage_snd: "closed S ⟹ closed (snd -` S)"
unfolding closed_open vimage_Compl [symmetric]
by (rule open_vimage_snd)
lemma closed_Times: "closed S ⟹ closed T ⟹ closed (S × T)"
proof -
have "S × T = (fst -` S) ∩ (snd -` T)"
by auto
then show "closed S ⟹ closed T ⟹ closed (S × T)"
by (simp add: closed_vimage_fst closed_vimage_snd closed_Int)
qed
lemma subset_fst_imageI: "A × B ⊆ S ⟹ y ∈ B ⟹ A ⊆ fst ` S"
unfolding image_def subset_eq by force
lemma subset_snd_imageI: "A × B ⊆ S ⟹ x ∈ A ⟹ B ⊆ snd ` S"
unfolding image_def subset_eq by force
lemma open_image_fst:
assumes "open S"
shows "open (fst ` S)"
proof (rule openI)
fix x
assume "x ∈ fst ` S"
then obtain y where "(x, y) ∈ S"
by auto
then obtain A B where "open A" "open B" "x ∈ A" "y ∈ B" "A × B ⊆ S"
using ‹open S› unfolding open_prod_def by auto
from ‹A × B ⊆ S› ‹y ∈ B› have "A ⊆ fst ` S"
by (rule subset_fst_imageI)
with ‹open A› ‹x ∈ A› have "open A ∧ x ∈ A ∧ A ⊆ fst ` S"
by simp
then show "∃T. open T ∧ x ∈ T ∧ T ⊆ fst ` S" ..
qed
lemma open_image_snd:
assumes "open S"
shows "open (snd ` S)"
proof (rule openI)
fix y
assume "y ∈ snd ` S"
then obtain x where "(x, y) ∈ S"
by auto
then obtain A B where "open A" "open B" "x ∈ A" "y ∈ B" "A × B ⊆ S"
using ‹open S› unfolding open_prod_def by auto
from ‹A × B ⊆ S› ‹x ∈ A› have "B ⊆ snd ` S"
by (rule subset_snd_imageI)
with ‹open B› ‹y ∈ B› have "open B ∧ y ∈ B ∧ B ⊆ snd ` S"
by simp
then show "∃T. open T ∧ y ∈ T ∧ T ⊆ snd ` S" ..
qed
lemma nhds_prod: "nhds (a, b) = nhds a ×⇩F nhds b"
unfolding nhds_def
proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
fix S T
assume "open S" "a ∈ S" "open T" "b ∈ T"
then show "(INF x ∈ {S. open S ∧ (a, b) ∈ S}. principal x) ≤ principal (S × T)"
by (intro INF_lower) (auto intro!: open_Times)
next
fix S'
assume "open S'" "(a, b) ∈ S'"
then obtain S T where "open S" "a ∈ S" "open T" "b ∈ T" "S × T ⊆ S'"
by (auto elim: open_prod_elim)
then show "(INF x ∈ {S. open S ∧ a ∈ S}. INF y ∈ {S. open S ∧ b ∈ S}.
principal (x × y)) ≤ principal S'"
by (auto intro!: INF_lower2)
qed
subsubsection ‹Continuity of operations›
lemma tendsto_fst [tendsto_intros]:
assumes "(f ⤏ a) F"
shows "((λx. fst (f x)) ⤏ fst a) F"
proof (rule topological_tendstoI)
fix S
assume "open S" and "fst a ∈ S"
then have "open (fst -` S)" and "a ∈ fst -` S"
by (simp_all add: open_vimage_fst)
with assms have "eventually (λx. f x ∈ fst -` S) F"
by (rule topological_tendstoD)
then show "eventually (λx. fst (f x) ∈ S) F"
by simp
qed
lemma tendsto_snd [tendsto_intros]:
assumes "(f ⤏ a) F"
shows "((λx. snd (f x)) ⤏ snd a) F"
proof (rule topological_tendstoI)
fix S
assume "open S" and "snd a ∈ S"
then have "open (snd -` S)" and "a ∈ snd -` S"
by (simp_all add: open_vimage_snd)
with assms have "eventually (λx. f x ∈ snd -` S) F"
by (rule topological_tendstoD)
then show "eventually (λx. snd (f x) ∈ S) F"
by simp
qed
lemma tendsto_Pair [tendsto_intros]:
assumes "(f ⤏ a) F" and "(g ⤏ b) F"
shows "((λx. (f x, g x)) ⤏ (a, b)) F"
unfolding nhds_prod using assms by (rule filterlim_Pair)
lemma continuous_fst[continuous_intros]: "continuous F f ⟹ continuous F (λx. fst (f x))"
unfolding continuous_def by (rule tendsto_fst)
lemma continuous_snd[continuous_intros]: "continuous F f ⟹ continuous F (λx. snd (f x))"
unfolding continuous_def by (rule tendsto_snd)
lemma continuous_Pair[continuous_intros]:
"continuous F f ⟹ continuous F g ⟹ continuous F (λx. (f x, g x))"
unfolding continuous_def by (rule tendsto_Pair)
lemma continuous_on_fst[continuous_intros]:
"continuous_on s f ⟹ continuous_on s (λx. fst (f x))"
unfolding continuous_on_def by (auto intro: tendsto_fst)
lemma continuous_on_snd[continuous_intros]:
"continuous_on s f ⟹ continuous_on s (λx. snd (f x))"
unfolding continuous_on_def by (auto intro: tendsto_snd)
lemma continuous_on_Pair[continuous_intros]:
"continuous_on s f ⟹ continuous_on s g ⟹ continuous_on s (λx. (f x, g x))"
unfolding continuous_on_def by (auto intro: tendsto_Pair)
lemma continuous_on_swap[continuous_intros]: "continuous_on A prod.swap"
by (simp add: prod.swap_def continuous_on_fst continuous_on_snd
continuous_on_Pair continuous_on_id)
lemma continuous_on_swap_args:
assumes "continuous_on (A×B) (λ(x,y). d x y)"
shows "continuous_on (B×A) (λ(x,y). d y x)"
proof -
have "(λ(x,y). d y x) = (λ(x,y). d x y) ∘ prod.swap"
by force
then show ?thesis
by (metis assms continuous_on_compose continuous_on_swap product_swap)
qed
lemma isCont_fst [simp]: "isCont f a ⟹ isCont (λx. fst (f x)) a"
by (fact continuous_fst)
lemma isCont_snd [simp]: "isCont f a ⟹ isCont (λx. snd (f x)) a"
by (fact continuous_snd)
lemma isCont_Pair [simp]: "⟦isCont f a; isCont g a⟧ ⟹ isCont (λx. (f x, g x)) a"
by (fact continuous_Pair)
lemma continuous_on_compose_Pair:
assumes f: "continuous_on (Sigma A B) (λ(a, b). f a b)"
assumes g: "continuous_on C g"
assumes h: "continuous_on C h"
assumes subset: "⋀c. c ∈ C ⟹ g c ∈ A" "⋀c. c ∈ C ⟹ h c ∈ B (g c)"
shows "continuous_on C (λc. f (g c) (h c))"
using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
by auto
subsubsection ‹Connectedness of products›
proposition connected_Times:
assumes S: "connected S" and T: "connected T"
shows "connected (S × T)"
proof (rule connectedI_const)
fix P::"'a × 'b ⇒ bool"
assume P[THEN continuous_on_compose2, continuous_intros]: "continuous_on (S × T) P"
have "continuous_on S (λs. P (s, t))" if "t ∈ T" for t
by (auto intro!: continuous_intros that)
from connectedD_const[OF S this]
obtain c1 where c1: "⋀s t. t ∈ T ⟹ s ∈ S ⟹ P (s, t) = c1 t"
by metis
moreover
have "continuous_on T (λt. P (s, t))" if "s ∈ S" for s
by (auto intro!: continuous_intros that)
from connectedD_const[OF T this]
obtain c2 where "⋀s t. t ∈ T ⟹ s ∈ S ⟹ P (s, t) = c2 s"
by metis
ultimately show "∃c. ∀s∈S × T. P s = c"
by auto
qed
corollary connected_Times_eq [simp]:
"connected (S × T) ⟷ S = {} ∨ T = {} ∨ connected S ∧ connected T" (is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof cases
assume "S ≠ {} ∧ T ≠ {}"
moreover
have "connected (fst ` (S × T))" "connected (snd ` (S × T))"
using continuous_on_fst continuous_on_snd continuous_on_id
by (blast intro: connected_continuous_image [OF _ L])+
ultimately show ?thesis
by auto
qed auto
qed (auto simp: connected_Times)
subsubsection ‹Separation axioms›
instance prod :: (t0_space, t0_space) t0_space
proof
fix x y :: "'a × 'b"
assume "x ≠ y"
then have "fst x ≠ fst y ∨ snd x ≠ snd y"
by (simp add: prod_eq_iff)
then show "∃U. open U ∧ (x ∈ U) ≠ (y ∈ U)"
by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t1_space, t1_space) t1_space
proof
fix x y :: "'a × 'b"
assume "x ≠ y"
then have "fst x ≠ fst y ∨ snd x ≠ snd y"
by (simp add: prod_eq_iff)
then show "∃U. open U ∧ x ∈ U ∧ y ∉ U"
by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd)
qed
instance prod :: (t2_space, t2_space) t2_space
proof
fix x y :: "'a × 'b"
assume "x ≠ y"
then have "fst x ≠ fst y ∨ snd x ≠ snd y"
by (simp add: prod_eq_iff)
then show "∃U V. open U ∧ open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}"
by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd)
qed
lemma isCont_swap[continuous_intros]: "isCont prod.swap a"
using continuous_on_eq_continuous_within continuous_on_swap by blast
lemma open_diagonal_complement:
"open {(x,y) |x y. x ≠ (y::('a::t2_space))}"
proof -
have "open {(x, y). x ≠ (y::'a)}"
unfolding split_def by (intro open_Collect_neq continuous_intros)
also have "{(x, y). x ≠ (y::'a)} = {(x, y) |x y. x ≠ (y::'a)}"
by auto
finally show ?thesis .
qed
lemma closed_diagonal:
"closed {y. ∃ x::('a::t2_space). y = (x,x)}"
proof -
have "{y. ∃ x::'a. y = (x,x)} = UNIV - {(x,y) | x y. x ≠ y}" by auto
then show ?thesis using open_diagonal_complement closed_Diff by auto
qed
lemma open_superdiagonal:
"open {(x,y) | x y. x > (y::'a::{linorder_topology})}"
proof -
have "open {(x, y). x > (y::'a)}"
unfolding split_def by (intro open_Collect_less continuous_intros)
also have "{(x, y). x > (y::'a)} = {(x, y) |x y. x > (y::'a)}"
by auto
finally show ?thesis .
qed
lemma closed_subdiagonal:
"closed {(x,y) | x y. x ≤ (y::'a::{linorder_topology})}"
proof -
have "{(x,y) | x y. x ≤ (y::'a)} = UNIV - {(x,y) | x y. x > (y::'a)}" by auto
then show ?thesis using open_superdiagonal closed_Diff by auto
qed
lemma open_subdiagonal:
"open {(x,y) | x y. x < (y::'a::{linorder_topology})}"
proof -
have "open {(x, y). x < (y::'a)}"
unfolding split_def by (intro open_Collect_less continuous_intros)
also have "{(x, y). x < (y::'a)} = {(x, y) |x y. x < (y::'a)}"
by auto
finally show ?thesis .
qed
lemma closed_superdiagonal:
"closed {(x,y) | x y. x ≥ (y::('a::{linorder_topology}))}"
proof -
have "{(x,y) | x y. x ≥ (y::'a)} = UNIV - {(x,y) | x y. x < y}" by auto
then show ?thesis using open_subdiagonal closed_Diff by auto
qed
end