equal
deleted
inserted
replaced
186 the Injection from @{typ real} to @{typ hypreal}*} |
186 the Injection from @{typ real} to @{typ hypreal}*} |
187 |
187 |
188 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
188 lemma inj_hypreal_of_real: "inj(hypreal_of_real)" |
189 by (rule inj_onI, simp) |
189 by (rule inj_onI, simp) |
190 |
190 |
|
191 lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)" |
|
192 by (cases x, simp add: star_n_def) |
|
193 |
191 lemma Rep_star_star_n_iff [simp]: |
194 lemma Rep_star_star_n_iff [simp]: |
192 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
195 "(X \<in> Rep_star (star_n Y)) = ({n. Y n = X n} \<in> \<U>)" |
193 by (simp add: star_n_def) |
196 by (simp add: star_n_def) |
194 |
197 |
195 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |
198 lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)" |