equal
deleted
inserted
replaced
17 |
17 |
18 definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real" |
18 definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real" |
19 where "dist_discrete n m = (if n = m then 0 else 1)" |
19 where "dist_discrete n m = (if n = m then 0 else 1)" |
20 |
20 |
21 definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where |
21 definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where |
22 "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" |
22 "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})" |
23 |
23 |
24 definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where |
24 definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where |
25 "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)" |
25 "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)" |
26 |
26 |
27 instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1]) |
27 instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1]) |