new bij_betw operator
authorpaulson
Wed May 19 11:30:56 2004 +0200 (2004-05-19)
changeset 14762bd349ff7907a
parent 14761 28b5eb4a867f
child 14763 c1fd297712ba
new bij_betw operator
src/HOL/Library/FuncSet.thy
     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.5    by (simp add: Pi_def)
     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.27 +by (simp add: bij_betw_def)
    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)"