equal
deleted
inserted
replaced
181 done |
181 done |
182 |
182 |
183 lemma set_of_subset_iff: "set_of X \<subseteq> set_of Y \<longleftrightarrow> lower Y \<le> lower X \<and> upper X \<le> upper Y" |
183 lemma set_of_subset_iff: "set_of X \<subseteq> set_of Y \<longleftrightarrow> lower Y \<le> lower X \<and> upper X \<le> upper Y" |
184 for X Y::"'a::linorder interval" |
184 for X Y::"'a::linorder interval" |
185 by (auto simp: set_of_eq subset_iff) |
185 by (auto simp: set_of_eq subset_iff) |
|
186 |
|
187 lemma set_of_subset_iff': |
|
188 "set_of a \<subseteq> set_of (b :: 'a :: linorder interval) \<longleftrightarrow> a \<le> b" |
|
189 unfolding less_eq_interval_def set_of_subset_iff .. |
186 |
190 |
187 lemma bounds_of_interval_eq_lower_upper: |
191 lemma bounds_of_interval_eq_lower_upper: |
188 "bounds_of_interval ivl = (lower ivl, upper ivl)" if "lower ivl \<le> upper ivl" |
192 "bounds_of_interval ivl = (lower ivl, upper ivl)" if "lower ivl \<le> upper ivl" |
189 using that |
193 using that |
190 by (auto simp: lower.rep_eq upper.rep_eq) |
194 by (auto simp: lower.rep_eq upper.rep_eq) |