equal
deleted
inserted
replaced
1090 then have "dist x1 x4 < (e/3 + e/3) + e/3" |
1090 then have "dist x1 x4 < (e/3 + e/3) + e/3" |
1091 by (metis assms(3) dist_commute dist_triangle_less_add) |
1091 by (metis assms(3) dist_commute dist_triangle_less_add) |
1092 then show ?thesis |
1092 then show ?thesis |
1093 by simp |
1093 by simp |
1094 qed |
1094 qed |
1095 |
1095 |
1096 subclass uniform_space |
1096 subclass uniform_space |
1097 proof |
1097 proof |
1098 fix E x |
1098 fix E x |
1099 assume "eventually E uniformity" |
1099 assume "eventually E uniformity" |
1100 then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)" |
1100 then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)" |