equal
deleted
inserted
replaced
1190 by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) |
1190 by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) |
1191 |
1191 |
1192 |
1192 |
1193 subsection \<open>Rationals\<close> |
1193 subsection \<open>Rationals\<close> |
1194 |
1194 |
|
1195 lemma Rats_abs_iff[simp]: |
|
1196 "\<bar>(x::real)\<bar> \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>" |
|
1197 by(simp add: abs_real_def split: if_splits) |
|
1198 |
1195 lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}" (is "_ = ?S") |
1199 lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}" (is "_ = ?S") |
1196 proof |
1200 proof |
1197 show "\<rat> \<subseteq> ?S" |
1201 show "\<rat> \<subseteq> ?S" |
1198 proof |
1202 proof |
1199 fix x :: real |
1203 fix x :: real |