equal
deleted
inserted
replaced
87 text {* the = relation between two chains is preserved by their lubs *} |
87 text {* the = relation between two chains is preserved by their lubs *} |
88 |
88 |
89 lemma lub_equal: |
89 lemma lub_equal: |
90 "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk> |
90 "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk> |
91 \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
91 \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
92 by (simp only: ext_iff [symmetric]) |
92 by (simp only: fun_eq_iff [symmetric]) |
93 |
93 |
94 lemma lub_eq: |
94 lemma lub_eq: |
95 "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
95 "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
96 by simp |
96 by simp |
97 |
97 |