equal
deleted
inserted
replaced
30 lemma open_discrete: "open (S :: 'a discrete set)" |
30 lemma open_discrete: "open (S :: 'a discrete set)" |
31 unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"]) |
31 unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"]) |
32 |
32 |
33 instance discrete :: (type) complete_space |
33 instance discrete :: (type) complete_space |
34 proof |
34 proof |
35 fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X" |
35 fix X::"nat\<Rightarrow>'a discrete" |
36 hence "\<exists>n. \<forall>m\<ge>n. X n = X m" |
36 assume "Cauchy X" |
|
37 then obtain n where "\<forall>m\<ge>n. X n = X m" |
37 by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1]) |
38 by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1]) |
38 then guess n .. |
|
39 thus "convergent X" |
39 thus "convergent X" |
40 by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n]) |
40 by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n]) |
41 (simp add: dist_discrete_def) |
41 (simp add: dist_discrete_def) |
42 qed |
42 qed |
43 |
43 |