added missing file

lecopivo · Sep 17, 2023 · afad241 · afad241
1 parent 9de5267
commit afad241
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/SciLean/Data/Function.lean b/SciLean/Data/Function.lean
@@ -0,0 +1,5 @@
+import Mathlib.Logic.Function.Basic
+
+def Function.Inverse (g : β → α) (f : α → β) :=
+  Function.LeftInverse g f ∧ Function.RightInverse g f
+