# 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 (\x. x + a)" + and bij_uminus: "bij uminus" and bij_diff: "bij ((-) a)" and bij_diff_right: "bij (\x. x - a)" by(simp_all add: bij_def)