equal
deleted
inserted
replaced
15 begin |
15 begin |
16 |
16 |
17 setup CooperData.setup |
17 setup CooperData.setup |
18 |
18 |
19 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *} |
19 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *} |
|
20 |
20 |
21 |
21 lemma minf: |
22 lemma minf: |
22 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |
23 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |
23 \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)" |
24 \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)" |
24 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |
25 "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> |