author  huffman 
Sat, 13 Jun 2009 07:33:50 0700  
changeset 31654  83662a8604c2 
parent 31592  61ee6256d863 
child 31655  bcb1eb2197f8 
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 
31560  9 
imports SEQ Euclidean_Space Product_Vector 
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 
euclidean :: "'a::topological_space topology" where 
9baa48bad81c
generalize some constants and lemmas to class topological_space
huffman
parents:
31402
diff
changeset

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

201 

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

202 
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

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

204 
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

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

206 
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

207 
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

208 

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

209 
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

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

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

212 
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

213 

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

214 
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

215 
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

216 

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

217 
lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

219 

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

220 
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

221 
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

222 

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

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

224 

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

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

226 
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

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

228 

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

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

230 
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

231 
"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

232 

30488  233 
lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def) 
234 
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

235 

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

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

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

238 
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

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

240 

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

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

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

243 
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

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

245 

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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

252 

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

253 
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s" 
30488  254 
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

255 

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

256 
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

257 

30488  258 
lemma diff_less_iff: "(a::real)  b > 0 \<longleftrightarrow> a > b" 
259 
"(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

260 
"a  b < c \<longleftrightarrow> a < c +b" "a  b > c \<longleftrightarrow> a > c +b" by arith+ 
30488  261 
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

262 
"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

263 

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

264 
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

265 
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

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

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

268 
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

269 
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

270 
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

271 
apply atomize 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

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

273 
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

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

275 

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

276 
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

277 
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

278 
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

279 

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

280 
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

281 
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

282 

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

283 
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

284 
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

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

286 
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

287 

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

288 
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

289 

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

290 
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

291 

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

292 
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

293 
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

294 

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

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

298 
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

299 
"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

300 
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

301 

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

302 
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

303 
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

304 

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

305 
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

306 
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

307 

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

308 
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

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

310 

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

311 
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

312 
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

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

314 
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

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

316 

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

317 
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

318 
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

319 

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

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

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

322 
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

323 
\<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

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

325 
{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

326 
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

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

328 
{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

329 
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

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

331 
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

332 
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

333 
{ 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

334 
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

335 
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

336 
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

337 
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

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

339 
{ 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

340 
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

341 
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

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

343 
hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) } 
30488  344 
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

345 
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

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

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

348 

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

349 
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

350 

30488  351 
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

352 
\<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

353 
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

354 

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

355 
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

356 
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

357 

30488  358 
lemma closedin_trans[trans]: 
359 
"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

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

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

362 
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

363 

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

364 
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

365 
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

366 

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

367 
subsection{* Connectedness *} 
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 
definition "connected S \<longleftrightarrow> 
30488  370 
~(\<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

371 
\<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

372 

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

374 
"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

375 
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

376 
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

377 
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

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

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

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

381 
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

382 

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

383 
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

384 
proof 
30488  385 

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

386 
{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

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

388 
{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

389 
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

390 
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

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

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

393 

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

394 
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

395 
(\<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

396 
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

397 
proof 
30488  398 
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> {})" 
399 
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

400 
apply (subst exists_diff) by blast 
30488  401 
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> {})" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

403 

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

404 
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

405 
(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

406 
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

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

408 
{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

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

410 
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

411 
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

412 
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

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

414 

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

415 
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

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

417 

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

418 
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

419 

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

422 

423 
class t1_space = 

424 
assumes t1_space: "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" 

425 
begin 

426 

427 
subclass t0_space 

428 
proof 

429 
qed (fast dest: t1_space) 

430 

431 
end 

31421  432 

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

434 

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

437 
begin 

438 

439 
subclass t1_space 

440 
proof 

441 
qed (fast dest: hausdorff) 

442 

443 
end 

31421  444 

445 
instance metric_space \<subseteq> t2_space 

446 
proof 

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

448 
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

449 
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

450 
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

451 
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

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

455 
by (auto simp add: expand_set_eq) 

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

457 
by blast 

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

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

459 

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

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

462 
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  463 
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

464 

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

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

467 
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  468 
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

469 

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

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

473 
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

474 

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

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

476 

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

477 
definition 
31420  478 
islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool" 
479 
(infixr "islimpt" 60) where 

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

480 
"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

481 

31489
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

482 
lemma islimptI: 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

483 
assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

484 
shows "x islimpt S" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

485 
using assms unfolding islimpt_def by auto 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

486 

10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

487 
lemma islimptE: 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

488 
assumes "x islimpt S" and "x \<in> T" and "open T" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

489 
obtains y where "y \<in> S" and "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

490 
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

491 

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

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

494 
lemma islimpt_approachable: 

495 
fixes x :: "'a::metric_space" 

496 
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

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

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

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

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

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

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

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

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

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

506 

31420  507 
lemma islimpt_approachable_le: 
508 
fixes x :: "'a::metric_space" 

509 
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

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

511 
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

512 
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

513 

31457  514 
class perfect_space = 
31420  515 
(* FIXME: perfect_space should inherit from topological_space *) 
31457  516 
assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV" 
31345
80667d5bee32
generalize topological notions to class metric_space; add class perfect_space
huffman
parents:
31344
diff
changeset

517 

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

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

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

520 
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

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

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

523 

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

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

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

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

527 
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

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

529 
done 
31420  530 

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

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

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

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

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

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

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

537 
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

538 
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

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

540 
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

541 
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

542 
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

543 
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

544 
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

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

546 
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

547 
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

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

549 
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

550 
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

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

552 
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

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

554 

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

555 
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

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

557 
apply (subst open_subopen) 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

559 
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

560 

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

561 
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}" 
31420  562 
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

563 

30582  564 
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

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

568 
{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

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

570 
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

571 
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

572 
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

573 
have th': "\<And>x (y::real). x < 0 \<Longrightarrow> 0 <= y ==> abs x <= abs (y  x)" by arith 
30582  574 
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

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

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

579 
from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) } 
30488  580 
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

581 
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

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

583 

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

585 
fixes a :: "'a::metric_space" 
31289  586 
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

587 
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

588 
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

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

591 
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

592 
{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

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

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

595 
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

596 
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

597 
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

598 
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

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

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

601 

31420  602 
lemma islimpt_finite: 
603 
fixes S :: "'a::metric_space set" 

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

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

606 
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

607 

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

608 
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

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

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

611 
apply (metis Un_upper1 Un_upper2 islimpt_subset) 
31420  612 
unfolding islimpt_def 
613 
apply (rule ccontr, clarsimp, rename_tac A B) 

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

31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

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

617 

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

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

620 
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

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

623 
{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

624 
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

625 
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

626 
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

627 
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

628 
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

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

630 
by (intro dist_triangle_lt [where z=x], simp) 
30488  631 
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

632 
have False by (auto simp add: dist_commute)} 
31420  633 
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

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

635 

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

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

637 
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

638 

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

639 
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

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

641 
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

642 

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

643 
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

644 

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

645 
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

646 

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

647 
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

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

649 
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

650 

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

651 
lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior) 
30488  652 
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

653 
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

654 
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

655 
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

656 
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

657 
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

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

659 
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

660 

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

661 
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

662 
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

663 

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

664 
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

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

666 
apply (metis Int_lower1 Int_lower2 subset_interior) 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

668 

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

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

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

671 
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

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

673 
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

674 
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

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

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

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

678 
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

679 
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

680 
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

681 
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

682 
from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute) 
30488  683 
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

684 
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

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

686 
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

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

688 

30488  689 
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

690 
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

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

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

693 
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

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

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

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

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

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

699 
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

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

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

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

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

704 
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

705 
unfolding interior_def expand_set_eq by fast 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

707 
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

708 
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

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

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

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

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

713 

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

714 

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

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

716 

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

717 
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

718 

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

719 
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

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

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

722 
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

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

724 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

738 
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

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

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

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

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

743 
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 

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

746 
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

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

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

749 
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

750 
unfolding interior_def closure_def islimpt_def 
31585
0e4906ccf280
replace all occurrences of 'op *s' at type real^'n with scaleR
huffman
parents:
31571
diff
changeset

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

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

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

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

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

756 

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

757 
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

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

759 
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

760 
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

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

762 

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

763 
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

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

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

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

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

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

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

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

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

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

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

774 
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

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

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

777 
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

778 
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

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

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

781 
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

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

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

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

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

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

787 
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

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

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

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

791 

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

792 
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

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

794 
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

795 
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

796 

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

797 
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

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

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

800 

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

801 
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

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

803 
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

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

805 

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

806 
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

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

808 
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

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

810 

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

811 
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

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

813 
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

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

815 

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

816 
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

817 
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

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

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

820 

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

821 
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

822 
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

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

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

825 

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

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

827 
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

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

829 

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

830 
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

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

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

833 

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

834 
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

835 
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

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 
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

839 
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

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

841 

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

842 
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

843 
"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

844 
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

845 
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

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

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

848 

31420  849 
lemma open_inter_closure_subset: 
31489
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

850 
"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

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

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

853 
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

854 
{ assume *:"x islimpt T" 
31489
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

855 
have "x islimpt (S \<inter> T)" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

856 
proof (rule islimptI) 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

857 
fix A 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

858 
assume "x \<in> A" "open A" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

859 
with as have "x \<in> A \<inter> S" "open (A \<inter> S)" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

860 
by (simp_all add: open_Int) 
31489
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

861 
with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

862 
by (rule islimptE) 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

863 
hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x" 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

864 
by simp_all 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

865 
thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" .. 
10080e31b294
lemmas islimptI, islimptE; generalize open_inter_closure_subset
huffman
parents:
31488
diff
changeset

866 
qed 
30262
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 
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

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

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

871 
qed 
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_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

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

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

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

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

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

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

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

881 

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

882 
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

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

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

885 

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

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

887 

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

888 
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

889 

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

890 
lemma frontier_closed: "closed(frontier S)" 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

892 

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

893 
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

894 
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

895 

31420  896 
lemma frontier_straddle: 
897 
fixes a :: "'a::metric_space" 

898 
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

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

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

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

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

903 
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

904 
{ assume "a\<in>S" 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

905 
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

906 
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

907 
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

908 
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

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

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

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

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

913 
hence ?rhse using `?lhs` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

914 
unfolding frontier_closures closure_def islimpt_def 
31285
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

915 
using open_ball[of a e] `e > 0` 
0a3f9ee4117c
generalize dist function to class real_normed_vector
huffman
parents:
31275
diff
changeset

916 
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

917 
} 
30488  918 
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

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

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

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

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

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

924 
{ 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

925 
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

926 
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

927 
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

928 
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

929 
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

930 
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

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

932 
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

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

934 
{ 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

935 
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

936 
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

937 
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

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

939 
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

940 
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

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

942 

30488  943 
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

944 
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

945 

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

946 
lemma frontier_empty: "frontier {} = {}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

947 
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

948 

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

949 
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

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

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

952 
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

953 
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

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

955 
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

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

957 

30488  958 
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

959 
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

960 

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

961 
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S" 
30488  962 
using frontier_complement frontier_subset_eq[of "UNIV  S"] 
31490
c350f3ad6b0d
move definitions of open, closed to RealVector.thy
huffman
parents:
31489
diff
changeset

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

964 

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

965 
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

966 

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

967 
definition 
31346  968 
at_infinity :: "'a::real_normed_vector net" where 
31390  969 
"at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))" 
31346  970 

971 
definition 

31530  972 
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where 
973 
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b  a = scaleR c v}" 

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

974 

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

975 
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

976 

31390  977 
lemma Rep_net_at_infinity: 
978 
"Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})" 

979 
unfolding at_infinity_def 

980 
apply (rule Abs_net_inverse') 

981 
apply (rule image_nonempty, simp) 

982 
apply (clarsimp, rename_tac r s) 

983 
apply (rule_tac x="max r s" in exI, auto) 

984 
done 

985 

31346  986 
lemma within_UNIV: "net within UNIV = net" 
31390  987 
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

988 

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

989 
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

990 

31346  991 
definition 
992 
trivial_limit :: "'a net \<Rightarrow> bool" where 

31390  993 
"trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net" 
31346  994 

995 
lemma trivial_limit_within: 

996 
shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S" 

31390  997 
proof 
998 
assume "trivial_limit (at a within S)" 

999 
thus "\<not> a islimpt S" 

1000 
unfolding trivial_limit_def 

1001 
unfolding Rep_net_within Rep_net_at 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1002 
unfolding islimpt_def 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1003 
apply (clarsimp simp add: expand_set_eq) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1004 
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

1005 
apply (clarsimp, drule_tac x=y in spec, simp) 
31390  1006 
done 
1007 
next 

1008 
assume "\<not> a islimpt S" 

1009 
thus "trivial_limit (at a within S)" 

1010 
unfolding trivial_limit_def 

1011 
unfolding Rep_net_within Rep_net_at 

31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1012 
unfolding islimpt_def 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1013 
apply (clarsimp simp add: image_image) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1014 
apply (rule_tac x=T in image_eqI) 
31390  1015 
apply (auto simp add: expand_set_eq) 
1016 
done 

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

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

1018 

31391  1019 
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV" 
31346  1020 
using trivial_limit_within [of a UNIV] 
1021 
by (simp add: within_UNIV) 

1022 

31391  1023 
lemma trivial_limit_at: 
1024 
fixes a :: "'a::perfect_space" 

1025 
shows "\<not> trivial_limit (at a)" 

1026 
by (simp add: trivial_limit_at_iff) 

1027 

31346  1028 
lemma trivial_limit_at_infinity: 
1029 
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)" 

31391  1030 
(* FIXME: find a more appropriate type class *) 
31390  1031 
unfolding trivial_limit_def Rep_net_at_infinity 
1032 
apply (clarsimp simp add: expand_set_eq) 

1033 
apply (drule_tac x="scaleR r (sgn 1)" in spec) 

31587  1034 
apply (simp add: norm_sgn) 
31390  1035 
done 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1036 

31346  1037 
lemma trivial_limit_sequentially: "\<not> trivial_limit sequentially" 
31390  1038 
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

1039 

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

1040 
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

1041 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1042 
lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *) 
31390  1043 
"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

1044 
unfolding eventually_at dist_nz by auto 
31390  1045 

1046 
lemma eventually_at_infinity: 

1047 
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)" 

1048 
unfolding eventually_def Rep_net_at_infinity by auto 

1049 

31346  1050 
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

1051 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 
31393  1052 
unfolding eventually_within eventually_at dist_nz by auto 
31390  1053 

1054 
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow> 

1055 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs") 

1056 
unfolding eventually_within 

1057 
apply safe 

1058 
apply (rule_tac x="d/2" in exI, simp) 

1059 
apply (rule_tac x="d" in exI, simp) 

1060 
done 

1061 

1062 
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)" 

1063 
unfolding eventually_def trivial_limit_def 

1064 
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

1065 

31347
357d58c5743a
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
huffman
parents:
31346
diff
changeset

1066 
lemma always_eventually: "(\<forall>x. P x) ==> eventually P net" 
31390  1067 
unfolding eventually_def trivial_limit_def 
1068 
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

1069 

31348  1070 
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net" 
31390  1071 
unfolding trivial_limit_def eventually_def by auto 
1072 

1073 
lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 

1074 
unfolding trivial_limit_def eventually_def by auto 

31348  1075 

1076 
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)" 

31390  1077 
apply (safe elim!: trivial_limit_eventually) 
1078 
apply (simp add: eventually_False [symmetric]) 

1079 
done 

31348  1080 

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

1081 
text{* Combining theorems for "eventually" *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1082 

31390  1083 
lemma eventually_conjI: 
1084 
"\<lbrakk>eventually (\<lambda>x. P x) net; eventually (\<lambda>x. Q x) net\<rbrakk> 

1085 
\<Longrightarrow> eventually (\<lambda>x. P x \<and> Q x) net" 

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

1087 

31390  1088 
lemma eventually_rev_mono: 
1089 
"eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net" 

1090 
using eventually_mono [of P Q] by fast 

1091 

1092 
lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" 

1093 
by (auto intro!: eventually_conjI elim: eventually_rev_mono) 

1094 

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

1095 
lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 
31390  1096 
by (auto simp add: eventually_False) 
1097 

1098 
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)" 

1099 
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

1100 

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

1101 
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

1102 

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

1103 
text{* Notation Lim to avoid collition with lim defined in analysis *} 
31488  1104 
definition 
31654  1105 
Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where 
31488  1106 
"Lim net f = (THE l. (f > l) net)" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1107 

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

1109 
"(f > l) net \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1110 
trivial_limit net \<or> 
31348  1111 
(\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" 
31488  1112 
unfolding tendsto_iff 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

1113 

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

1114 

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

1115 
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

1116 

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

1117 
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

1118 
(\<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)" 
31488  1119 
by (auto simp add: tendsto_iff eventually_within_le) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1120 

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

1121 
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

1122 
(\<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)" 
31488  1123 
by (auto simp add: tendsto_iff eventually_within) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1124 

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

1125 
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

1126 
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 
31488  1127 
by (auto simp add: tendsto_iff eventually_at) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1128 

31342
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1129 
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

1130 
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

1131 

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

1132 
lemma Lim_at_infinity: 
31531  1133 
"(f > l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)" 
31488  1134 
by (auto simp add: tendsto_iff eventually_at_infinity) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1135 

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

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

1138 
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)" 
31488  1139 
by (auto simp add: tendsto_iff eventually_sequentially) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1140 

31342
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1141 
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

1142 
unfolding Lim_sequentially LIMSEQ_def .. 
b7941738e3a1
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ
huffman
parents:
31341
diff
changeset

1143 

31525  1144 
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f > l) net" 
1145 
by (rule topological_tendstoI, 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

1146 

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

1147 
text{* The expected monotonicity property. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1148 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1149 
lemma Lim_within_empty: "(f > l) (net within {})" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1150 
unfolding tendsto_def Limits.eventually_within by simp 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1151 

97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1152 
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

1153 
unfolding tendsto_def Limits.eventually_within 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1154 
by (auto elim!: eventually_elim1) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1155 

97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1156 
lemma Lim_Un: assumes "(f > l) (net within S)" "(f > l) (net within T)" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1157 
shows "(f > l) (net within (S \<union> T))" 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1158 
using assms unfolding tendsto_def Limits.eventually_within 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1159 
apply clarify 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1160 
apply (drule spec, drule (1) mp, drule (1) mp) 
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1161 
apply (drule spec, drule (1) mp, drule (1) mp) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1162 
apply (auto elim: eventually_elim2) 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

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

1164 

30488  1165 
lemma Lim_Un_univ: 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1166 
"(f > l) (net within S) \<Longrightarrow> (f > l) (net within T) \<Longrightarrow> S \<union> T = UNIV 
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1167 
==> (f > l) net" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1168 
by (metis Lim_Un within_UNIV) 
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{* Interrelations between restricted and unrestricted limits. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1171 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1172 
lemma Lim_at_within: "(f > l) net ==> (f > l)(net within S)" 
31525  1173 
(* FIXME: rename *) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1174 
unfolding tendsto_def Limits.eventually_within 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1175 
apply (clarify, drule spec, drule (1) mp, drule (1) mp) 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

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

1177 

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

1178 
lemma Lim_within_open: 
31525  1179 
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1180 
assumes"a \<in> S" "open S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1181 
shows "(f > l)(at a within S) \<longleftrightarrow> (f > l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1183 
assume ?lhs 
31525  1184 
{ fix A assume "open A" "l \<in> A" 
1185 
with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)" 

1186 
by (rule topological_tendstoD) 

1187 
hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)" 

31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1188 
unfolding Limits.eventually_within . 
31525  1189 
then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> f x \<in> A" 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

1190 
unfolding eventually_at_topological by fast 
31525  1191 
hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1192 
using assms by auto 
31525  1193 
hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)" 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1194 
by fast 
31525  1195 
hence "eventually (\<lambda>x. f x \<in> A) (at a)" 
31492
5400beeddb55
replace 'topo' with 'open'; add extra type constraint for 'open'
huffman
parents:
31490
diff
changeset

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

1197 
} 
31525  1198 
thus ?rhs by (rule topological_tendstoI) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1200 
assume ?rhs 
31447
97bab1ac463e
generalize type of 'at' to topological_space; generalize some lemmas
huffman
parents:
31445
diff
changeset

1201 
thus ?lhs by (rule Lim_at_within) 
30262
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1203 

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

1204 
text{* Another limit point characterization. *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1205 

30488  1206 
lemma islimpt_sequential: 
31488  1207 
fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *) 
1208 
shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S {x}) \<and> (f > x) sequentially)" 

1209 
(is "?lhs = ?rhs") 

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

1210 
proof 
5794fee816c3
A fo 