src/HOL/Library/FuncSet.thy
changeset 39595 9f86e46779e4
parent 39302 d7728f65b353
child 40631 b3f85ba3dae4
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Sep 20 14:50:45 2010 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Sep 20 21:09:25 2010 +0200
     1.3 @@ -173,6 +173,20 @@
     1.4  text{*The definition of @{const bij_betw} is in @{text "Fun.thy"}, but most of
     1.5  the theorems belong here, or need at least @{term Hilbert_Choice}.*}
     1.6  
     1.7 +lemma bij_betwI:
     1.8 +assumes "f \<in> A \<rightarrow> B" and "g \<in> B \<rightarrow> A"
     1.9 +    and g_f: "\<And>x. x\<in>A \<Longrightarrow> g (f x) = x" and f_g: "\<And>y. y\<in>B \<Longrightarrow> f (g y) = y"
    1.10 +shows "bij_betw f A B"
    1.11 +unfolding bij_betw_def
    1.12 +proof
    1.13 +  show "inj_on f A" by (metis g_f inj_on_def)
    1.14 +next
    1.15 +  have "f ` A \<subseteq> B" using `f \<in> A \<rightarrow> B` by auto
    1.16 +  moreover
    1.17 +  have "B \<subseteq> f ` A" by auto (metis Pi_mem `g \<in> B \<rightarrow> A` f_g image_iff)
    1.18 +  ultimately show "f ` A = B" by blast
    1.19 +qed
    1.20 +
    1.21  lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
    1.22  by (auto simp add: bij_betw_def)
    1.23  
    1.24 @@ -207,6 +221,9 @@
    1.25        !!x. x\<in>A ==> f x = g x |] ==> f = g"
    1.26  by (force simp add: fun_eq_iff extensional_def)
    1.27  
    1.28 +lemma extensional_restrict:  "f \<in> extensional A \<Longrightarrow> restrict f A = f"
    1.29 +by(rule extensionalityI[OF restrict_extensional]) auto
    1.30 +
    1.31  lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
    1.32  by (unfold inv_into_def) (fast intro: someI2)
    1.33