author  huffman 
Thu, 04 Jun 2009 17:24:09 0700  
changeset 31447  97bab1ac463e 
parent 31445  c8a474a919a7 
child 31448  29090e3111bd 
permissions  rwrr 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1 
(* Title: Topology 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
30267  3 
Author: Robert Himmelmann, TU Muenchen 
4 
*) 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

5 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

6 
header {* Elementary topology in Euclidean space. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

7 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

8 
theory Topology_Euclidean_Space 
30654  9 
imports SEQ Euclidean_Space 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

10 
begin 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

11 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

12 
declare fstcart_pastecart[simp] sndcart_pastecart[simp] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

13 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

14 
subsection{* General notion of a topology *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

15 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

16 
definition "istopology L \<longleftrightarrow> {} \<in> L \<and> (\<forall>S \<in>L. \<forall>T \<in>L. S \<inter> T \<in> L) \<and> (\<forall>K. K \<subseteq>L \<longrightarrow> \<Union> K \<in> L)" 
30488  17 
typedef (open) 'a topology = "{L::('a set) set. istopology L}" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

18 
morphisms "openin" "topology" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

19 
unfolding istopology_def by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

20 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

21 
lemma istopology_open_in[intro]: "istopology(openin U)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

22 
using openin[of U] by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

23 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

24 
lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

25 
using topology_inverse[unfolded mem_def Collect_def] . 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

26 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

27 
lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

28 
using topology_inverse[of U] istopology_open_in[of "topology U"] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

29 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

30 
lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

31 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

32 
{assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

33 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

34 
{assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

35 
hence "openin T1 = openin T2" by (metis mem_def set_ext) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

36 
hence "topology (openin T1) = topology (openin T2)" by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

37 
hence "T1 = T2" unfolding openin_inverse .} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

38 
ultimately show ?thesis by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

39 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

40 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

41 
text{* Infer the "universe" from union of all sets in the topology. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

42 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

43 
definition "topspace T = \<Union>{S. openin T S}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

44 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

45 
subsection{* Main properties of open sets *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

46 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

47 
lemma openin_clauses: 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

48 
fixes U :: "'a topology" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

49 
shows "openin U {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

50 
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

51 
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

52 
using openin[of U] unfolding istopology_def Collect_def mem_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

53 
by (metis mem_def subset_eq)+ 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

54 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

55 
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

56 
unfolding topspace_def by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

57 
lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

58 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

59 
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

60 
by (simp add: openin_clauses) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

61 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

62 
lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" by (simp add: openin_clauses) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

63 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

64 
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

65 
using openin_Union[of "{S,T}" U] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

66 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

67 
lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

68 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

69 
lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)" (is "?lhs \<longleftrightarrow> ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

70 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

71 
{assume ?lhs then have ?rhs by auto } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

72 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

73 
{assume H: ?rhs 
30488  74 
then obtain t where t: "\<forall>x\<in>S. openin U (t x) \<and> x \<in> t x \<and> t x \<subseteq> S" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

75 
unfolding Ball_def ex_simps(6)[symmetric] choice_iff by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

76 
from t have th0: "\<forall>x\<in> t`S. openin U x" by auto 
30488  77 
have "\<Union> t`S = S" using t by auto 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

78 
with openin_Union[OF th0] have "openin U S" by simp } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

79 
ultimately show ?thesis by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

80 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

81 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

82 
subsection{* Closed sets *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

83 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

84 
definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

85 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

86 
lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

87 
lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) 
30488  88 
lemma closedin_topspace[intro,simp]: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

89 
"closedin U (topspace U)" by (simp add: closedin_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

90 
lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

91 
by (auto simp add: Diff_Un closedin_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

92 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

93 
lemma Diff_Inter[intro]: "A  \<Inter>S = \<Union> {A  ss. s\<in>S}" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

94 
lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

95 
shows "closedin U (\<Inter> K)" using Ke Kc unfolding closedin_def Diff_Inter by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

96 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

97 
lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

98 
using closedin_Inter[of "{S,T}" U] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

99 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

100 
lemma Diff_Diff_Int: "A  (A  B) = A \<inter> B" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

101 
lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

102 
apply (auto simp add: closedin_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

103 
apply (metis openin_subset subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

104 
apply (auto simp add: Diff_Diff_Int) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

105 
apply (subgoal_tac "topspace U \<inter> S = S") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

106 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

107 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

108 
lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U  S))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

109 
by (simp add: openin_closedin_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

110 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

111 
lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S  T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

112 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

113 
have "S  T = S \<inter> (topspace U  T)" using openin_subset[of U S] oS cT 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

114 
by (auto simp add: topspace_def openin_subset) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

115 
then show ?thesis using oS cT by (auto simp add: closedin_def) 
30488  116 
qed 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

117 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

118 
lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S  T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

119 
proof 
30488  120 
have "S  T = S \<inter> (topspace U  T)" using closedin_subset[of U S] oS cT 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

121 
by (auto simp add: topspace_def ) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

122 
then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

123 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

124 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

125 
subsection{* Subspace topology. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

126 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

127 
definition "subtopology U V = topology {S \<inter> V S. openin U S}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

128 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

129 
lemma istopology_subtopology: "istopology {S \<inter> V S. openin U S}" (is "istopology ?L") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

130 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

131 
have "{} \<in> ?L" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

132 
{fix A B assume A: "A \<in> ?L" and B: "B \<in> ?L" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

133 
from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

134 
have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)" using Sa Sb by blast+ 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

135 
then have "A \<inter> B \<in> ?L" by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

136 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

137 
{fix K assume K: "K \<subseteq> ?L" 
30488  138 
have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U " 
139 
apply (rule set_ext) 

140 
apply (simp add: Ball_def image_iff) 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

141 
by (metis mem_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

142 
from K[unfolded th0 subset_image_iff] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

143 
obtain Sk where Sk: "Sk \<subseteq> openin U" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

144 
have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

145 
moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq mem_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

146 
ultimately have "\<Union>K \<in> ?L" by blast} 
30488  147 
ultimately show ?thesis unfolding istopology_def by blast 
148 
qed 

149 

150 
lemma openin_subtopology: 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

151 
"openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))" 
30488  152 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 
153 
by (auto simp add: Collect_def) 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

154 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

155 
lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

156 
by (auto simp add: topspace_def openin_subtopology) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

157 

30488  158 
lemma closedin_subtopology: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

159 
"closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

160 
unfolding closedin_def topspace_subtopology 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

161 
apply (simp add: openin_subtopology) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

162 
apply (rule iffI) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

163 
apply clarify 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

164 
apply (rule_tac x="topspace U  T" in exI) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

165 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

166 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

167 
lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

168 
unfolding openin_subtopology 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

169 
apply (rule iffI, clarify) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

170 
apply (frule openin_subset[of U]) apply blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

171 
apply (rule exI[where x="topspace U"]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

172 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

173 

30488  174 
lemma subtopology_superset: assumes UV: "topspace U \<subseteq> V" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

175 
shows "subtopology U V = U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

176 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

177 
{fix S 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

178 
{fix T assume T: "openin U T" "S = T \<inter> V" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

179 
from T openin_subset[OF T(1)] UV have eq: "S = T" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

180 
have "openin U S" unfolding eq using T by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

181 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

182 
{assume S: "openin U S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

183 
hence "\<exists>T. openin U T \<and> S = T \<inter> V" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

184 
using openin_subset[OF S] UV by auto} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

185 
ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

186 
then show ?thesis unfolding topology_eq openin_subtopology by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

187 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

188 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

189 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

190 
lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

191 
by (simp add: subtopology_superset) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

192 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

193 
lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

194 
by (simp add: subtopology_superset) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

195 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

196 
subsection{* The universal Euclidean versions are what we use most of the time *} 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

197 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

198 
definition 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

199 
"open" :: "'a::topological_space set \<Rightarrow> bool" where 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

200 
"open S \<longleftrightarrow> S \<in> topo" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

201 

9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

202 
definition 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

203 
closed :: "'a::topological_space set \<Rightarrow> bool" where 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

204 
"closed S \<longleftrightarrow> open(UNIV  S)" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

205 

9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

206 
definition 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

207 
euclidean :: "'a::topological_space topology" where 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

208 
"euclidean = topology open" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

209 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

210 
lemma open_UNIV[intro,simp]: "open UNIV" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

211 
unfolding open_def by (rule topo_UNIV) 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

212 

9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

213 
lemma open_inter[intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

214 
unfolding open_def by (rule topo_Int) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

215 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

216 
lemma open_Union[intro]: "(\<forall>S\<in>K. open S) \<Longrightarrow> open (\<Union> K)" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

217 
unfolding open_def subset_eq [symmetric] by (rule topo_Union) 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

218 

9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

219 
lemma open_empty[intro,simp]: "open {}" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

220 
using open_Union [of "{}"] by simp 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

221 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

222 
lemma open_openin: "open S \<longleftrightarrow> openin euclidean S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

223 
unfolding euclidean_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

224 
apply (rule cong[where x=S and y=S]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

225 
apply (rule topology_inverse[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

226 
apply (auto simp add: istopology_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

227 
by (auto simp add: mem_def subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

228 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

229 
lemma topspace_euclidean: "topspace euclidean = UNIV" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

230 
apply (simp add: topspace_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

231 
apply (rule set_ext) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

232 
by (auto simp add: open_openin[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

233 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

234 
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

235 
by (simp add: topspace_euclidean topspace_subtopology) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

236 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

237 
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

238 
by (simp add: closed_def closedin_def topspace_euclidean open_openin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

239 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

240 
lemma open_Un[intro]: 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

241 
fixes S T :: "'a::topological_space set" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

242 
shows "open S \<Longrightarrow> open T \<Longrightarrow> open (S\<union>T)" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

243 
by (auto simp add: open_openin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

244 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

245 
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

246 
by (simp add: open_openin openin_subopen[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

247 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

248 
lemma closed_empty[intro, simp]: "closed {}" by (simp add: closed_closedin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

249 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

250 
lemma closed_UNIV[simp,intro]: "closed UNIV" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

251 
by (simp add: closed_closedin topspace_euclidean[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

252 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

253 
lemma closed_Un[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<union>T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

254 
by (auto simp add: closed_closedin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

255 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

256 
lemma closed_Int[intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S\<inter>T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

257 
by (auto simp add: closed_closedin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

258 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

259 
lemma closed_Inter[intro]: assumes H: "\<forall>S \<in>K. closed S" shows "closed (\<Inter>K)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

260 
using H 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

261 
unfolding closed_closedin 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

262 
apply (cases "K = {}") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

263 
apply (simp add: closed_closedin[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

264 
apply (rule closedin_Inter, auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

265 
done 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

266 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

267 
lemma open_closed: "open S \<longleftrightarrow> closed (UNIV  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

268 
by (simp add: open_openin closed_closedin topspace_euclidean openin_closedin_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

269 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

270 
lemma closed_open: "closed S \<longleftrightarrow> open(UNIV  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

271 
by (simp add: open_openin closed_closedin topspace_euclidean closedin_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

272 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

273 
lemma open_diff[intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S  T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

274 
by (auto simp add: open_openin closed_closedin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

275 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

276 
lemma closed_diff[intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed(ST)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

277 
by (auto simp add: open_openin closed_closedin) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

278 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

279 
lemma open_Inter[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. open T" shows "open (\<Inter>S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

280 
using h by (induct rule: finite_induct[OF fS], auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

281 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

282 
lemma closed_Union[intro]: assumes fS: "finite S" and h: "\<forall>T\<in>S. closed T" shows "closed (\<Union>S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

283 
using h by (induct rule: finite_induct[OF fS], auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

284 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

285 
subsection{* Open and closed balls. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

286 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

287 
definition 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

288 
ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

289 
"ball x e = {y. dist x y < e}" 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

290 

0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

291 
definition 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

292 
cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

293 
"cball x e = {y. dist x y \<le> e}" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

294 

30488  295 
lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def) 
296 
lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def) 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

297 

80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

298 
lemma mem_ball_0 [simp]: 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

299 
fixes x :: "'a::real_normed_vector" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

300 
shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

301 
by (simp add: dist_norm) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

302 

80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

303 
lemma mem_cball_0 [simp]: 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

304 
fixes x :: "'a::real_normed_vector" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

305 
shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

306 
by (simp add: dist_norm) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

307 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

308 
lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e" by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

309 
lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

310 
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

311 
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

312 
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

313 
by (simp add: expand_set_eq) arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

314 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

315 
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" 
30488  316 
by (simp add: expand_set_eq) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

317 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

318 
subsection{* Topological properties of open balls *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

319 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

320 
lemma open_dist: 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

321 
fixes S :: "'a::metric_space set" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

322 
shows "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

323 
unfolding open_def topo_dist by simp 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

324 

30488  325 
lemma diff_less_iff: "(a::real)  b > 0 \<longleftrightarrow> a > b" 
326 
"(a::real)  b < 0 \<longleftrightarrow> a < b" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

327 
"a  b < c \<longleftrightarrow> a < c +b" "a  b > c \<longleftrightarrow> a > c +b" by arith+ 
30488  328 
lemma diff_le_iff: "(a::real)  b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real)  b \<le> 0 \<longleftrightarrow> a \<le> b" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

329 
"a  b \<le> c \<longleftrightarrow> a \<le> c +b" "a  b \<ge> c \<longleftrightarrow> a \<ge> c +b" by arith+ 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

330 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

331 
lemma open_ball[intro, simp]: "open (ball x e)" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

332 
unfolding open_dist ball_def Collect_def Ball_def mem_def 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

333 
unfolding dist_commute 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

334 
apply clarify 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

335 
apply (rule_tac x="e  dist xa x" in exI) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

336 
using dist_triangle_alt[where z=x] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

337 
apply (clarsimp simp add: diff_less_iff) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

338 
apply atomize 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

339 
apply (erule_tac x="x'" in allE) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

340 
apply (erule_tac x="xa" in allE) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

341 
by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

342 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

343 
lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

344 
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

345 
unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

346 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

347 
lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

348 
by (metis open_contains_ball subset_eq centre_in_ball) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

349 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

350 
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

351 
unfolding mem_ball expand_set_eq 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

352 
apply (simp add: not_less) 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

353 
by (metis zero_le_dist order_trans dist_self) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

354 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

355 
lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

356 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

357 
subsection{* Basic "localization" results are handy for connectedness. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

358 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

359 
lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

360 
by (auto simp add: openin_subtopology open_openin[symmetric]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

361 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

362 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)" 
30488  363 
by (auto simp add: openin_open) 
364 

365 
lemma open_openin_trans[trans]: 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

366 
"open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

367 
by (metis Int_absorb1 openin_open_Int) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

368 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

369 
lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

370 
by (auto simp add: openin_open) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

371 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

372 
lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

373 
by (simp add: closedin_subtopology closed_closedin Int_ac) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

374 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

375 
lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \<inter> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

376 
by (metis closedin_closed) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

377 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

378 
lemma closed_closedin_trans: "closed S \<Longrightarrow> closed T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> closedin (subtopology euclidean S) T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

379 
apply (subgoal_tac "S \<inter> T = T" ) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

380 
apply auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

381 
apply (frule closedin_closed_Int[of T S]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

382 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

383 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

384 
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

385 
by (auto simp add: closedin_closed) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

386 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

387 
lemma openin_euclidean_subtopology_iff: 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

388 
fixes S U :: "'a::metric_space set" 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

389 
shows "openin (subtopology euclidean U) S 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

390 
\<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

391 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

392 
{assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric] 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

393 
by (simp add: open_dist) blast} 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

394 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

395 
{assume SU: "S \<subseteq> U" and H: "\<And>x. x \<in> S \<Longrightarrow> \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x' \<in> S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

396 
from H obtain d where d: "\<And>x . x\<in> S \<Longrightarrow> d x > 0 \<and> (\<forall>x' \<in> U. dist x' x < d x \<longrightarrow> x' \<in> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

397 
by metis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

398 
let ?T = "\<Union>{B. \<exists>x\<in>S. B = ball x (d x)}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

399 
have oT: "open ?T" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

400 
{ fix x assume "x\<in>S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

401 
hence "x \<in> \<Union>{B. \<exists>x\<in>S. B = ball x (d x)}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

402 
apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

403 
by (rule d [THEN conjunct1]) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

404 
hence "x\<in> ?T \<inter> U" using SU and `x\<in>S` by auto } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

405 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

406 
{ fix y assume "y\<in>?T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

407 
then obtain B where "y\<in>B" "B\<in>{B. \<exists>x\<in>S. B = ball x (d x)}" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

408 
then obtain x where "x\<in>S" and x:"y \<in> ball x (d x)" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

409 
assume "y\<in>U" 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

410 
hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) } 
30488  411 
ultimately have "S = ?T \<inter> U" by blast 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

412 
with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

413 
ultimately show ?thesis by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

414 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

415 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

416 
text{* These "transitivity" results are handy too. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

417 

30488  418 
lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

419 
\<Longrightarrow> openin (subtopology euclidean U) S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

420 
unfolding open_openin openin_open by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

421 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

422 
lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

423 
by (auto simp add: openin_open intro: openin_trans) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

424 

30488  425 
lemma closedin_trans[trans]: 
426 
"closedin (subtopology euclidean T) S \<Longrightarrow> 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

427 
closedin (subtopology euclidean U) T 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

428 
==> closedin (subtopology euclidean U) S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

429 
by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

430 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

431 
lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

432 
by (auto simp add: closedin_closed intro: closedin_trans) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

433 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

434 
subsection{* Connectedness *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

435 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

436 
definition "connected S \<longleftrightarrow> 
30488  437 
~(\<exists>e1 e2. open e1 \<and> open e2 \<and> S \<subseteq> (e1 \<union> e2) \<and> (e1 \<inter> e2 \<inter> S = {}) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

438 
\<and> ~(e1 \<inter> S = {}) \<and> ~(e2 \<inter> S = {}))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

439 

30488  440 
lemma connected_local: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

441 
"connected S \<longleftrightarrow> ~(\<exists>e1 e2. 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

442 
openin (subtopology euclidean S) e1 \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

443 
openin (subtopology euclidean S) e2 \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

444 
S \<subseteq> e1 \<union> e2 \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

445 
e1 \<inter> e2 = {} \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

446 
~(e1 = {}) \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

447 
~(e2 = {}))" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

448 
unfolding connected_def openin_open by (safe, blast+) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

449 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

450 
lemma exists_diff: "(\<exists>S. P(UNIV  S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

451 
proof 
30488  452 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

453 
{assume "?lhs" hence ?rhs by blast } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

454 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

455 
{fix S assume H: "P S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

456 
have "S = UNIV  (UNIV  S)" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

457 
with H have "P (UNIV  (UNIV  S))" by metis } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

458 
ultimately show ?thesis by metis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

459 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

460 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

461 
lemma connected_clopen: "connected S \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

462 
(\<forall>T. openin (subtopology euclidean S) T \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

463 
closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

464 
proof 
30488  465 
have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (UNIV  e2) \<and> S \<subseteq> e1 \<union> (UNIV  e2) \<and> e1 \<inter> (UNIV  e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV  e2) \<inter> S \<noteq> {})" 
466 
unfolding connected_def openin_open closedin_closed 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

467 
apply (subst exists_diff) by blast 
30488  468 
hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV  e2) \<and> e1 \<inter> (UNIV  e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV  e2) \<inter> S \<noteq> {})" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

469 
(is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

470 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

471 
have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

472 
(is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

473 
unfolding connected_def openin_open closedin_closed by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

474 
{fix e2 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

475 
{fix e1 have "?P e2 e1 \<longleftrightarrow> (\<exists>t. closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

476 
by auto} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

477 
then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

478 
then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

479 
then show ?thesis unfolding th0 th1 by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

480 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

481 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

482 
lemma connected_empty[simp, intro]: "connected {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

483 
by (simp add: connected_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

484 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

485 
subsection{* Hausdorff and other separation properties *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

486 

31421  487 
axclass t0_space \<subseteq> topological_space 
488 
t0_space: 

489 
"x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)" 

490 

491 
axclass t1_space \<subseteq> topological_space 

492 
t1_space: 

493 
"x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<notin> U \<and> x \<notin> V \<and> y \<in> V" 

494 

495 
instance t1_space \<subseteq> t0_space 

496 
by default (fast dest: t1_space) 

497 

498 
text {* T2 spaces are also known as Hausdorff spaces. *} 

499 

500 
axclass t2_space \<subseteq> topological_space 

501 
hausdorff: 

502 
"x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

503 

504 
instance t2_space \<subseteq> t1_space 

505 
by default (fast dest: hausdorff) 

506 

507 
instance metric_space \<subseteq> t2_space 

508 
proof 

509 
fix x y :: "'a::metric_space" 

510 
assume xy: "x \<noteq> y" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

511 
let ?U = "ball x (dist x y / 2)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

512 
let ?V = "ball y (dist x y / 2)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

513 
have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

514 
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith 
31421  515 
have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}" 
516 
using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] 

517 
by (auto simp add: expand_set_eq) 

518 
then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" 

519 
by blast 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

520 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

521 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

522 
lemma separation_t2: 
31421  523 
fixes x y :: "'a::t2_space" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

524 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 
30488  525 
using hausdorff[of x y] by blast 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

526 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

527 
lemma separation_t1: 
31421  528 
fixes x y :: "'a::t1_space" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

529 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in>U \<and> y\<notin> U \<and> x\<notin>V \<and> y\<in>V)" 
31421  530 
using t1_space[of x y] by blast 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

531 

31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

532 
lemma separation_t0: 
31421  533 
fixes x y :: "'a::t0_space" 
534 
shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" 

535 
using t0_space[of x y] by blast 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

536 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

537 
subsection{* Limit points *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

538 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

539 
definition 
31420  540 
islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool" 
541 
(infixr "islimpt" 60) where 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

542 
"x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

543 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

544 
(* FIXME: Sure this form is OK????*) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

545 
lemma islimptE: assumes "x islimpt S" and "x \<in> T" and "open T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

546 
obtains "(\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

547 
using assms unfolding islimpt_def by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

548 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

549 
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def) 
31420  550 

551 
lemma islimpt_approachable: 

552 
fixes x :: "'a::metric_space" 

553 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

554 
unfolding islimpt_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

555 
apply auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

556 
apply(erule_tac x="ball x e" in allE) 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

557 
apply auto 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

558 
apply(rule_tac x=y in bexI) 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

559 
apply (auto simp add: dist_commute) 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

560 
apply (simp add: open_dist, drule (1) bspec) 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

561 
apply (clarify, drule spec, drule (1) mp, auto) 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

562 
done 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

563 

31420  564 
lemma islimpt_approachable_le: 
565 
fixes x :: "'a::metric_space" 

566 
shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

567 
unfolding islimpt_approachable 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

568 
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"] 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

569 
by metis (* FIXME: VERY slow! *) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

570 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

571 
axclass perfect_space \<subseteq> metric_space 
31420  572 
(* FIXME: perfect_space should inherit from topological_space *) 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

573 
islimpt_UNIV [simp, intro]: "x islimpt UNIV" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

574 

80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

575 
lemma perfect_choose_dist: 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

576 
fixes x :: "'a::perfect_space" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

577 
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

578 
using islimpt_UNIV [of x] 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

579 
by (simp add: islimpt_approachable) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

580 

80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

581 
instance real :: perfect_space 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

582 
apply default 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

583 
apply (rule islimpt_approachable [THEN iffD2]) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

584 
apply (clarify, rule_tac x="x + e/2" in bexI) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

585 
apply (auto simp add: dist_norm) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

586 
done 
31420  587 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

588 
instance "^" :: (perfect_space, finite) perfect_space 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

589 
proof 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

590 
fix x :: "'a ^ 'b" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

591 
{ 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

592 
fix e :: real assume "0 < e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

593 
def a \<equiv> "x $ arbitrary" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

594 
have "a islimpt UNIV" by (rule islimpt_UNIV) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

595 
with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

596 
unfolding islimpt_approachable by auto 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

597 
def y \<equiv> "Cart_lambda ((Cart_nth x)(arbitrary := b))" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

598 
from `b \<noteq> a` have "y \<noteq> x" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

599 
unfolding a_def y_def by (simp add: Cart_eq) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

600 
from `dist b a < e` have "dist y x < e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

601 
unfolding dist_vector_def a_def y_def 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

602 
apply simp 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

603 
apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]]) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

604 
apply (subst setsum_diff1' [where a=arbitrary], simp, simp, simp) 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

605 
done 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

606 
from `y \<noteq> x` and `dist y x < e` 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

607 
have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

608 
} 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

609 
then show "x islimpt UNIV" unfolding islimpt_approachable by blast 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

610 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

611 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

612 
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

613 
unfolding closed_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

614 
apply (subst open_subopen) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

615 
apply (simp add: islimpt_def subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

616 
by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

617 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

618 
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" 
31420  619 
unfolding islimpt_def by auto 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

620 

30582  621 
lemma closed_positive_orthant: "closed {x::real^'n::finite. \<forall>i. 0 \<le>x$i}" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

622 
proof 
30582  623 
let ?U = "UNIV :: 'n set" 
624 
let ?O = "{x::real^'n. \<forall>i. x$i\<ge>0}" 

625 
{fix x:: "real^'n" and i::'n assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

626 
and xi: "x$i < 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

627 
from xi have th0: "x$i > 0" by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

628 
from H[rule_format, OF th0] obtain x' where x': "x' \<in>?O" "x' \<noteq> x" "dist x' x < x $ i" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

629 
have th:" \<And>b a (x::real). abs x <= b \<Longrightarrow> b <= a ==> ~(a + x < 0)" by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

630 
have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y  x)" by arith 
30582  631 
have th1: "\<bar>x$i\<bar> \<le> \<bar>(x'  x)$i\<bar>" using x'(1) xi 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

632 
apply (simp only: vector_component) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

633 
by (rule th') auto 
30582  634 
have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x'  x)$i\<bar>" using component_le_norm[of "x'x" i] 
31289  635 
apply (simp add: dist_norm) by norm 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

636 
from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) } 
30488  637 
then show ?thesis unfolding closed_limpt islimpt_approachable 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

638 
unfolding not_le[symmetric] by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

639 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

640 

31289  641 
lemma finite_set_avoid: 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

642 
fixes a :: "'a::metric_space" 
31289  643 
assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

644 
proof(induct rule: finite_induct[OF fS]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

645 
case 1 thus ?case apply auto by ferrack 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

646 
next 
30488  647 
case (2 x F) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

648 
from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

649 
{assume "x = a" hence ?case using d by auto } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

650 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

651 
{assume xa: "x\<noteq>a" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

652 
let ?d = "min d (dist a x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

653 
have dp: "?d > 0" using xa d(1) using dist_nz by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

654 
from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

655 
with dp xa have ?case by(auto intro!: exI[where x="?d"]) } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

656 
ultimately show ?case by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

657 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

658 

31420  659 
lemma islimpt_finite: 
660 
fixes S :: "'a::metric_space set" 

661 
assumes fS: "finite S" shows "\<not> a islimpt S" 

30488  662 
unfolding islimpt_approachable 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

663 
using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

664 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

665 
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

666 
apply (rule iffI) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

667 
defer 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

668 
apply (metis Un_upper1 Un_upper2 islimpt_subset) 
31420  669 
unfolding islimpt_def 
670 
apply (rule ccontr, clarsimp, rename_tac A B) 

671 
apply (drule_tac x="A \<inter> B" in spec) 

672 
apply (auto simp add: open_inter) 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

673 
done 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

674 

30488  675 
lemma discrete_imp_closed: 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

676 
fixes S :: "'a::metric_space set" 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

677 
assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

678 
shows "closed S" 
30488  679 
proof 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

680 
{fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

681 
from e have e2: "e/2 > 0" by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

682 
from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

683 
let ?m = "min (e/2) (dist x y) " 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

684 
from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

685 
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

686 
have th: "dist z y < e" using z y 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

687 
by (intro dist_triangle_lt [where z=x], simp) 
30488  688 
from d[rule_format, OF y(1) z(1) th] y z 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

689 
have False by (auto simp add: dist_commute)} 
31420  690 
then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

691 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

692 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

693 
subsection{* Interior of a Set *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

694 
definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

695 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

696 
lemma interior_eq: "interior S = S \<longleftrightarrow> open S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

697 
apply (simp add: expand_set_eq interior_def) 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

698 
apply (subst (2) open_subopen) by (safe, blast+) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

699 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

700 
lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

701 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

702 
lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

703 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

704 
lemma open_interior[simp, intro]: "open(interior S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

705 
apply (simp add: interior_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

706 
apply (subst open_subopen) by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

707 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

708 
lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior) 
30488  709 
lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

710 
lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

711 
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

712 
lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

713 
by (metis equalityI interior_maximal interior_subset open_interior) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

714 
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

715 
apply (simp add: interior_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

716 
by (metis open_contains_ball centre_in_ball open_ball subset_trans) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

717 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

718 
lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

719 
by (metis interior_maximal interior_subset subset_trans) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

720 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

721 
lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

722 
apply (rule equalityI, simp) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

723 
apply (metis Int_lower1 Int_lower2 subset_interior) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

724 
by (metis Int_mono interior_subset open_inter open_interior open_subset_interior) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

725 

31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

726 
lemma interior_limit_point [intro]: 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

727 
fixes x :: "'a::perfect_space" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

728 
assumes x: "x \<in> interior S" shows "x islimpt S" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

729 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

730 
from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

731 
unfolding mem_interior subset_eq Ball_def mem_ball by blast 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

732 
{ 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

733 
fix d::real assume d: "d>0" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

734 
let ?m = "min d e" 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

735 
have mde2: "0 < ?m" using e(1) d(1) by simp 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

736 
from perfect_choose_dist [OF mde2, of x] 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

737 
obtain y where "y \<noteq> x" and "dist y x < ?m" by blast 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

738 
then have "dist y x < e" "dist y x < d" by simp_all 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

739 
from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute) 
30488  740 
have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d" 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

741 
using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast 
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

742 
} 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

743 
then show ?thesis unfolding islimpt_approachable by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

744 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

745 

30488  746 
lemma interior_closed_Un_empty_interior: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

747 
assumes cS: "closed S" and iT: "interior T = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

748 
shows "interior(S \<union> T) = interior S" 
31394
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

749 
proof 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

750 
show "interior S \<subseteq> interior (S\<union>T)" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

751 
by (rule subset_interior, blast) 
31394
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

752 
next 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

753 
show "interior (S \<union> T) \<subseteq> interior S" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

754 
proof 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

755 
fix x assume "x \<in> interior (S \<union> T)" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

756 
then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

757 
unfolding interior_def by fast 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

758 
show "x \<in> interior S" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

759 
proof (rule ccontr) 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

760 
assume "x \<notin> interior S" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

761 
with `x \<in> R` `open R` obtain y where "y \<in> R  S" 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

762 
unfolding interior_def expand_set_eq by fast 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

763 
from `open R` `closed S` have "open (R  S)" by (rule open_diff) 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

764 
from `R \<subseteq> S \<union> T` have "R  S \<subseteq> T" by fast 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

765 
from `y \<in> R  S` `open (R  S)` `R  S \<subseteq> T` `interior T = {}` 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

766 
show "False" unfolding interior_def by fast 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

767 
qed 
8d8417abb14f
generalize lemma interior_closed_Un_empty_interior
huffman
parents:
31393
diff
changeset

768 
qed 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

769 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

770 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

771 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

772 
subsection{* Closure of a Set *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

773 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

774 
definition "closure S = S \<union> {x  x. x islimpt S}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

775 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

776 
lemma closure_interior: "closure S = UNIV  interior (UNIV  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

777 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

778 
{ fix x 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

779 
have "x\<in>UNIV  interior (UNIV  S) \<longleftrightarrow> x \<in> closure S" (is "?lhs = ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

780 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

781 
let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> UNIV  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

782 
assume "?lhs" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

783 
hence *:"\<not> ?exT x" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

784 
unfolding interior_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

785 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

786 
{ assume "\<not> ?rhs" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

787 
hence False using * 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

788 
unfolding closure_def islimpt_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

789 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

790 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

791 
thus "?rhs" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

792 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

793 
next 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

794 
assume "?rhs" thus "?lhs" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

795 
unfolding closure_def interior_def islimpt_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

796 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

797 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

798 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

799 
thus ?thesis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

800 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

801 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

802 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

803 
lemma interior_closure: "interior S = UNIV  (closure (UNIV  S))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

804 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

805 
{ fix x 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

806 
have "x \<in> interior S \<longleftrightarrow> x \<in> UNIV  (closure (UNIV  S))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

807 
unfolding interior_def closure_def islimpt_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

808 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

809 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

810 
thus ?thesis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

811 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

812 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

813 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

814 
lemma closed_closure[simp, intro]: "closed (closure S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

815 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

816 
have "closed (UNIV  interior (UNIV S))" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

817 
thus ?thesis using closure_interior[of S] by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

818 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

819 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

820 
lemma closure_hull: "closure S = closed hull S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

821 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

822 
have "S \<subseteq> closure S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

823 
unfolding closure_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

824 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

825 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

826 
have "closed (closure S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

827 
using closed_closure[of S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

828 
by assumption 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

829 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

830 
{ fix t 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

831 
assume *:"S \<subseteq> t" "closed t" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

832 
{ fix x 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

833 
assume "x islimpt S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

834 
hence "x islimpt t" using *(1) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

835 
using islimpt_subset[of x, of S, of t] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

836 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

837 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

838 
with * have "closure S \<subseteq> t" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

839 
unfolding closure_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

840 
using closed_limpt[of t] 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

841 
by auto 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

842 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

843 
ultimately show ?thesis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

844 
using hull_unique[of S, of "closure S", of closed] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

845 
unfolding mem_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

846 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

847 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

848 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

849 
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

850 
unfolding closure_hull 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

851 
using hull_eq[of closed, unfolded mem_def, OF closed_Inter, of S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

852 
by (metis mem_def subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

853 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

854 
lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

855 
using closure_eq[of S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

856 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

857 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

858 
lemma closure_closure[simp]: "closure (closure S) = closure S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

859 
unfolding closure_hull 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

860 
using hull_hull[of closed S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

861 
by assumption 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

862 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

863 
lemma closure_subset: "S \<subseteq> closure S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

864 
unfolding closure_hull 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

865 
using hull_subset[of S closed] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

866 
by assumption 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

867 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

868 
lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

869 
unfolding closure_hull 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

870 
using hull_mono[of S T closed] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

871 
by assumption 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

872 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

873 
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

874 
using hull_minimal[of S T closed] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

875 
unfolding closure_hull mem_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

876 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

877 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

878 
lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

879 
using hull_unique[of S T closed] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

880 
unfolding closure_hull mem_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

881 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

882 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

883 
lemma closure_empty[simp]: "closure {} = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

884 
using closed_empty closure_closed[of "{}"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

885 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

886 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

887 
lemma closure_univ[simp]: "closure UNIV = UNIV" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

888 
using closure_closed[of UNIV] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

889 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

890 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

891 
lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

892 
using closure_empty closure_subset[of S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

893 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

894 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

895 
lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

896 
using closure_eq[of S] closure_subset[of S] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

897 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

898 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

899 
lemma open_inter_closure_eq_empty: 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

900 
"open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

901 
using open_subset_interior[of S "UNIV  T"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

902 
using interior_subset[of "UNIV  T"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

903 
unfolding closure_interior 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

904 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

905 

31420  906 
lemma open_inter_closure_subset: 
907 
fixes S :: "'a::metric_space set" 

908 
(* FIXME: generalize to topological_space *) 

909 
shows "open S \<Longrightarrow> (S \<inter> (closure T)) \<subseteq> closure(S \<inter> T)" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

910 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

911 
fix x 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

912 
assume as: "open S" "x \<in> S \<inter> closure T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

913 
{ assume *:"x islimpt T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

914 
{ fix e::real 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

915 
assume "e > 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

916 
from as `open S` obtain e' where "e' > 0" and e':"\<forall>x'. dist x' x < e' \<longrightarrow> x' \<in> S" 
31418
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

917 
unfolding open_dist 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

918 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

919 
let ?e = "min e e'" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

920 
from `e>0` `e'>0` have "?e > 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

921 
by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

922 
then obtain y where y:"y\<in>T" "y \<noteq> x \<and> dist y x < ?e" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

923 
using islimpt_approachable[of x T] using * 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

924 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

925 
hence "\<exists>x'\<in>S \<inter> T. x' \<noteq> x \<and> dist x' x < e" using e' 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

926 
using y 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

927 
by(rule_tac x=y in bexI, simp+) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

928 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

929 
hence "x islimpt S \<inter> T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

930 
using islimpt_approachable[of x "S \<inter> T"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

931 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

932 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

933 
then show "x \<in> closure (S \<inter> T)" using as 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

934 
unfolding closure_def 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

935 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

936 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

937 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

938 
lemma closure_complement: "closure(UNIV  S) = UNIV  interior(S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

939 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

940 
have "S = UNIV  (UNIV  S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

941 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

942 
thus ?thesis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

943 
unfolding closure_interior 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

944 
by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

945 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

946 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

947 
lemma interior_complement: "interior(UNIV  S) = UNIV  closure(S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

948 
unfolding closure_interior 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

949 
by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

950 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

951 
subsection{* Frontier (aka boundary) *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

952 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

953 
definition "frontier S = closure S  interior S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

954 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

955 
lemma frontier_closed: "closed(frontier S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

956 
by (simp add: frontier_def closed_diff closed_closure) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

957 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

958 
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV  S))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

959 
by (auto simp add: frontier_def interior_closure) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

960 

31420  961 
lemma frontier_straddle: 
962 
fixes a :: "'a::metric_space" 

963 
shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))" (is "?lhs \<longleftrightarrow> ?rhs") 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

964 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

965 
assume "?lhs" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

966 
{ fix e::real 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

967 
assume "e > 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

968 
let ?rhse = "(\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

969 
{ assume "a\<in>S" 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

970 
have "\<exists>x\<in>S. dist a x < e" using `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

971 
moreover have "\<exists>x. x \<notin> S \<and> dist a x < e" using `?lhs` `a\<in>S` 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

972 
unfolding frontier_closures closure_def islimpt_def using `e>0` 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

973 
by (auto, erule_tac x="ball a e" in allE, auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

974 
ultimately have ?rhse by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

975 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

976 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

977 
{ assume "a\<notin>S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

978 
hence ?rhse using `?lhs` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

979 
unfolding frontier_closures closure_def islimpt_def 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

980 
using open_ball[of a e] `e > 0` 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

981 
by (auto, erule_tac x = "ball a e" in allE, auto) (* FIXME: VERY slow! *) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

982 
} 
30488  983 
ultimately have ?rhse by auto 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

984 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

985 
thus ?rhs by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

986 
next 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

987 
assume ?rhs 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

988 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

989 
{ fix T assume "a\<notin>S" and 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

990 
as:"\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)" "a \<notin> S" "a \<in> T" "open T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

991 
from `open T` `a \<in> T` have "\<exists>e>0. ball a e \<subseteq> T" unfolding open_contains_ball[of T] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

992 
then obtain e where "e>0" "ball a e \<subseteq> T" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

993 
then obtain y where y:"y\<in>S" "dist a y < e" using as(1) by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

994 
have "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> a" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

995 
using `dist a y < e` `ball a e \<subseteq> T` unfolding ball_def using `y\<in>S` `a\<notin>S` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

996 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

997 
hence "a \<in> closure S" unfolding closure_def islimpt_def using `?rhs` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

998 
moreover 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

999 
{ fix T assume "a \<in> T" "open T" "a\<in>S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1000 
then obtain e where "e>0" and balle: "ball a e \<subseteq> T" unfolding open_contains_ball using `?rhs` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1001 
obtain x where "x \<notin> S" "dist a x < e" using `?rhs` using `e>0` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1002 
hence "\<exists>y\<in>UNIV  S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1003 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1004 
hence "a islimpt (UNIV  S) \<or> a\<notin>S" unfolding islimpt_def by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1005 
ultimately show ?lhs unfolding frontier_closures using closure_def[of "UNIV  S"] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1006 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1007 

30488  1008 
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1009 
by (metis frontier_def closure_closed Diff_subset) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1010 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1011 
lemma frontier_empty: "frontier {} = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1012 
by (simp add: frontier_def closure_empty) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1013 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1014 
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1015 
proof 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1016 
{ assume "frontier S \<subseteq> S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1017 
hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1018 
hence "closed S" using closure_subset_eq by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1019 
} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1020 
thus ?thesis using frontier_subset_closed[of S] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1021 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1022 

30488  1023 
lemma frontier_complement: "frontier(UNIV  S) = frontier S" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1024 
by (auto simp add: frontier_def closure_complement interior_complement) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1025 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1026 
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S" 
30488  1027 
using frontier_complement frontier_subset_eq[of "UNIV  S"] 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1028 
unfolding open_closed by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1029 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1030 
subsection{* Common nets and The "within" modifier for nets. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1031 

31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

1032 
definition 
31346  1033 
at_infinity :: "'a::real_normed_vector net" where 
31390  1034 
"at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))" 
31346  1035 

1036 
definition 

1037 
indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where 

1038 
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b  a = c*s v}" 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1039 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1040 
text{* Prove That They are all nets. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1041 

31390  1042 
lemma Rep_net_at_infinity: 
1043 
"Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})" 

1044 
unfolding at_infinity_def 

1045 
apply (rule Abs_net_inverse') 

1046 
apply (rule image_nonempty, simp) 

1047 
apply (clarsimp, rename_tac r s) 

1048 
apply (rule_tac x="max r s" in exI, auto) 

1049 
done 

1050 

31346  1051 
lemma within_UNIV: "net within UNIV = net" 
31390  1052 
by (simp add: Rep_net_inject [symmetric] Rep_net_within) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1053 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1054 
subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1055 

31346  1056 
definition 
1057 
trivial_limit :: "'a net \<Rightarrow> bool" where 

31390  1058 
"trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net" 
31346  1059 

1060 
lemma trivial_limit_within: 

1061 
shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S" 

31390  1062 
proof 
1063 
assume "trivial_limit (at a within S)" 

1064 
thus "\<not> a islimpt S" 

1065 
unfolding trivial_limit_def 

1066 
unfolding Rep_net_within Rep_net_at 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1067 
unfolding islimpt_def open_def [symmetric] 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1068 
apply (clarsimp simp add: expand_set_eq) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1069 
apply (rename_tac T, rule_tac x=T in exI) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1070 
apply (clarsimp, drule_tac x=y in spec, simp) 
31390  1071 
done 
1072 
next 

1073 
assume "\<not> a islimpt S" 

1074 
thus "trivial_limit (at a within S)" 

1075 
unfolding trivial_limit_def 

1076 
unfolding Rep_net_within Rep_net_at 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1077 
unfolding islimpt_def open_def [symmetric] 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1078 
apply (clarsimp simp add: image_image) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1079 
apply (rule_tac x=T in image_eqI) 
31390  1080 
apply (auto simp add: expand_set_eq) 
1081 
done 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1082 
qed 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1083 

31391  1084 
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV" 
31346  1085 
using trivial_limit_within [of a UNIV] 
1086 
by (simp add: within_UNIV) 

1087 

31391  1088 
lemma trivial_limit_at: 
1089 
fixes a :: "'a::perfect_space" 

1090 
shows "\<not> trivial_limit (at a)" 

1091 
by (simp add: trivial_limit_at_iff) 

1092 

31346  1093 
lemma trivial_limit_at_infinity: 
1094 
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)" 

31391  1095 
(* FIXME: find a more appropriate type class *) 
31390  1096 
unfolding trivial_limit_def Rep_net_at_infinity 
1097 
apply (clarsimp simp add: expand_set_eq) 

1098 
apply (drule_tac x="scaleR r (sgn 1)" in spec) 

1099 
apply (simp add: norm_scaleR norm_sgn) 

1100 
done 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1101 

31346  1102 
lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially" 
31390  1103 
by (auto simp add: trivial_limit_def Rep_net_sequentially) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1104 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1105 
subsection{* Some property holds "sufficiently close" to the limit point. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1106 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1107 
lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *) 
31390  1108 
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1109 
unfolding eventually_at dist_nz by auto 
31390  1110 

1111 
lemma eventually_at_infinity: 

1112 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)" 

1113 
unfolding eventually_def Rep_net_at_infinity by auto 

1114 

31346  1115 
lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow> 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1116 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 
31393  1117 
unfolding eventually_within eventually_at dist_nz by auto 
31390  1118 

1119 
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow> 

1120 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs") 

1121 
unfolding eventually_within 

1122 
apply safe 

1123 
apply (rule_tac x="d/2" in exI, simp) 

1124 
apply (rule_tac x="d" in exI, simp) 

1125 
done 

1126 

1127 
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)" 

1128 
unfolding eventually_def trivial_limit_def 

1129 
using Rep_net_nonempty [of net] by auto 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1130 

31347
357d58c5743a
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
huffman
parents:
31346
diff
changeset

1131 
lemma always_eventually: "(\<forall>x. P x) ==> eventually P net" 
31390  1132 
unfolding eventually_def trivial_limit_def 
1133 
using Rep_net_nonempty [of net] by auto 

31347
357d58c5743a
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
huffman
parents:
31346
diff
changeset

1134 

31348  1135 
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net" 
31390  1136 
unfolding trivial_limit_def eventually_def by auto 
1137 

1138 
lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 

1139 
unfolding trivial_limit_def eventually_def by auto 

31348  1140 

1141 
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)" 

31390  1142 
apply (safe elim!: trivial_limit_eventually) 
1143 
apply (simp add: eventually_False [symmetric]) 

1144 
done 

31348  1145 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1146 
text{* Combining theorems for "eventually" *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1147 

31390  1148 
lemma eventually_conjI: 
1149 
"\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk> 

1150 
\<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net" 

31393  1151 
by (rule eventually_conj) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1152 

31390  1153 
lemma eventually_rev_mono: 
1154 
"eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net" 

1155 
using eventually_mono [of P Q] by fast 

1156 

1157 
lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" 

1158 
by (auto intro!: eventually_conjI elim: eventually_rev_mono) 

1159 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1160 
lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 
31390  1161 
by (auto simp add: eventually_False) 
1162 

1163 
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)" 

1164 
by (simp add: eventually_False) 

31347
357d58c5743a
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
huffman
parents:
31346
diff
changeset

1165 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1166 
subsection{* Limits, defined as vacuously true when the limit is trivial. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1167 

31393  1168 
notation tendsto (infixr ">" 55) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1169 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1170 
text{* Notation Lim to avoid collition with lim defined in analysis *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1171 
definition "Lim net f = (THE l. (f > l) net)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1172 

30488  1173 
lemma Lim: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1174 
"(f > l) net \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1175 
trivial_limit net \<or> 
31348  1176 
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" 
1177 
unfolding tendsto_def trivial_limit_eq by auto 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1178 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1179 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1180 
text{* Show that they yield usual definitions in the various cases. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1181 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1182 
lemma Lim_within_le: "(f > l)(at a within S) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1183 
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1184 
by (auto simp add: tendsto_def eventually_within_le) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1185 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1186 
lemma Lim_within: "(f > l) (at a within S) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1187 
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1188 
by (auto simp add: tendsto_def eventually_within) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1189 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1190 
lemma Lim_at: "(f > l) (at a) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1191 
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1192 
by (auto simp add: tendsto_def eventually_at) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1193 

31342
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1194 
lemma Lim_at_iff_LIM: "(f > l) (at a) \<longleftrightarrow> f  a > l" 
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1195 
unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) 
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1196 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1197 
lemma Lim_at_infinity: 
30582  1198 
"(f > l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1199 
by (auto simp add: tendsto_def eventually_at_infinity) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1200 

30488  1201 
lemma Lim_sequentially: 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1202 
"(S > l) sequentially \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1203 
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1204 
by (auto simp add: tendsto_def eventually_sequentially) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1205 

31342
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1206 
lemma Lim_sequentially_iff_LIMSEQ: "(S > l) sequentially \<longleftrightarrow> S > l" 
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1207 
unfolding Lim_sequentially LIMSEQ_def .. 
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1208 

30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1209 
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f > l) net" 
31348  1210 
unfolding tendsto_def by (auto elim: eventually_rev_mono) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1211 

5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1212 
text{* The expected monotonicity property. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1213 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1214 
lemma Lim_within_empty: "(f > l) (net within {})" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1215 
unfolding tendsto_def Limits.eventually_within by simp 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1216 

97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1217 
lemma Lim_within_subset: "(f > l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f > l) (net within T)" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1218 
unfolding tendsto_def Limits.eventually_within 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1219 
by (auto elim!: eventually_elim1) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1220 

97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1221 
lemma Lim_Un: assumes "(f > l) (net within S)" "(f > l) (net within T)" 
