# HG changeset patch # User paulson # Date 1084959056 -7200 # Node ID bd349ff7907aa5a5c28acb4ea7b6fecba7126f8a # Parent 28b5eb4a867f086b7923a9a83577431d9308db15 new bij_betw operator diff -r 28b5eb4a867f -r bd349ff7907a src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Wed May 19 11:30:18 2004 +0200 +++ b/src/HOL/Library/FuncSet.thy Wed May 19 11:30:56 2004 +0200 @@ -57,6 +57,9 @@ lemma funcset_mem: "[|f \ A -> B; x \ A|] ==> f x \ B" by (simp add: Pi_def) +lemma funcset_image: "f \ A\B ==> f ` A \ B" +by (auto simp add: Pi_def) + lemma Pi_eq_empty: "((PI x: A. B x) = {}) = (\x\A. B(x) = {})" apply (simp add: Pi_def, auto) txt{*Converse direction requires Axiom of Choice to exhibit a function @@ -166,6 +169,34 @@ done +subsection{*Bijections Between Sets*} + +text{*The basic definition could be moved to @{text "Fun.thy"}, but most of +the theorems belong here, or need at least @{term Hilbert_Choice}.*} + +constdefs + bij_betw :: "['a => 'b, 'a set, 'b set] => bool" (*bijective*) + "bij_betw f A B == inj_on f A & f ` A = B" + +lemma bij_betw_imp_inj_on: "bij_betw f A B \ inj_on f A" +by (simp add: bij_betw_def) + +lemma bij_betw_imp_funcset: "bij_betw f A B \ f \ A \ B" +by (auto simp add: bij_betw_def inj_on_Inv Pi_def) + +lemma bij_betw_Inv: "bij_betw f A B \ bij_betw (Inv A f) B A" +apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem) +apply (simp add: image_compose [symmetric] o_def) +apply (simp add: image_def Inv_f_f) +done + +lemma bij_betw_compose: + "[| bij_betw f A B; bij_betw g B C |] ==> bij_betw (compose A g f) A C" +apply (simp add: bij_betw_def compose_eq inj_on_compose) +apply (auto simp add: compose_def image_def) +done + + subsection{*Cardinality*} lemma card_inj: "[|f \ A\B; inj_on f A; finite B|] ==> card(A) \ card(B)"