feat(library/data/set): add theory of functions and maps between sets

library/data/set/classical_inverse.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.set.function
+Author: Jeremy Avigad, Andrew Zipperer
+
+Using classical logic, defines an inverse function.
+-/
+import .function .map
+import logic.axioms.classical
+open eq.ops
+
+namespace set
+
+variables {X Y : Type}
+
+definition inv_fun (f : X → Y) (a : set X) (dflt : X) (y : Y) : X :=
+if H : ∃₀ x ∈ a, f x = y then some H else dflt
+
+theorem inv_fun_pos {f : X → Y} {a : set X} {dflt : X} {y : Y}
+  (H : ∃₀ x ∈ a, f x = y) : (inv_fun f a dflt y ∈ a) ∧ (f (inv_fun f a dflt y) = y) :=
+have H1 : inv_fun f a dflt y = some H, from dif_pos H,
+H1⁻¹ ▸ some_spec H
+
+theorem inv_fun_neg {f : X → Y} {a : set X} {dflt : X} {y : Y}
+  (H : ¬ ∃₀ x ∈ a, f x = y) : inv_fun f a dflt y = dflt :=
+dif_neg H
+
+variables {f : X → Y} {a : set X} {b : set Y}
+
+theorem maps_to_inv_fun {dflt : X} (dflta : dflt ∈ a) :
+  maps_to (inv_fun f a dflt) b a :=
+let f' := inv_fun f a dflt in
+take y,
+assume yb : y ∈ b,
+show f' y ∈ a, from
+  by_cases
+    (assume H : ∃₀ x ∈ a, f x = y,
+      and.left (inv_fun_pos H))
+    (assume H : ¬ ∃₀ x ∈ a, f x = y,
+      (inv_fun_neg H)⁻¹ ▸ dflta)
+
+theorem left_inv_on_inv_fun_of_inj_on (dflt : X) (H : inj_on f a) :
+  left_inv_on (inv_fun f a dflt) f a :=
+let f' := inv_fun f a dflt in
+take x,
+assume xa : x ∈ a,
+have H1 : ∃₀ x' ∈ a, f x' = f x, from exists.intro x (and.intro xa rfl),
+have H2 : f' (f x) ∈ a ∧ f (f' (f x)) = f x, from inv_fun_pos H1,
+show f' (f x) = x, from H (and.left H2) xa (and.right H2)
+
+theorem right_inv_on_inv_fun_of_surj_on (dflt : X) (H : surj_on f a b) :
+  right_inv_on (inv_fun f a dflt) f b :=
+let f' := inv_fun f a dflt in
+take y,
+assume yb: y ∈ b,
+obtain x (Hx : x ∈ a ∧ f x = y), from H yb,
+have Hy : f' y ∈ a ∧ f (f' y) = y, from inv_fun_pos (exists.intro x Hx),
+and.right Hy
+
+end set
+
+open set
+
+namespace map
+
+variables {X Y : Type} {a : set X} {b : set Y}
+
+protected definition inverse (f : map a b) {dflt : X} (dflta : dflt ∈ a) :=
+map.mk (inv_fun f a dflt) (@maps_to_inv_fun _ _ _ _ b _ dflta)
+
+theorem left_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : injective f) :
+  left_inverse (inverse f dflta) f :=
+left_inv_on_inv_fun_of_inj_on dflt H
+
+theorem right_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : surjective f) :
+  right_inverse (inverse f dflta) f :=
+right_inv_on_inv_fun_of_surj_on dflt H
+
+theorem is_inverse_inverse {f : map a b} {dflt : X} (dflta : dflt ∈ a) (H : bijective f) :
+is_inverse (inverse f dflta) f :=
+and.intro
+  (left_inverse_inverse dflta (and.left H))
+  (right_inverse_inverse dflta (and.right H))
+
+end map

library/data/set/default.lean

@@ -5,4 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.set.default
 Author: Jeremy Avigad
 -/
-import .basic
+import .basic .function .map

library/data/set/function.lean

@@ -12,53 +12,220 @@ import algebra.function
 open function eq.ops
 
 namespace set
-  variables {X Y Z : Type}
 
-  abbreviation eq_on (f1 f2 : X → Y) (a : set X) : Prop :=
+variables {X Y Z : Type}
-  ∀₀ x ∈ a, f1 x = f2 x
 
-  definition image (f : X → Y) (a : set X) : set Y := {y : Y | ∃x, x ∈ a ∧ f x = y}
+abbreviation eq_on (f1 f2 : X → Y) (a : set X) : Prop :=
-  notation f `'[`:max a `]` := image f a
+∀₀ x ∈ a, f1 x = f2 x
 
-  theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) :
+/- image -/
-    f1 '[a] = f2 '[a] :=
-  setext (take y, iff.intro
-    (assume H2,
-      obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
-      have H4 : x ∈ a, from and.left H3,
-      have H5 : f2 x = y, from (H1 H4)⁻¹ ⬝ and.right H3,
-      exists.intro x (and.intro H4 H5))
-    (assume H2,
-      obtain x (H3 : x ∈ a ∧ f2 x = y), from H2,
-      have H4 : x ∈ a, from and.left H3,
-      have H5 : f1 x = y, from (H1 H4) ⬝ and.right H3,
-      exists.intro x (and.intro H4 H5)))
 
-  definition maps_to (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b
+definition image (f : X → Y) (a : set X) : set Y := {y : Y | ∃x, x ∈ a ∧ f x = y}
+notation f `'[`:max a `]` := image f a
 
-  theorem maps_to_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+theorem image_eq_image_of_eq_on {f1 f2 : X → Y} {a : set X} (H1 : eq_on f1 f2 a) :
-     (H1 : maps_to g b c) (H2 : maps_to f a b) : maps_to (g ∘ f) a c :=
+  f1 '[a] = f2 '[a] :=
-  take x, assume H : x ∈ a, H1 (H2 H)
+setext (take y, iff.intro
+  (assume H2,
+    obtain x (H3 : x ∈ a ∧ f1 x = y), from H2,
+    have H4 : x ∈ a, from and.left H3,
+    have H5 : f2 x = y, from (H1 H4)⁻¹ ⬝ and.right H3,
+    exists.intro x (and.intro H4 H5))
+  (assume H2,
+    obtain x (H3 : x ∈ a ∧ f2 x = y), from H2,
+    have H4 : x ∈ a, from and.left H3,
+    have H5 : f1 x = y, from (H1 H4) ⬝ and.right H3,
+    exists.intro x (and.intro H4 H5)))
 
-  definition inj_on (f : X → Y) (a : set X) : Prop :=
+/- maps to -/
-  ∀⦃x1 x2 : X⦄, x1 ∈ a → x2 ∈ a → f x1 = f x2 → x1 = x2
 
-  theorem inj_on_of_eq_on {f1 f2 : X → Y} {a : set X} (inj_f1 : inj_on f1 a)
+definition maps_to [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b
-      (eq_f1_f2 : eq_on f1 f2 a) : inj_on f2 a :=
-  take x1 x2 : X,
-  assume ax1 : x1 ∈ a,
-  assume ax2 : x2 ∈ a,
-  assume H : f2 x1 = f2 x2,
-  have H' : f1 x1 = f1 x2, from eq_f1_f2 ax1 ⬝ H ⬝ (eq_f1_f2 ax2)⁻¹,
-  show x1 = x2, from inj_f1 ax1 ax2 H'
 
-  definition surj_on (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]
+theorem maps_to_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eq_on_a : eq_on f1 f2 a)
+    (maps_to_f1 : maps_to f1 a b) :
+  maps_to f2 a b :=
+take x,
+assume xa : x ∈ a,
+have H : f1 x ∈ b, from maps_to_f1 xa,
+show f2 x ∈ b, from eq_on_a xa ▸ H
+
+theorem maps_to_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+   (H1 : maps_to g b c) (H2 : maps_to f a b) : maps_to (g ∘ f) a c :=
+take x, assume H : x ∈ a, H1 (H2 H)
+
+/- injectivity -/
+
+definition inj_on [reducible] (f : X → Y) (a : set X) : Prop :=
+∀⦃x1 x2 : X⦄, x1 ∈ a → x2 ∈ a → f x1 = f x2 → x1 = x2
+
+theorem inj_on_of_eq_on {f1 f2 : X → Y} {a : set X} (eq_f1_f2 : eq_on f1 f2 a)
+    (inj_f1 : inj_on f1 a) :
+  inj_on f2 a :=
+take x1 x2 : X,
+assume ax1 : x1 ∈ a,
+assume ax2 : x2 ∈ a,
+assume H : f2 x1 = f2 x2,
+have H' : f1 x1 = f1 x2, from eq_f1_f2 ax1 ⬝ H ⬝ (eq_f1_f2 ax2)⁻¹,
+show x1 = x2, from inj_f1 ax1 ax2 H'
+
+theorem inj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y}
+    (fab : maps_to f a b) (Hg : inj_on g b) (Hf: inj_on f a) :
+  inj_on (g ∘ f) a :=
+take x1 x2 : X,
+assume x1a : x1 ∈ a,
+assume x2a : x2 ∈ a,
+have  fx1b : f x1 ∈ b, from fab x1a,
+have  fx2b : f x2 ∈ b, from fab x2a,
+assume  H1 : g (f x1) = g (f x2),
+have    H2 : f x1 = f x2, from Hg fx1b fx2b H1,
+show x1 = x2, from Hf x1a x2a H2
+
+/- surjectivity -/
+
+definition surj_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := b ⊆ f '[a]
+
+theorem surj_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eq_f1_f2 : eq_on f1 f2 a)
+    (surj_f1 : surj_on f1 a b) :
+  surj_on f2 a b :=
+take y, assume H : y ∈ b,
+obtain x (H1 : x ∈ a ∧ f1 x = y), from surj_f1 H,
+have H2 : x ∈ a, from and.left H1,
+have H3 : f2 x = y, from (eq_f1_f2 H2)⁻¹ ⬝ and.right H1,
+exists.intro x (and.intro H2 H3)
+
+theorem surj_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+  (Hg : surj_on g b c) (Hf: surj_on f a b) :
+  surj_on (g ∘ f) a c :=
+take z,
+assume zc : z ∈ c,
+obtain y (H1 : y ∈ b ∧ g y = z), from Hg zc,
+obtain x (H2 : x ∈ a ∧ f x = y), from Hf (and.left H1),
+show ∃x, x ∈ a ∧ g (f x) = z, from
+  exists.intro x
+    (and.intro
+      (and.left H2)
+      (calc
+        g (f x) = g y : {and.right H2}
+            ... = z   : and.right H1))
+
+/- bijectivity -/
+
+definition bij_on [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop :=
+maps_to f a b ∧ inj_on f a ∧ surj_on f a b
+
+theorem bij_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (eqf : eq_on f1 f2 a)
+     (H : bij_on f1 a b) : bij_on f2 a b :=
+match H with and.intro Hmap (and.intro Hinj Hsurj) :=
+  and.intro
+    (maps_to_of_eq_on eqf Hmap)
+    (and.intro
+      (inj_on_of_eq_on eqf Hinj)
+      (surj_on_of_eq_on eqf Hsurj))
+end
+
+theorem bij_on_compose {g : Y → Z} {f : X → Y} {a : set X} {b : set Y} {c : set Z}
+  (Hg : bij_on g b c) (Hf: bij_on f a b) :
+  bij_on (g ∘ f) a c :=
+match Hg with and.intro Hgmap (and.intro Hginj Hgsurj) :=
+  match Hf with and.intro Hfmap (and.intro Hfinj Hfsurj) :=
+    and.intro
+      (maps_to_compose Hgmap Hfmap)
+      (and.intro
+        (inj_on_compose Hfmap Hginj Hfinj)
+        (surj_on_compose Hgsurj Hfsurj))
+  end
+end
+
+/- left inverse -/
+
+-- g is a left inverse to f on a
+definition left_inv_on [reducible] (g : Y → X) (f : X → Y) (a : set X) : Prop :=
+∀₀ x ∈ a, g (f x) = x
+
+theorem left_inv_on_of_eq_on_left {g1 g2 : Y → X} {f : X → Y} {a : set X} {b : set Y}
+  (fab : maps_to f a b) (eqg : eq_on g1 g2 b) (H : left_inv_on g1 f a) : left_inv_on g2 f a :=
+take x,
+assume xa : x ∈ a,
+calc
+  g2 (f x) = g1 (f x) : (eqg (fab xa))⁻¹
+       ... = x        : H xa
+
+theorem left_inv_on_of_eq_on_right {g : Y → X} {f1 f2 : X → Y} {a : set X}
+  (eqf : eq_on f1 f2 a) (H : left_inv_on g f1 a) : left_inv_on g f2 a :=
+take x,
+assume xa : x ∈ a,
+calc
+  g (f2 x) = g (f1 x) : {(eqf xa)⁻¹}
+       ... = x        : H xa
+
+theorem inj_on_of_left_inv_on {g : Y → X} {f : X → Y} {a : set X} (H : left_inv_on g f a) :
+  inj_on f a :=
+take x1 x2,
+assume x1a : x1 ∈ a,
+assume x2a : x2 ∈ a,
+assume H1 : f x1 = f x2,
+calc
+  x1     = g (f x1) : H x1a
+     ... = g (f x2) : H1
+     ... = x2       : H x2a
+
+theorem left_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
+   {a : set X} {b : set Y} (fab : maps_to f a b)
+    (Hf : left_inv_on f' f a) (Hg : left_inv_on g' g b) : left_inv_on (f' ∘ g') (g ∘ f) a :=
+take x : X,
+assume xa : x ∈ a,
+have fxb : f x ∈ b, from fab xa,
+calc
+  f' (g' (g (f x))) = f' (f x) : Hg fxb
+                ... = x        : Hf xa
+
+/- right inverse -/
+
+-- g is a right inverse to f on a
+definition right_inv_on [reducible] (g : Y → X) (f : X → Y) (b : set Y) : Prop :=
+left_inv_on f g b
+
+theorem right_inv_on_of_eq_on_left {g1 g2 : Y → X} {f : X → Y} {a : set X} {b : set Y}
+  (eqg : eq_on g1 g2 b) (H : right_inv_on g1 f b) : right_inv_on g2 f b :=
+left_inv_on_of_eq_on_right eqg H
+
+theorem right_inv_on_of_eq_on_right {g : Y → X} {f1 f2 : X → Y} {a : set X} {b : set Y}
+  (gba : maps_to g b a) (eqf : eq_on f1 f2 a) (H : right_inv_on g f1 b) : right_inv_on g f2 b :=
+left_inv_on_of_eq_on_left gba eqf H
+
+theorem surj_on_of_right_inv_on {g : Y → X} {f : X → Y} {a : set X} {b : set Y}
+    (gba : maps_to g b a) (H : right_inv_on g f b) :
+  surj_on f a b :=
+take y,
+assume yb : y ∈ b,
+have gya : g y ∈ a, from gba yb,
+have H1 : f (g y) = y, from H yb,
+exists.intro (g y) (and.intro gya H1)
+
+theorem right_inv_on_compose {f' : Y → X} {g' : Z → Y} {g : Y → Z} {f : X → Y}
+   {c : set Z} {b : set Y} (g'cb : maps_to g' c b)
+    (Hf : right_inv_on f' f b) (Hg : right_inv_on g' g c) : right_inv_on (f' ∘ g') (g ∘ f) c :=
+left_inv_on_compose g'cb Hg Hf
+
+theorem eq_on_of_left_inv_of_right_inv {g1 g2 : Y → X} {f : X → Y} {a : set X} {b : set Y}
+  (g2ba : maps_to g2 b a) (Hg1 : left_inv_on g1 f a) (Hg2 : right_inv_on g2 f b) : eq_on g1 g2 b :=
+take y,
+assume yb : y ∈ b,
+calc
+  g1 y = g1 (f (g2 y)) : {(Hg2 yb)⁻¹}
+   ... = g2 y          : Hg1 (g2ba yb)
+
+/- inverses -/
+
+-- g is an inverse to f viewed as a map from a to b
+definition inv_on [reducible] (g : Y → X) (f : X → Y) (a : set X) (b : set Y) : Prop :=
+left_inv_on g f a ∧ right_inv_on g f b
+
+theorem bij_on_of_inv_on {g : Y → X} {f : X → Y} {a : set X} {b : set Y} (fab : maps_to f a b)
+  (gba : maps_to g b a) (H : inv_on g f a b) : bij_on f a b :=
+and.intro fab
+  (and.intro
+    (inj_on_of_left_inv_on (and.left H))
+    (surj_on_of_right_inv_on gba (and.right H)))
 
-  theorem surj_on_of_eq_on {f1 f2 : X → Y} {a : set X} {b : set Y} (surj_f1 : surj_on f1 a b)
-      (eq_f1_f2 : eq_on f1 f2 a) : surj_on f2 a b :=
-  take y, assume H : y ∈ b,
-  obtain x (H1 : x ∈ a ∧ f1 x = y), from surj_f1 H,
-  have H2 : x ∈ a, from and.left H1,
-  have H3 : f2 x = y, from (eq_f1_f2 H2)⁻¹ ⬝ and.right H1,
-  exists.intro x (and.intro H2 H3)
 end set

library/data/set/map.lean

@@ -0,0 +1,152 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.set.map
+Author: Jeremy Avigad, Andrew Zipperer
+
+Functions between subsets of finite types, bundled with the domain and range.
+-/
+import data.set.function
+open eq.ops set
+
+record map {X Y : Type} (a : set X) (b : set Y) := (func : X → Y) (mapsto : maps_to func a b)
+attribute map.func [coercion]
+
+namespace map
+
+variables {X Y Z: Type}
+variables {a : set X} {b : set Y} {c : set Z}
+
+/- the equivalence relation -/
+
+protected definition equiv [reducible] (f1 f2 : map a b) : Prop := eq_on f1 f2 a
+
+namespace equiv_notation
+  infix `~` := map.equiv
+end equiv_notation
+open equiv_notation
+
+protected theorem equiv.refl (f : map a b) : f ~ f := take x, assume H, rfl
+
+protected theorem equiv.symm {f₁ f₂ : map a b} : f₁ ~ f₂ → f₂ ~ f₁ :=
+assume H : f₁ ~ f₂,
+take x, assume Ha : x ∈ a, eq.symm (H Ha)
+
+protected theorem equiv.trans {f₁ f₂ f₃ : map a b} : f₁ ~ f₂ → f₂ ~ f₃ → f₁ ~ f₃ :=
+assume H₁ : f₁ ~ f₂, assume H₂ : f₂ ~ f₃,
+take x, assume Ha : x ∈ a, eq.trans (H₁ Ha) (H₂ Ha)
+
+protected theorem equiv.is_equivalence {X Y : Type} (a : set X) (b : set Y) :
+  equivalence (@equiv X Y a b) :=
+mk_equivalence (@equiv X Y a b) (@equiv.refl X Y a b) (@equiv.symm X Y a b) (@equiv.trans X Y a b)
+
+/- compose -/
+
+definition compose (g : map b c) (f : map a b) : map a c :=
+map.mk (#function g ∘ f) (maps_to_compose (mapsto g) (mapsto f))
+
+notation g ∘ f := compose g f
+
+/- range -/
+
+definition range (f : map a b) : set Y := image f a
+
+theorem range_eq_range_of_equiv {f1 f2 : map a b} (H : f1 ~ f2) : range f1 = range f2 :=
+image_eq_image_of_eq_on H
+
+/- injective -/
+
+definition injective (f : map a b) : Prop := inj_on f a
+
+theorem injective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : injective f1) :
+  injective f2 :=
+inj_on_of_eq_on H1 H2
+
+theorem injective_compose {g : map b c} {f : map a b} (Hg : injective g) (Hf: injective f) :
+  injective (g ∘ f) :=
+inj_on_compose (mapsto f) Hg Hf
+
+/- surjective -/
+
+definition surjective (f : map a b) : Prop := surj_on f a b
+
+theorem surjective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : surjective f1) :
+  surjective f2 :=
+surj_on_of_eq_on H1 H2
+
+theorem surjective_compose {g : map b c} {f : map a b} (Hg : surjective g) (Hf: surjective f) :
+  surjective (g ∘ f) :=
+surj_on_compose Hg Hf
+
+/- bijective -/
+
+definition bijective (f : map a b) : Prop := injective f ∧ surjective f
+
+theorem bijective_of_equiv {f1 f2 : map a b} (H1 : f1 ~ f2) (H2 : bijective f1) :
+  bijective f2 :=
+and.intro (injective_of_equiv H1 (and.left H2)) (surjective_of_equiv H1 (and.right H2))
+
+theorem bijective_compose {g : map b c} {f : map a b} (Hg : bijective g) (Hf: bijective f) :
+  bijective (g ∘ f) :=
+and.intro
+  (injective_compose (and.left Hg) (and.left Hf))
+  (surjective_compose (and.right Hg) (and.right Hf))
+
+/- left inverse -/
+
+-- g is a left inverse to f
+definition left_inverse (g : map b a) (f : map a b) : Prop := left_inv_on g f a
+
+theorem left_inverse_of_equiv_left {g1 g2 : map b a} {f : map a b} (eqg : g1 ~ g2)
+  (H : left_inverse g1 f) : left_inverse g2 f :=
+left_inv_on_of_eq_on_left (mapsto f) eqg H
+
+theorem left_inverse_of_equiv_right {g : map b a} {f1 f2 : map a b} (eqf : f1 ~ f2)
+  (H : left_inverse g f1) : left_inverse g f2 :=
+left_inv_on_of_eq_on_right eqf H
+
+theorem injective_of_left_inverse {g : map b a} {f : map a b} (H : left_inverse g f) :
+  injective f :=
+inj_on_of_left_inv_on H
+
+theorem left_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
+    (Hf : left_inverse f' f) (Hg : left_inverse g' g) : left_inverse (f' ∘ g') (g ∘ f) :=
+left_inv_on_compose (mapsto f) Hf Hg
+
+/- right inverse -/
+
+-- g is a right inverse to f
+definition right_inverse (g : map b a) (f : map a b) : Prop := left_inverse f g
+
+theorem right_inverse_of_equiv_left {g1 g2 : map b a} {f : map a b} (eqg : g1 ~ g2)
+  (H : right_inverse g1 f) : right_inverse g2 f :=
+left_inverse_of_equiv_right eqg H
+
+theorem right_inverse_of_equiv_right {g : map b a} {f1 f2 : map a b} (eqf : f1 ~ f2)
+  (H : right_inverse g f1) : right_inverse g f2 :=
+left_inverse_of_equiv_left eqf H
+
+theorem surjective_of_right_inverse {g : map b a} {f : map a b} (H : right_inverse g f) :
+  surjective f :=
+surj_on_of_right_inv_on (mapsto g) H
+
+theorem right_inverse_compose {f' : map b a} {g' : map c b} {g : map b c} {f : map a b}
+    (Hf : right_inverse f' f) (Hg : right_inverse g' g) : right_inverse (f' ∘ g') (g ∘ f) :=
+left_inverse_compose Hg Hf
+
+theorem equiv_of_left_inverse_of_right_inverse {g1 g2 : map b a} {f : map a b}
+  (H1 : left_inverse g1 f) (H2 : right_inverse g2 f) : g1 ~ g2 :=
+eq_on_of_left_inv_of_right_inv (mapsto g2) H1 H2
+
+/- inverse -/
+
+-- g is an inverse to f
+definition is_inverse (g : map b a) (f : map a b) : Prop := left_inverse g f ∧ right_inverse g f
+
+theorem bijective_of_is_inverse {g : map b a} {f : map a b} (H : is_inverse g f) : bijective f :=
+and.intro
+  (injective_of_left_inverse (and.left H))
+  (surjective_of_right_inverse (and.right H))
+
+end map

library/data/set/set.md

@@ -3,4 +3,7 @@ data.set
 
 Subsets of an arbitrary type.
 
-* [basic](basic.lean)
+* [basic](basic.lean) : unions, intersections, etc.
+* [function](function.lean) : functions from one set to another
+* [map](map.lean) : set functions bundled with their domain and codomain
+* [classical_inverse](classical_inverse.lean) : inverse functions, defined classically