equal
deleted
inserted
replaced
137 |
137 |
138 |
138 |
139 subsection{*@{term preal_of_prat}: the Injection from prat to preal*} |
139 subsection{*@{term preal_of_prat}: the Injection from prat to preal*} |
140 |
140 |
141 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal" |
141 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal" |
142 apply (auto simp add: preal_def cut_def intro: order_less_trans) |
142 apply (auto simp del: empty_Collect_eq simp add: preal_def cut_def intro: order_less_trans) |
143 apply (force simp only: eq_commute [of "{}"] interval_empty_iff) |
143 apply (force simp only: eq_commute [of "{}"] interval_empty_iff) |
144 apply (blast dest: dense intro: order_less_trans) |
144 apply (blast dest: dense intro: order_less_trans) |
145 done |
145 done |
146 |
146 |
147 lemma rat_subset_imp_le: |
147 lemma rat_subset_imp_le: |