From 4e56330e2f65e7f8e4e7d21593b453d537d90e67 Mon Sep 17 00:00:00 2001
From: Tim Makarios <tjm1983@gmail.com>
Date: Thu, 2 Apr 2015 16:53:37 +1300
Subject: [PATCH] Showed "inv f y = x" is equivalent to "f x = y" if "bij f" is
 true

---
 Miscellany.thy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Miscellany.thy b/Miscellany.thy
index b72be69..ef1a073 100644
--- a/Miscellany.thy
+++ b/Miscellany.thy
@@ -7,4 +7,9 @@ lemma bij_f_inv_f [simp]:
   shows "f (inv f x) = x"
   by (metis UNIV_I assms bij_betw_imp_surj f_inv_into_f)
 
+lemma bij_f_x_equiv_inv_f_y [simp]:
+  assumes "bij f"
+  shows "inv f y = x \<longleftrightarrow> f x = y"
+  by (metis assms bij_betw_def bij_f_inv_f inv_f_eq)
+
 end
-- 
2.11.4.GIT