src/HOL/Library/Formal_Power_Series.thy
changeset 62101 26c0a70f78a3
parent 61969 e01015e49041
child 62102 877463945ce9
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -815,13 +815,14 @@
     1.4  instantiation fps :: (comm_ring_1) metric_space
     1.5  begin
     1.6  
     1.7 -definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
     1.8 -
     1.9 +definition uniformity_fps_def [code del]:
    1.10 +  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    1.11 +
    1.12 +definition open_fps_def' [code del]:
    1.13 +  "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
    1.14  
    1.15  instance
    1.16  proof
    1.17 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" for S :: "'a fps set"
    1.18 -    by (auto simp add: open_fps_def ball_def subset_eq)
    1.19    show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
    1.20      by (simp add: dist_fps_def split: split_if_asm)
    1.21    then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
    1.22 @@ -853,10 +854,12 @@
    1.23      qed
    1.24      thus ?thesis by (auto simp add: not_le[symmetric])
    1.25    qed
    1.26 -qed
    1.27 +qed (rule open_fps_def' uniformity_fps_def)+
    1.28  
    1.29  end
    1.30  
    1.31 +lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
    1.32 +  unfolding open_dist ball_def subset_eq by simp
    1.33  
    1.34  text \<open>The infinite sums and justification of the notation in textbooks.\<close>
    1.35