equal
deleted
inserted
replaced
144 "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i" |
144 "\<lbrakk>compact x; chain Y; x \<sqsubseteq> (\<Squnion>i. Y i)\<rbrakk> \<Longrightarrow> \<exists>i. x \<sqsubseteq> Y i" |
145 unfolding compact_def adm_def by fast |
145 unfolding compact_def adm_def by fast |
146 |
146 |
147 lemma compact_below_lub_iff: |
147 lemma compact_below_lub_iff: |
148 "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)" |
148 "\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)" |
149 by (fast intro: compactD2 elim: below_trans is_ub_thelub) |
149 by (fast intro: compactD2 elim: below_lub) |
150 |
150 |
151 lemma compact_chfin [simp]: "compact (x::'a::chfin)" |
151 lemma compact_chfin [simp]: "compact (x::'a::chfin)" |
152 by (rule compactI [OF adm_chfin]) |
152 by (rule compactI [OF adm_chfin]) |
153 |
153 |
154 lemma compact_imp_max_in_chain: |
154 lemma compact_imp_max_in_chain: |