src/HOL/Library/FuncSet.thy
 changeset 14762 bd349ff7907a parent 14745 94be403deb84 child 14853 8d710bece29f
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Wed May 19 11:30:18 2004 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy	Wed May 19 11:30:56 2004 +0200
1.3 @@ -57,6 +57,9 @@
1.4  lemma funcset_mem: "[|f \<in> A -> B; x \<in> A|] ==> f x \<in> B"
1.6
1.7 +lemma funcset_image: "f \<in> A\<rightarrow>B ==> f ` A \<subseteq> B"
1.8 +by (auto simp add: Pi_def)
1.9 +
1.10  lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\<exists>x\<in>A. B(x) = {})"
1.11  apply (simp add: Pi_def, auto)
1.12  txt{*Converse direction requires Axiom of Choice to exhibit a function
1.13 @@ -166,6 +169,34 @@
1.14    done
1.15
1.16
1.17 +subsection{*Bijections Between Sets*}
1.18 +
1.19 +text{*The basic definition could be moved to @{text "Fun.thy"}, but most of
1.20 +the theorems belong here, or need at least @{term Hilbert_Choice}.*}
1.21 +
1.22 +constdefs
1.23 +  bij_betw :: "['a => 'b, 'a set, 'b set] => bool"         (*bijective*)
1.24 +    "bij_betw f A B == inj_on f A & f ` A = B"
1.25 +
1.26 +lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
1.28 +
1.29 +lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
1.30 +by (auto simp add: bij_betw_def inj_on_Inv Pi_def)
1.31 +
1.32 +lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
1.33 +apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
1.34 +apply (simp add: image_compose [symmetric] o_def)
1.35 +apply (simp add: image_def Inv_f_f)
1.36 +done
1.37 +
1.38 +lemma bij_betw_compose:
1.39 +    "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C"
1.40 +apply (simp add: bij_betw_def compose_eq inj_on_compose)
1.41 +apply (auto simp add: compose_def image_def)
1.42 +done
1.43 +
1.44 +
1.45  subsection{*Cardinality*}
1.46
1.47  lemma card_inj: "[|f \<in> A\<rightarrow>B; inj_on f A; finite B|] ==> card(A) \<le> card(B)"
```