equal
deleted
inserted
replaced
87 |
87 |
88 lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}" |
88 lemma bdd_below_Ici [simp, intro]: "bdd_below {a ..}" |
89 by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) |
89 by (auto simp add: bdd_below_def intro: exI[of _ a] less_imp_le) |
90 |
90 |
91 end |
91 end |
|
92 |
|
93 lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A" |
|
94 by (rule bdd_aboveI[of _ top]) simp |
|
95 |
|
96 lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A" |
|
97 by (rule bdd_belowI[of _ bot]) simp |
92 |
98 |
93 context lattice |
99 context lattice |
94 begin |
100 begin |
95 |
101 |
96 lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A" |
102 lemma bdd_above_insert [simp]: "bdd_above (insert a A) = bdd_above A" |
267 lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u" |
273 lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u" |
268 by (auto intro: cINF_lower assms order_trans) |
274 by (auto intro: cINF_lower assms order_trans) |
269 |
275 |
270 lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f" |
276 lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f" |
271 by (auto intro: cSUP_upper assms order_trans) |
277 by (auto intro: cSUP_upper assms order_trans) |
|
278 |
|
279 lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c" |
|
280 by (intro antisym cSUP_least) (auto intro: cSUP_upper) |
|
281 |
|
282 lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c" |
|
283 by (intro antisym cINF_greatest) (auto intro: cINF_lower) |
272 |
284 |
273 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)" |
285 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)" |
274 by (metis cINF_greatest cINF_lower assms order_trans) |
286 by (metis cINF_greatest cINF_lower assms order_trans) |
275 |
287 |
276 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" |
288 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)" |