src/HOL/Library/FuncSet.thy
changeset 58606 9c66f7c541fb
parent 56777 9c3f0ae99532
child 58783 c6348a062131
     1.1 --- a/src/HOL/Library/FuncSet.thy	Mon Oct 06 21:21:46 2014 +0200
     1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Oct 07 10:34:24 2014 +0200
     1.3 @@ -199,6 +199,9 @@
     1.4      "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
     1.5    by (simp add: fun_eq_iff Pi_def restrict_def)
     1.6  
     1.7 +lemma restrict_UNIV: "restrict f UNIV = f"
     1.8 +  by (simp add: restrict_def)
     1.9 +
    1.10  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
    1.11    by (simp add: inj_on_def restrict_def)
    1.12