482 assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
482 assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)" |
483 begin |
483 begin |
484 |
484 |
485 lemma sup_INF: |
485 lemma sup_INF: |
486 "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" |
486 "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)" |
487 unfolding sup_Inf by simp |
487 by (simp add: sup_Inf) |
488 |
488 |
489 lemma inf_SUP: |
489 lemma inf_SUP: |
490 "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" |
490 "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)" |
491 unfolding inf_Sup by simp |
491 by (simp add: inf_Sup) |
492 |
492 |
493 lemma dual_complete_distrib_lattice: |
493 lemma dual_complete_distrib_lattice: |
494 "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
494 "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>" |
495 apply (rule class.complete_distrib_lattice.intro) |
495 apply (rule class.complete_distrib_lattice.intro) |
496 apply (fact dual_complete_lattice) |
496 apply (fact dual_complete_lattice) |
605 lemma complete_linorder_sup_max: "sup = max" |
605 lemma complete_linorder_sup_max: "sup = max" |
606 by (auto intro: antisym simp add: max_def fun_eq_iff) |
606 by (auto intro: antisym simp add: max_def fun_eq_iff) |
607 |
607 |
608 lemma Inf_less_iff: |
608 lemma Inf_less_iff: |
609 "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
609 "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)" |
610 unfolding not_le [symmetric] le_Inf_iff by auto |
610 by (simp add: not_le [symmetric] le_Inf_iff) |
611 |
611 |
612 lemma INF_less_iff: |
612 lemma INF_less_iff: |
613 "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
613 "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)" |
614 using Inf_less_iff [of "f ` A"] by simp |
614 by (simp add: Inf_less_iff [of "f ` A"]) |
615 |
615 |
616 lemma less_Sup_iff: |
616 lemma less_Sup_iff: |
617 "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
617 "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)" |
618 unfolding not_le [symmetric] Sup_le_iff by auto |
618 by (simp add: not_le [symmetric] Sup_le_iff) |
619 |
619 |
620 lemma less_SUP_iff: |
620 lemma less_SUP_iff: |
621 "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
621 "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)" |
622 using less_Sup_iff [of _ "f ` A"] by simp |
622 by (simp add: less_Sup_iff [of _ "f ` A"]) |
623 |
623 |
624 lemma Sup_eq_top_iff [simp]: |
624 lemma Sup_eq_top_iff [simp]: |
625 "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)" |
625 "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)" |
626 proof |
626 proof |
627 assume *: "\<Squnion>A = \<top>" |
627 assume *: "\<Squnion>A = \<top>" |
628 show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric] |
628 show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric] |
629 proof (intro allI impI) |
629 proof (intro allI impI) |
630 fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i" |
630 fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i" |
631 unfolding less_Sup_iff by auto |
631 by (simp add: less_Sup_iff) |
632 qed |
632 qed |
633 next |
633 next |
634 assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i" |
634 assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i" |
635 show "\<Squnion>A = \<top>" |
635 show "\<Squnion>A = \<top>" |
636 proof (rule ccontr) |
636 proof (rule ccontr) |