equal
deleted
inserted
replaced
107 qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+ |
107 qed (meson assms compact_imp_closed seq_compact_closed_subset seq_compact_eq_compact)+ |
108 |
108 |
109 |
109 |
110 subsection\<open>Arcwise Connections\<close> |
110 subsection\<open>Arcwise Connections\<close> |
111 |
111 |
112 subsection\<open>Density of points with dyadic rational coordinates.\<close> |
112 subsection\<open>Density of points with dyadic rational coordinates\<close> |
113 |
113 |
114 proposition closure_dyadic_rationals: |
114 proposition closure_dyadic_rationals: |
115 "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. |
115 "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>. |
116 { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV" |
116 { \<Sum>i :: 'a :: euclidean_space \<in> Basis. (f i / 2^k) *\<^sub>R i }) = UNIV" |
117 proof - |
117 proof - |