equal
deleted
inserted
replaced
84 by (fast elim: someI) |
84 by (fast elim: someI) |
85 |
85 |
86 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)" |
86 lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)" |
87 by (fast elim: someI) |
87 by (fast elim: someI) |
88 |
88 |
|
89 lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))" |
|
90 by (fast elim: someI) |
|
91 |
|
92 lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))" |
|
93 by (fast elim: someI) |
|
94 |
|
95 lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))" |
|
96 by (fast elim: someI) |
|
97 |
|
98 lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))" |
|
99 by (fast elim: someI) |
89 |
100 |
90 subsection {*Function Inverse*} |
101 subsection {*Function Inverse*} |
91 |
102 |
92 lemma inv_def: "inv f = (%y. SOME x. f x = y)" |
103 lemma inv_def: "inv f = (%y. SOME x. f x = y)" |
93 by(simp add: inv_into_def) |
104 by(simp add: inv_into_def) |