equal
deleted
inserted
replaced
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: expand_fun_eq [symmetric]) |
92 by (simp only: expand_fun_eq [symmetric]) |
|
93 |
|
94 lemma lub_eq: |
|
95 "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)" |
|
96 by simp |
93 |
97 |
94 text {* more results about mono and = of lubs of chains *} |
98 text {* more results about mono and = of lubs of chains *} |
95 |
99 |
96 lemma lub_mono2: |
100 lemma lub_mono2: |
97 "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk> |
101 "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk> |