author  chaieb 
Wed, 04 Mar 2009 19:21:56 +0000  
changeset 30262  5794fee816c3 
child 30267  171b3bd93c90 
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 
ID: $Id: 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

4 
Robert Himmelmann, TU Muenchen*) 
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 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

9 
imports SEQ Euclidean_Space 
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 

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

13 
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

14 

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

15 
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

16 

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

17 
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)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

18 
typedef (open) 'a topology = "{L::('a set) set. istopology L}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

21 

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

22 
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

23 
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

24 

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

25 
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

26 
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

27 

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

28 
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

29 
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

30 

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

31 
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

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

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

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

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

36 
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

37 
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

38 
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

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

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

41 

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

42 
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

43 

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

44 
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

45 

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

46 
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

47 

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

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

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

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

51 
"\<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

52 
"\<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

53 
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

54 
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

55 

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

56 
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

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

58 
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

59 

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

60 
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

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

62 

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

63 
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

64 

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

65 
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

66 
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

67 

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

68 
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

69 

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

70 
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

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

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

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

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

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

76 
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

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

78 
have "\<Union> t`S = S" using t by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

79 
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

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

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

82 

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

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

84 

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

85 
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

86 

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

87 
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

88 
lemma closedin_empty[simp]: "closedin 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

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

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

91 
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

92 
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

93 

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

94 
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

95 
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

96 
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

97 

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

98 
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

99 
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

100 

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

101 
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

102 
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

103 
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

104 
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

105 
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

106 
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

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

108 

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

109 
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

110 
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

111 

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

112 
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

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

114 
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

115 
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

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

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

118 

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

119 
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

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

121 
have "S  T = S \<inter> (topspace U  T)" using closedin_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

122 
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

123 
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

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

125 

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

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

127 

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

128 
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

129 

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

130 
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

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

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

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

134 
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

135 
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

136 
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

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

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

139 
have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U " 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

143 
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

144 
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

145 
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

146 
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

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

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

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

150 

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

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

152 
"openin (subtopology U V) S \<longleftrightarrow> (\<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

153 
unfolding subtopology_def topology_inverse'[OF istopology_subtopology] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

155 

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

156 
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

157 
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

158 

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

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

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

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

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

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

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

165 
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

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

167 

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

168 
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

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

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

171 
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

172 
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

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

174 

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

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

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

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

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

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

180 
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

181 
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

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

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

184 
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

185 
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

186 
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

187 
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

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

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

191 
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

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

193 

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

194 
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

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

196 

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

197 
subsection{* The universal Euclidean versions are what we use most of the time *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

198 
definition "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>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

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

200 
definition "euclidean = topology open" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

201 

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

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

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

204 
by (simp add: open_def, rule exI[where x="1"], auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

205 

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

206 
lemma open_inter[intro]: assumes S: "open S" and T: "open T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

209 
note thS = S[unfolded open_def, rule_format] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

210 
note thT = T[unfolded open_def, rule_format] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

212 
hence xS: "x \<in> S" and xT: "x \<in> T" by simp_all 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

213 
from thS[OF xS] obtain eS where eS: "eS > 0" "\<forall>x'. dist x' x < eS \<longrightarrow> x' \<in> S" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

214 
from thT[OF xT] obtain eT where eT: "eT > 0" "\<forall>x'. dist x' x < eT \<longrightarrow> x' \<in> T" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

215 
from real_lbound_gt_zero[OF eS(1) eT(1)] obtain e where e: "e > 0" "e < eS" "e < eT" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

216 
{ fix x' assume d: "dist x' x < e" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

217 
hence dS: "dist x' x < eS" and dT: "dist x' x < eT" using e by arith+ 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

218 
from eS(2)[rule_format, OF dS] eT(2)[rule_format, OF dT] have "x' \<in> S\<inter>T" by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

219 
hence "\<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> (S\<inter>T)" using e by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

221 
qed 
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 
lemma open_Union[intro]: "(\<forall>S\<in>K. open S) \<Longrightarrow> open (\<Union> K)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

225 

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

226 
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

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

228 
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

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

230 
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

231 
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

232 

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

233 
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

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

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

236 
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

237 

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

238 
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

239 
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

240 

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

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

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

243 

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

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

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

246 

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

247 
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

248 
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

249 

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

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

251 

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

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

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

254 

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

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

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

257 

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

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

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

260 

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

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

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

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

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

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

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

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

268 

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

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

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

271 

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

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

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

274 

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

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

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

277 

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

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

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

280 

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

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

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

283 

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

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

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

286 

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

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

288 

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

289 
definition "ball x e = {y. dist x y < e}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

290 
definition "cball x e = {y. dist x y \<le> e}" 
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 mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

294 
lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

296 
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

297 
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

298 
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

299 
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

300 
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

301 
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

302 

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

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

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

305 

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

306 
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

307 

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

308 
lemma diff_less_iff: "(a::real)  b > 0 \<longleftrightarrow> a > b" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

309 
"(a::real)  b < 0 \<longleftrightarrow> a < b" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

313 

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

314 
lemma open_ball[intro, simp]: "open (ball x e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

318 
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

319 
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

320 
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

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

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

323 
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

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

325 

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

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

327 
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<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

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

329 

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

330 
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

331 
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

332 

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

333 
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

334 
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

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

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

337 

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

338 
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

339 

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

340 
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

341 

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

342 
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

343 
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

344 

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

345 
lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (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

346 
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

347 

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

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

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

350 
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

351 

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

352 
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

353 
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

354 

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

355 
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

356 
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

357 

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

358 
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

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

360 

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

361 
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

362 
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

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

364 
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

365 
by simp 
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 
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

368 
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

369 

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

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

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

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

373 
{assume ?lhs hence ?rhs unfolding openin_subtopology open_openin[symmetric] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

377 
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

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

379 
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

380 
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

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

382 
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

383 
apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

384 
unfolding dist_refl using d[of x] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

385 
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

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

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

388 
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

389 
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

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

391 
hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_sym) } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

392 
ultimately have "S = ?T \<inter> U" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

393 
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

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

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

396 

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

397 
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

398 

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

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

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

401 
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

402 

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

403 
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

404 
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

405 

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

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

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

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

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

410 
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

411 

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

412 
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

413 
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

414 

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

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

416 

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

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

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

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

420 

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

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

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

423 
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

424 
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

425 
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

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

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

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

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

430 

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

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

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

433 

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

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

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

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

437 
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

438 
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

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

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

441 

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

442 
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

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

444 
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

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

446 
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> {})" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

449 
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> {})" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

451 

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

452 
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

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

454 
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

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

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

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

458 
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

459 
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

460 
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

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

462 

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

463 
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

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

465 

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

466 
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

467 

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

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

469 
assumes xy: "x \<noteq> y" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

470 
shows "\<exists>U V. open U \<and> open V \<and> x\<in> U \<and> y \<in> V \<and> (U \<inter> V = {})" (is "\<exists>U V. ?P U V") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

472 
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

473 
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

474 
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

475 
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

476 
have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

477 
by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

480 

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

481 
lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

483 

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

484 
lemma separation_t1: "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)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

486 

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

487 
lemma separation_t0: "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))" by(metis separation_t1) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

488 

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

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

490 

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

491 
definition islimpt:: "real ^'n \<Rightarrow> (real^'n) set \<Rightarrow> bool" (infixr "islimpt" 60) where 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

493 

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

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

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

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

497 
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

498 

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

499 
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T ==> x islimpt T" by (auto simp add: islimpt_def) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

500 
lemma islimpt_approachable: "x islimpt S \<longleftrightarrow> (\<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

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

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

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

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

505 
apply(rule_tac x=y in bexI) apply (auto simp add: dist_sym) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

507 

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

508 
lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<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

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

510 
using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

512 

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

513 
lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n) islimpt UNIV" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

517 
from vector_choose_size[of "e/2"] ep have "\<exists>(c:: real ^'n). norm c = e/2" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

518 
then obtain c ::"real^'n" where c: "norm c = e/2" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

519 
let ?x = "x + c" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

520 
have "?x \<noteq> x" using c ep by (auto simp add: norm_eq_0_imp) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

521 
moreover have "dist ?x x < e" using c ep apply simp by norm 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

522 
ultimately have "\<exists>x'. x' \<noteq> x\<and> dist x' x < e" by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

523 
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

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

525 

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

526 
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

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

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

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

530 
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

531 

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

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

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

534 

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

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

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

537 
let ?U = "{1 .. dimindex(UNIV :: 'n set)}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

538 
let ?O = "{x::real^'n. \<forall>i\<in>?U. x$i\<ge>0}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

539 
{fix x:: "real^'n" and i::nat assume H: "\<forall>e>0. \<exists>x'\<in>?O. x' \<noteq> x \<and> dist x' x < e" and i: "i \<in> ?U" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

541 
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

542 
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

543 
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

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

545 
have th1: "\<bar>x$i\<bar> \<le> \<bar>(x'  x)$i\<bar>" using i x'(1) xi 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

548 
have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x'  x)$i\<bar>" using component_le_norm[OF i, of "x'x"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

550 
from th[OF th1 th2] x'(3) have False by (simp add: dist_sym dist_pos_le) } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

552 
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

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 finite_set_avoid: assumes fS: "finite S" shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

556 
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

557 
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

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

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

560 
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

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

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

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

564 
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

565 
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

566 
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

567 
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

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

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

570 

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

571 
lemma islimpt_finite: assumes fS: "finite S" shows "\<not> a islimpt S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

574 

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

575 
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

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

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

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

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

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

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

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

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

584 

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

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

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

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

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

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

590 
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

591 
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

592 
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

593 
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

594 
from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

595 
have th: "norm (z  y) < e" using z y by norm 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

596 
from d[rule_format, OF y(1) z(1) th] y z 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

600 

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

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

602 
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

603 

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

604 
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

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

606 
apply (subst (2) open_subopen) by blast 
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 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

609 

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

610 
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

611 

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

612 
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

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

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

615 

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

616 
lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

617 
lemma interior_subset: "interior S \<subseteq> 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

618 
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

619 
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

620 
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

621 
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

622 
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

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

624 
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

625 

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

626 
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

627 
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

628 

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

629 
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

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

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

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

633 

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

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

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

636 
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

637 
unfolding mem_interior subset_eq Ball_def mem_ball by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

640 
have mde2: "?m \<ge> 0" using e(1) d(1) by arith 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

641 
from vector_choose_dist[OF mde2, of x] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

642 
obtain y where y: "dist x y = ?m" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

643 
have th: "dist x y < e" "dist x y < d" unfolding y using e(1) d(1) by arith+ 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

644 
have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

646 
using e th y by (auto simp add: dist_sym)} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

647 
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

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

649 

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

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

651 
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

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

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

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

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

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

657 
{fix x e assume e: "e > 0" "\<forall>x' \<in> ball x e. x'\<in>(S\<union>T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

661 
have kp: "?k > 0" using d e(1) y[unfolded mem_ball] by norm 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

662 
have "?k/2 \<ge> 0" using kp by simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

663 
then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

664 
from iT[unfolded expand_set_eq mem_interior] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

665 
have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

666 
then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

667 
have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

668 
using w e(1) d apply (auto simp only: dist_sym) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

670 
apply (cases "d \<le> e  dist x y", auto simp add: ring_simps cong del: if_weak_cong) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

672 
apply (cases "d \<le> e  dist x y", auto simp add: ring_simps not_le not_less cong del: if_weak_cong) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

675 
apply (cases "d \<le> e  dist x y", auto simp add: ring_simps not_le not_less cong del: if_weak_cong) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

679 
then have "\<exists>z. z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

680 
then have "\<exists>x' \<in>S. x'\<noteq>y \<and> dist x' y < d" using e by auto} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

681 
then have "y\<in>S" by (metis islimpt_approachable cS closed_limpt) } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

682 
then have "x \<in> interior S" unfolding mem_interior using e(1) by blast} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

683 
hence "interior (S\<union>T) \<subseteq> interior S" unfolding mem_interior Ball_def subset_eq by blast 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

686 

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

687 

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

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

689 

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

690 
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

691 

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

692 
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

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

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

695 
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

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

697 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

711 
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

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

713 
qed 
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 
thus ?thesis 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

729 

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

730 
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

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

732 
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

733 
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

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

735 

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

736 
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

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

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

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

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

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

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

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

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

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

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

747 
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

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

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

750 
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

751 
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

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

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

754 
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

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

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

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

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

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

760 
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

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

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

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

764 

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

765 
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

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

767 
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

768 
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

769 

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

770 
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

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

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

773 

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

774 
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

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

776 
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

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

778 

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

779 
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

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

781 
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

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

783 

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

784 
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

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

786 
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

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

788 

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

789 
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

790 
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

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

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

793 

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

794 
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

795 
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

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

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

798 

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

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

800 
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

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

802 

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

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

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

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

806 

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

807 
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

808 
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

809 
by blast 
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 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

812 
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

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

814 

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

815 
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

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

817 
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

818 
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

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

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

821 

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

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

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

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

825 
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

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

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

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

829 
from as `open S` obtain e' where "e' > 0" and e':"\<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

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

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

832 
let ?e = "min e e'" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

833 
from `e>0` `e'>0` have "?e > 0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

835 
then obtain y where y:"y\<in>T" "y \<noteq> x \<and> dist y x < ?e" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

836 
using islimpt_approachable[of x T] using * 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

838 
hence "\<exists>x'\<in>S \<inter> T. x' \<noteq> x \<and> dist x' x < e" using e' 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

840 
by(rule_tac x=y in bexI, simp+) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

842 
hence "x islimpt S \<inter> T" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

843 
using islimpt_approachable[of x "S \<inter> T"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

846 
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

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

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

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

850 

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

851 
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

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

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

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

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

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

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

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

859 

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

860 
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

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

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

863 

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

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

865 

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

866 
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

867 

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

868 
lemma frontier_closed: "closed(frontier S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

870 

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

871 
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

872 
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

873 

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

874 
lemma frontier_straddle: "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") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

879 
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

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

881 
have "\<exists>x\<in>S. dist a x < e" using dist_refl[of a] `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

882 
moreover have "\<exists>x. x \<notin> S \<and> dist a x < e" using `?lhs` `a\<in>S` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

883 
unfolding frontier_closures closure_def islimpt_def using dist_refl[of a] `e>0` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

884 
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

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

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

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

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

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

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

891 
using open_ball[of a e] dist_refl[of a] `e > 0` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

892 
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

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

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

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

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

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

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

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

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

901 
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

902 
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

903 
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

904 
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

905 
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

906 
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

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

908 
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

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

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

911 
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

912 
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

913 
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

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

915 
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

916 
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

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

918 

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

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

920 
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

921 

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

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

923 
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

924 

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

925 
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

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

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

928 
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

929 
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

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

931 
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

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

933 

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

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

935 
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

936 

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

937 
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

940 

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

941 
subsection{* A variant of nets (Slightly nonstandard but good for our purposes). *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

942 

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

943 
typedef (open) 'a net = 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

944 
"{g :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>x y. (\<forall>z. g z x \<longrightarrow> g z y) \<or> (\<forall>z. g z y \<longrightarrow> g z x)}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

946 
lemma net: "(\<forall>z. netord n z x \<longrightarrow> netord n z y) \<or> (\<forall>z. netord n z y \<longrightarrow> netord n z x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

947 
using netord[of n] by auto 
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 oldnet: "netord n x x \<Longrightarrow> netord n y y \<Longrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

950 
\<exists>z. netord n z z \<and> (\<forall>w. netord n w z \<longrightarrow> netord n w x \<and> netord n w y)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

952 

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

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

954 
"\<exists>a. (\<exists>x. netord net x a) \<and> (\<forall>x. netord net x a \<longrightarrow> P x) \<Longrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

955 
\<exists>b. (\<exists>x. netord net x b) \<and> (\<forall>x. netord net x b \<longrightarrow> Q x) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

956 
\<Longrightarrow> \<exists>c. (\<exists>x. netord net x c) \<and> (\<forall>x. netord net x c \<longrightarrow> P x \<and> Q x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

958 

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

959 
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

960 

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

961 
definition "at a = mknet(\<lambda>x y. 0 < dist x a \<and> dist x a <= dist y a)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

962 
definition "at_infinity = mknet(\<lambda>x y. norm x \<ge> norm y)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

963 
definition "sequentially = mknet(\<lambda>(m::nat) n. m >= n)" 
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 
definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

966 
within_def: "net within S = mknet (\<lambda>x y. netord net x y \<and> x \<in> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

967 

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

968 
definition indirection :: "real ^'n \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

969 
indirection_def: "a indirection v = (at a) within {b. \<exists>c\<ge>0. b  a = c*s v}" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

970 

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

971 
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

972 

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

973 
lemma mknet_inverse': "netord (mknet r) = r \<longleftrightarrow> (\<forall>x y. (\<forall>z. r z x \<longrightarrow> r z y) \<or> (\<forall>z. r z y \<longrightarrow> r z x))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

974 
using mknet_inverse[of r] apply (auto simp add: netord_inverse) by (metis net) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

975 

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

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

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

978 
val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

979 
val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

980 
fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

981 
in Method.thms_args (Method.SIMPLE_METHOD' o tac) end 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

982 

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

983 
*} "Reduces goals about net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

984 

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

985 
lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

987 
by (metis dist_sym real_le_linear real_le_trans) 
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 
lemma at_infinity: 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

990 
"\<And>x y. netord at_infinity x y \<longleftrightarrow> norm x >= norm y" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

994 

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

995 
lemma sequentially: "\<And>m n. netord sequentially m n \<longleftrightarrow> m >= n" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

997 
apply (metis linorder_linear min_max.le_supI2 min_max.sup_absorb1) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

999 

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

1000 
lemma within: "netord (n within S) x y \<longleftrightarrow> netord n x y \<and> x \<in> S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1002 
have "\<forall>x y. (\<forall>z. netord n z x \<and> z \<in> S \<longrightarrow> netord n z y) \<or> (\<forall>z. netord n z y \<and> z \<in> S \<longrightarrow> netord n z x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

1006 
using mknet_inverse[of "\<lambda>x y. netord n x y \<and> x \<in> S"] 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1009 

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

1010 
lemma in_direction: "netord (a indirection v) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a \<le> dist y a \<and> (\<exists>c \<ge> 0. x  a = c *s v)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1012 

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

1013 
lemma within_UNIV: "at x within UNIV = at x" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1015 

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

1016 
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

1017 

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

1018 

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

1019 
definition "trivial_limit (net:: 'a net) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1020 
(\<forall>(a::'a) b. a = b) \<or> (\<exists>(a::'a) b. a \<noteq> b \<and> (\<forall>x. ~(netord (net) x a) \<and> ~(netord(net) x b)))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1021 

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

1022 

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

1023 
lemma trivial_limit_within: "trivial_limit (at (a::real^'n) within S) \<longleftrightarrow> ~(a islimpt S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1025 
{assume "\<forall>(a::real^'n) b. a = b" hence "\<not> a islimpt S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1027 
by (rule exI[where x=1], auto)} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1029 
{fix b c assume bc: "b \<noteq> c" "\<forall>x. \<not> netord (at a within S) x b \<and> \<not> netord (at a within S) x c" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1030 
have "dist a b > 0 \<or> dist a c > 0" using bc by (auto simp add: within at dist_nz[THEN sym]) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1031 
then have "\<not> a islimpt S" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1034 
by(auto simp add: dist_triangle dist_sym dist_eq_0[THEN sym]) } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

1039 
from e vector_choose_dist[of e a] obtain b where b: "dist a b = e" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1040 
from b e(1) have "a \<noteq> b" by (simp add: dist_nz) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1041 
moreover have "\<forall>x. \<not> ((0 < dist x a \<and> dist x a \<le> dist a a) \<and> x \<in> S) \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1042 
\<not> ((0 < dist x a \<and> dist x a \<le> dist b a) \<and> x \<in> S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1043 
using e(2) b by (auto simp add: dist_refl dist_sym) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1044 
ultimately have "trivial_limit (at a within S)" unfolding trivial_limit_def within at 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

1048 

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

1049 
lemma trivial_limit_at: "~(trivial_limit (at a))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1052 

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

1053 
lemma trivial_limit_at_infinity: "~(trivial_limit (at_infinity :: ('a::{norm,zero_neq_one}) net))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1056 

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

1057 
lemma trivial_limit_sequentially: "~(trivial_limit sequentially)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1059 

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

1060 
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

1061 

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

1062 
definition "eventually P net \<longleftrightarrow> trivial_limit net \<or> (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> P x))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1063 

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

1064 
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1066 

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

1067 
lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1068 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

1073 
then obtain e where "e>0" and e:"\<forall>x'\<in>S. \<not> (x' \<noteq> a \<and> dist x' a \<le> e)" unfolding islimpt_approachable_le by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1074 
hence "?rhs" apply auto apply (rule_tac x=e in exI) by auto } 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1076 
{ assume "\<exists>y. (\<exists>x. netord (at a within S) x y) \<and> (\<forall>x. netord (at a within S) x y \<longrightarrow> P x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1077 
then obtain x y where xy:"netord (at a within S) x y \<and> (\<forall>x. netord (at a within S) x y \<longrightarrow> P x)" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1078 
hence "?rhs" unfolding within at by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1080 
ultimately show "?rhs" unfolding eventually_def trivial_limit_within by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1083 
then obtain d where "d>0" and d:"\<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> P x" by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1085 
unfolding eventually_def trivial_limit_within islimpt_approachable_le within at unfolding dist_nz[THEN sym] by (clarsimp, rule_tac x=d in exI, auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1087 

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

1088 
lemma eventually_within: " eventually P (at a within S) \<longleftrightarrow> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1089 
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1092 
assume "d>0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1093 
hence "\<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> (d/2) \<longrightarrow> P x" using order_less_imp_le by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1096 
by (auto, rule_tac x="d/2" in exI, auto) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1098 

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

1099 
lemma eventually_at: "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1101 
by (simp add: eventually_within) 
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 
lemma eventually_sequentially: "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1105 
apply (metis dlo_simps(7) dlo_simps(9) le_maxI2 min_max.le_iff_sup min_max.sup_absorb1 order_antisym_conv) done 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1106 

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

1107 
(* FIXME Declare this with P::'a::some_type \<Rightarrow> bool *) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1108 
lemma eventually_at_infinity: "eventually (P::(real^'n \<Rightarrow> bool)) at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)" (is "?lhs = ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

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

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

1115 
then obtain b where b:"\<forall>x. b \<le> norm x \<longrightarrow> P x" and "b\<ge>0" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1117 
obtain y::"real^'n" where y:"norm y = b" using `b\<ge>0` 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1118 
using vector_choose_size[of b] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1119 
thus "?lhs" unfolding eventually_def at_infinity using b y by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1121 

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

1122 
lemma always_eventually: "(\<forall>(x::'a::zero_neq_one). P x) ==> eventually P net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1124 
by (rule exI[where x=0], rule exI[where x=1], rule zero_neq_one) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1125 

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

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

1127 

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

1128 
lemma eventually_and: " eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1131 
using net_dilemma[of net P Q] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1132 

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

1133 
lemma eventually_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1135 

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

1136 
lemma eventually_mp: "eventually (\<lambda>x. P x \<longrightarrow> Q x) net \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

1140 

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

1141 
lemma eventually_false: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1143 

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

1144 
lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually P net)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1145 
by (auto simp add: eventually_def) 
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 
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

1148 

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

1149 
definition tendsto:: "('a \<Rightarrow> real ^'n) \<Rightarrow> real ^'n \<Rightarrow> 'a net \<Rightarrow> bool" (infixr ">" 55) where 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1150 
tendsto_def: "(f > l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1151 

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

1152 
lemma tendstoD: "(f > l) net \<Longrightarrow> e>0 \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1154 

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

1155 
text{* Notation Lim to avoid collition with lim defined in analysis *} 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1157 

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

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

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

1160 
trivial_limit net \<or> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1161 
(\<forall>e>0. \<exists>y. (\<exists>x. netord net x y) \<and> 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1162 
(\<forall>x. netord(net) x y \<longrightarrow> dist (f x) l < e))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1164 

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

1165 

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

1166 
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

1167 

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

1168 
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

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

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

1171 

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

1172 
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

1173 
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1175 

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

1176 
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

1177 
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1179 

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

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

1181 
"(f > l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n. norm x >= b \<longrightarrow> dist (f x) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1183 

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

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

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

1186 
(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1188 

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

1189 
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f > l) net" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1191 

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

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

1193 

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

1194 
lemma Lim_within_empty: "(f > l) (at x within {})" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1196 

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

1197 
lemma Lim_within_subset: "(f > l) (at a within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f > l) (at a within T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1200 

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

1201 
lemma Lim_Un: assumes "(f > l) (at x within S)" "(f > l) (at x within T)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1202 
shows "(f > l) (at x within (S \<union> T))" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1205 
obtain d1 where d1:"d1>0" "\<forall>xa\<in>T. 0 < dist xa x \<and> dist xa x < d1 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1206 
obtain d2 where d2:"d2>0" "\<forall>xa\<in>S. 0 < dist xa x \<and> dist xa x < d2 \<longrightarrow> dist (f xa) l < e" using assms unfolding Lim_within using `e>0` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1207 
have "\<exists>d>0. \<forall>xa\<in>S \<union> T. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) l < e" using d1 d2 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1208 
by (rule_tac x="min d1 d2" in exI)auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

1212 

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

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

1214 
"(f > l) (at x within S) \<Longrightarrow> (f > l) (at x within T) \<Longrightarrow> S \<union> T = (UNIV::(real^'n) set) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1216 
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

1217 

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

1218 
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

1219 

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

1220 
lemma Lim_at_within: "(f > l)(at a) ==> (f > l)(at a within S)" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1223 

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

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

1225 
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

1226 
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

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

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

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

1230 
obtain d where d: "d >0" "\<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?lhs` `e>0` unfolding Lim_within by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1231 
obtain d' where d': "d'>0" "\<forall>x. dist x a < d' \<longrightarrow> x \<in> S" using assms unfolding open_def by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1232 
from d d' have "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" by (rule_tac x= "min d d'" in exI)auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

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

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

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

1238 
then obtain d where "d>0" and d:"\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `?rhs` unfolding Lim_at by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1239 
hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using `d>0` by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1241 
thus ?lhs using Lim_at_within[of f l a S] by (auto simp add: Lim_at) 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1243 

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

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

1245 

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

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

1247 
"x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S {x}) \<and> (f > x) sequentially)" (is "?lhs = ?rhs") 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1250 
then obtain f where f:"\<forall>y. y>0 \<longrightarrow> f y \<in> S \<and> f y \<noteq> x \<and> dist (f y) x < y" 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

1251 
unfolding islimpt_approachable using choice[of "\<lambda>e y. e>0 \<longrightarrow> y\<in>S \<and> y\<noteq>x \<and> dist y x < e"] by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

1253 
have "f (inverse (real n + 1)) \<in> S  {x}" using f by auto 
5794fee816c3
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb
parents:
diff
changeset

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

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

1256 
{ fix e::real assume "e>0" 