# HG changeset patch
# User nipkow
# Date 1665555667 -7200
# Node ID 60511708a650ad874aa3307d4bc74f8cc87266b6
# Parent  5ede2fce5b01b764cab52b57431cdba684e68317
one more lemma

diff -r 5ede2fce5b01 -r 60511708a650 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Oct 11 18:52:01 2022 +0200
+++ b/src/HOL/Fun.thy	Wed Oct 12 08:21:07 2022 +0200
@@ -722,6 +722,9 @@
 lemma inj_uminus[simp, intro]: "inj_on uminus A"
   by (auto intro!: inj_onI)
 
+lemma surj_uminus[simp]: "surj uminus"
+using surjI minus_minus by blast
+
 lemma surj_plus [simp]:
   "surj ((+) a)"
 proof (standard, simp, standard, simp)
@@ -762,6 +765,7 @@
 qed
 
 lemma shows bij_plus: "bij ((+) a)" and bij_plus_right: "bij (\<lambda>x. x + a)"
+  and bij_uminus: "bij uminus"
   and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\<lambda>x. x - a)"
 by(simp_all add: bij_def)