equal
deleted
inserted
replaced
31 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
31 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A" |
32 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
32 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z" |
33 begin |
33 begin |
34 |
34 |
35 lemma dual_complete_lattice: |
35 lemma dual_complete_lattice: |
36 "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" |
36 "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>" |
37 by (auto intro!: complete_lattice.intro dual_bounded_lattice) |
37 by (auto intro!: class.complete_lattice.intro dual_bounded_lattice) |
38 (unfold_locales, (fact bot_least top_greatest |
38 (unfold_locales, (fact bot_least top_greatest |
39 Sup_upper Sup_least Inf_lower Inf_greatest)+) |
39 Sup_upper Sup_least Inf_lower Inf_greatest)+) |
40 |
40 |
41 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}" |
41 lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}" |
42 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |
42 by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) |