Module mathcomp.classical.functions

From mathcomp Require Import boot order finmap ssralg ssrnum ssrint rat.
From HB Require Import structures.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets.
Add Search Blacklist "__canonical__".
Add Search Blacklist "__functions_".
Add Search Blacklist "_factory_".
Add Search Blacklist "_mixin_".

# Theory of functions This file provides a theory of functions $f : A\to B$ whose domain $A$ and codomain $B$ are represented by sets. ``` set_fun A B f == f : aT -> rT is a function with domain A : set aT and codomain B : set rT set_surj A B f == f is surjective set_inj A B f == f is injective set_bij A B f == f is bijective {fun A >-> B} == type of functions f : aT -> rT from A : set aT to B : set rT `funS f` is a proof of `set_fun A B f`. {oinv aT >-> rT} == type of functions with a partial inverse {oinvfun A >-> B} == combination of {fun A >-> B} and {oinv aT >-> rT} {inv aT >-> rT} == type of functions with an inverse f ^-1 == inverse of f : {inv aT >-> rT} {invfun A >-> B} == combination of {fun A >-> B} and {inv aT >-> rT} {surj A >-> B} == type of surjective functions {surjfun A >-> B} == combination of {fun A >-> B} and {surj A >-> B} {splitsurj A >-> B} == type of surjective functions with an inverse {splitsurjfun A >-> B} == combination of {fun A >-> B} and {splitsurj A >-> B} {inj A >-> rT} == type of injective functions {injfun A >-> B} == combination of {fun A >-> B} and {inj A >-> rT} {splitinj A >-> B} == type of injective functions with an inverse {splitinjfun A >-> B} == combination of {fun A >-> B} and {splitinj A >-> B} {bij A >-> B} == combination of {injfun A >-> B} and {surjfun A >-> B} {splitbij A >-> B} == combination of {splitinj A >-> B} and {splitsurj A >-> B} 'inj_ f == proof of {in A &, injective f} where f has type {splitinj A >-> _} ``` ``` [fun f in A] == the function f from the set A to the set f @` A with f : aT -> rT and A : set aT This is a notation for funin A f, which is an HB alias. 'split_ d f == partial injection from aT : Type to rT : Type, f : aT -> rT, and d : rT -> aT This is a notation for split_ d f which is an HB alias. split := 'split_(fun=> point) @to_setT T == function that associates to x : T a dependent pair of x with a proof that x belongs to setT (i.e., the type set_type [set: T]) incl AB == identity function from T to T, where AB is a proof of A `<=` B, with A, B : set T inclT A := incl (@subsetT _ _) eqincl AB == identity function from T to T, where AB is a proof of A = B, with A, B : set T mkfun fAB == builds a function {fun A >-> B} given a function f : aT -> rT and a proof fAB that {homo f : x / A x >-> B x} @set_val T A == injection from set_type A to T, where A has type set T @ssquash T == function of type {splitsurj [set: T] >-> [set: $| T |]} @finset_val T X == function that turns an element x : X (with X : {fset T}) into a dependent pair of x with a proof that x belongs to X (i.e., the type set_type [set` X]) @val_finset T X == function of type [set` X] -> X with X : {fset T} that cancels finset_val glue XY AB f g == function that behaves as f over X, as g over Y XY is a proof that sets X and Y are disjoint, AB is a proof that sets A and B are disjoint, A and B are intended to be the ranges of f and g 'pinv_ d A f == inverse of the function [fun f in A] over f @` A, function d outside of f @` A This is a notation for pinv_ which is defined as the inverse of a partial injection ('split_). pinv := 'pinv_(fun=> point) ``` ## Function restriction ``` patch d A f == "partial function" that behaves as the function f over the set A and as the function d otherwise restrict D f := patch (fun=> point) D f f \_ D := restrict D f sigL A f == "left restriction"; given a set A : set U and a function f : U -> V, returns the corresponding function of type set_type A -> V sigR A f == "right restriction"; given a set B : set V and a function f : {fun [set: U] >-> B}, returns the corresponding function of type U -> set_type B sigLR A B f == the function of type set_type A -> set_type B corresponding to f : {fun A >-> B} valL_ v == function cancelled by sigL A, with A : set U and v : V valR f == the function of type U -> V corresponding to f : U -> set_type B, with B : set V valR_fun == the function of type {fun [set: U] >-> B} corresponding to f : U -> set_type B, with B : set V valLR v f == the function of type U -> V corresponding to f : set_type A -> set_type B (where v : V), i.e., 'valL_ v \o valR_fun valLfun_ v A B f := [fun of valL_ f] with f : {fun [set: A] >-> B} valL := 'valL_ point valLRfun v := 'valLfun_ v \o valR_fun ``` ``` Section function_space == canonical nmodType, zmodType, ringType, comRingType, and lmodType structures for functions whose range is nmodType, zmodType, ringType, comRingType, and lmodType resp. fctE == multi-rule for fct ``` ``` linfun E F s == membership predicate for linear functions of type E -> F with scalar operator s : K -> F -> F E and F have type lmodType K. This is used in particular to attach a type of lmodType to {linear E -> F | s}. linfun_spec f == specification for membership of the linear function f ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Reserved Notation "f \_ D" (at level 10).
Reserved Notation "'{' 'fun' A '>->' B '}'"
  (format "'{' 'fun' A '>->' B '}'").
Reserved Notation "'{' 'oinv' T '>->' U '}'"
  (format "'{' 'oinv' T '>->' U '}'").
Reserved Notation "'{' 'inv' T '>->' U '}'"
  (format "'{' 'inv' T '>->' U '}'").
Reserved Notation "'{' 'oinvfun' T '>->' U '}'"
  (format "'{' 'oinvfun' T '>->' U '}'").
Reserved Notation "'{' 'invfun' T '>->' U '}'"
  (format "'{' 'invfun' T '>->' U '}'").
Reserved Notation "'{' 'inj' A '>->' T '}'"
  (format "'{' 'inj' A '>->' T '}'").
Reserved Notation "'{' 'splitinj' A '>->' T '}'"
  (format "'{' 'splitinj' A '>->' T '}'").
Reserved Notation "'{' 'surj' A '>->' B '}'"
  (format "'{' 'surj' A '>->' B '}'").
Reserved Notation "'{' 'splitsurj' A '>->' B '}'"
  (format "'{' 'splitsurj' A '>->' B '}'").
Reserved Notation "'{' 'injfun' A '>->' B '}'"
  (format "'{' 'injfun' A '>->' B '}'").
Reserved Notation "'{' 'surjfun' A '>->' B '}'"
  (format "'{' 'surjfun' A '>->' B '}'").
Reserved Notation "'{' 'splitinjfun' A '>->' B '}'"
  (format "'{' 'splitinjfun' A '>->' B '}'").
Reserved Notation "'{' 'splitsurjfun' A '>->' B '}'"
  (format "'{' 'splitsurjfun' A '>->' B '}'").
Reserved Notation "'{' 'bij' A '>->' B '}'"
  (format "'{' 'bij' A '>->' B '}'").
Reserved Notation "'{' 'splitbij' A '>->' B '}'"
  (format "'{' 'splitbij' A '>->' B '}'").

Reserved Notation "[ 'fun' 'of' f ]" (format "[ 'fun' 'of' f ]").
Reserved Notation "[ 'fun' f 'in' A ]" (format "[ 'fun' f 'in' A ]").
Reserved Notation "[ 'oinv' 'of' f ]" (format "[ 'oinv' 'of' f ]").
Reserved Notation "[ 'inv' 'of' f ]" (format "[ 'inv' 'of' f ]").
Reserved Notation "[ 'oinv' 'of' f ]" (format "[ 'oinv' 'of' f ]").
Reserved Notation "[ 'inv' 'of' f ]" (format "[ 'inv' 'of' f ]").
Reserved Notation "[ 'inj' 'of' f ]" (format "[ 'inj' 'of' f ]").
Reserved Notation "[ 'splitinj' 'of' f ]" (format "[ 'splitinj' 'of' f ]").
Reserved Notation "[ 'surj' 'of' f ]" (format "[ 'surj' 'of' f ]").
Reserved Notation "[ 'splitsurj' 'of' f ]" (format "[ 'splitsurj' 'of' f ]").
Reserved Notation "[ 'injfun' 'of' f ]" (format "[ 'injfun' 'of' f ]").
Reserved Notation "[ 'surjfun' 'of' f ]" (format "[ 'surjfun' 'of' f ]").
Reserved Notation "[ 'splitinjfun' 'of' f ]"
  (format "[ 'splitinjfun' 'of' f ]").
Reserved Notation "[ 'splitsurjfun' 'of' f ]"
  (format "[ 'splitsurjfun' 'of' f ]").
Reserved Notation "[ 'bij' 'of' f ]" (format "[ 'bij' 'of' f ]").
Reserved Notation "[ 'splitbij' 'of' f ]" (format "[ 'splitbij' 'of' f ]").

Reserved Notation "''oinv_' f" (at level 8, f at level 2, format "''oinv_' f").
Reserved Notation "''funS_' f" (at level 8, f at level 2, format "''funS_' f").
Reserved Notation "''mem_fun_' f"
  (at level 8, f at level 2, format "''mem_fun_' f").
Reserved Notation "''oinvK_' f"
  (at level 8, f at level 2, format "''oinvK_' f").
Reserved Notation "''oinvS_' f"
  (at level 8, f at level 2, format "''oinvS_' f").
Reserved Notation "''oinvP_' f"
  (at level 8, f at level 2, format "''oinvP_' f").
Reserved Notation "''oinvT_' f"
  (at level 8, f at level 2, format "''oinvT_' f").
Reserved Notation "''invK_' f"
  (at level 8, f at level 2, format "''invK_' f").
Reserved Notation "''invS_' f"
  (at level 8, f at level 2, format "''invS_' f").
Reserved Notation "''funoK_' f"
  (at level 8, f at level 2, format "''funoK_' f").
Reserved Notation "''inj_' f"
  (at level 8, f at level 2, format "''inj_' f").
Reserved Notation "''funK_' f"
  (at level 8, f at level 2, format "''funK_' f").
Reserved Notation "''totalfun_' A"
  (at level 8, A at level 2, format "''totalfun_' A").
Reserved Notation "''surj_' f"
  (at level 8, f at level 2, format "''surj_' f").
Reserved Notation "''split_' a"
  (at level 8, a at level 2, format "''split_' a").
Reserved Notation "''bijTT_' f"
  (at level 8, f at level 2, format "''bijTT_' f").
Reserved Notation "''bij_' f" (at level 8, f at level 2, format "''bij_' f").
Reserved Notation "''valL_' v" (at level 8, v at level 2, format "''valL_' v").
Reserved Notation "''valLfun_' v"
  (at level 8, v at level 2, format "''valLfun_' v").
Reserved Notation "''pinv_' dflt"
  (at level 8, dflt at level 2, format "''pinv_' dflt").
Reserved Notation "''pPbij_' dflt"
  (at level 8, dflt at level 2, format "''pPbij_' dflt").
Reserved Notation "''pPinj_' dflt"
  (at level 8, dflt at level 2, format "''pPinj_' dflt").
Reserved Notation "''injpPfun_' dflt"
  (at level 8, dflt at level 2, format "''injpPfun_' dflt").
Reserved Notation "''funpPinj_' dflt"
  (at level 8, dflt at level 2, format "''funpPinj_' dflt").

Local Open Scope classical_set_scope.

Section MainProperties.
Context { } ( : set aT) ( : set rT) ( : aT -> rT).
Definition := {homo f : / A x >-> B x}.
Definition := B `<=` f @` A.
Definition := {in A &, injective f}.
Definition := [/\ set_fun, set_inj & set_surj].
End MainProperties.

. ( aT) (B : set rT) (f : aT -> rT) :=
  { funS : set_fun A B f }.
. ( aT) (B : set rT) :=
  { of isFun _ _ A B f }.
Notation := (@Fun.type _ _ A B) : form_scope.
Notation := [the {fun _ >-> _} of f : _ -> _] : form_scope.

. ( -> rT) := { oinv : rT -> option aT }.
. of OInv aT rT f}.
Notation := (@OInversible.type aT rT) : type_scope.
Notation := [the {oinv _ >-> _} of f : _ -> _] :
  form_scope.
Definition ( : {oinv aT >-> rT})
  & phantom (_ -> _) f := @oinv _ _ f.
Notation := (@phant_oinv _ _ _ (Phantom (_ -> _) f%FUN)).

.
  { of OInv aT rT f & isFun aT rT A B f}.
Notation := (@OInvFun.type _ _ A B) : type_scope.
Notation :=
  [the {oinvfun _ >-> _} of f : _ -> _] : form_scope.

. ( -> rT) & OInv _ _ f := {
  inv : rT -> aT;
  oliftV : olift inv = 'oinv_f
}.

. ( -> rT) := { inv : rT -> aT }.
. ( -> rT) & Inv _ _ f.
  ..Build _ _ f (olift inv).
  ..Build _ _ f erefl.
..

. of Inv aT rT f}.
Notation := (@Inversible.type aT rT) : type_scope.
Notation := [the {inv _ >-> _} of f : _ -> _] : form_scope.
Definition ( : {inv aT >-> rT}) & phantom (_ -> _) f :=
  @inv _ _ f.
Notation := (@inv _ _ f%function) (only printing) : function_scope.
Notation :=
  (@phant_inv _ _ _ (Phantom (_ -> _) f%function)) : function_scope.

.
  { of Inv aT rT f & isFun aT rT A B f}.
Notation := (@InvFun.type _ _ A B) : type_scope.
Notation :=
  [the {invfun _ >-> _} of f : _ -> _] : form_scope.

. aT} {B : set rT}
  (f : aT -> rT) & OInv _ _ f := {
    oinvS : {homo 'oinv_f : / B x >-> (some @` A) x};
    oinvK : {in B, ocancel 'oinv_f f};
  }.

. aT} {B : set rT} (f : aT -> rT) := {
    oinv; oinvS : {homo oinv : / B x >-> (some @` A) x};
          oinvK : {in B, ocancel oinv f};
  }.
. aT} {B : set rT} (f : aT -> rT)
   & OCanV _ _ A B f.
..Build _ _ f oinv.
..Build _ _ A B f oinvS oinvK.
..

. of @OCanV aT rT A B f}.
Notation := (@Surject.type _ _ A B) : type_scope.
Notation :=
  [the {surj _ >-> _} of f : _ -> _] : form_scope.

.
  { of @Surject aT rT A B f & @Fun _ _ A B f}.
Notation := (@SurjFun.type _ _ A B) : type_scope.
Notation :=
  [the {surjfun _ >-> _} of f : _ -> _] : form_scope.

.
  { of @Surject aT rT A B f & @Inv _ _ f}.
Notation := (@SplitSurj.type _ _ A B) : type_scope.
Notation :=
  [the {splitsurj _ >-> _} of f : _ -> _] : form_scope.

.
   { of @SplitSurj aT rT A B f & @Fun _ _ A B f}.
Notation :=
  (@SplitSurjFun.type _ _ A B) : type_scope.
Notation :=
  [the {splitsurjfun _ >-> _} of f : _ -> _] : form_scope.

. ( aT) (f : aT -> rT) & OInv _ _ f :=
  { funoK : {in A, pcancel f 'oinv_f} }.

.
  { of OInv aT rT f & OInv_Can aT rT A f}.
Notation := (@Inject.type _ rT A) : type_scope.
Notation := [the {inj _ >-> _} of f : _ -> _] : form_scope.

. ( aT) (B : set rT) :=
   { of @Fun _ _ A B f & @Inject _ _ A f }.
Notation := (@InjFun.type _ _ A B) : type_scope.
Notation :=
  [the {injfun _ >-> _} of f : _ -> _] : form_scope.

. ( aT) :=
  { of @Inv aT rT f & @Inject aT rT A f}.
Notation := (@SplitInj.type _ rT A) : type_scope.
Notation :=
  [the {splitinj _ >-> _} of f : _ -> _] : form_scope.

. ( aT) (B : set rT) :=
  { of @SplitInj _ rT A f & @isFun _ _ A B f}.
Notation := (@SplitInjFun.type _ _ A B) : type_scope.
Notation :=
  [the {splitinjfun _ >-> _} of f : _ -> _] : form_scope.

. aT} {B : set rT} :=
   { of @InjFun _ _ A B f & @SurjFun _ _ A B f}.
Notation := (@Bij.type _ _ A B) : type_scope.
Notation := [the {bij _ >-> _} of f] : form_scope.

. aT} {B : set rT} :=
   { of @SplitInjFun _ _ A B f & @SplitSurjFun _ _ A B f}.
Notation := (@SplitBij.type _ _ A B) : type_scope.
Notation := [the {splitbij _ >-> _} of f] : form_scope.

Module .
Notation := {fun A >-> B} (at level 70) : type_scope.
Notation := {oinv aT >-> rT} (at level 70) : type_scope.
Notation := {oinvfun A >-> B} (at level 70) : type_scope.
Notation := {inv aT >-> rT} (at level 70) : type_scope.
Notation := {invfun A >-> B} (at level 70) : type_scope.
Notation := {surj A >-> B} (at level 70) : type_scope.
Notation := {surjfun A >-> B} (at level 70) : type_scope.
Notation := {splitsurj A >-> B} (at level 70) : type_scope.
Notation := {splitsurjfun A >-> B} (at level 70) : type_scope.
Notation := {inj A >-> rT} (at level 70) : type_scope.
Notation := {injfun A >-> B} (at level 70) : type_scope.
Notation := {splitinj A >-> rT} (at level 70) : type_scope.
Notation := {splitinjfun A >-> B} (at level 70) : type_scope.
Notation := {bij A >-> B} (at level 70) : type_scope.
Notation := {splitbij A >-> B} (at level 70) : type_scope.
End ShortFunSyntax.

## Theory

Definition ( : set aT) ( : set rT)
  ( : {fun A >-> B}) & phantom (_ -> _) f := @funS _ _ _ _ f.
Notation := (phant_funS (Phantom (_ -> _) f))
  (at level 8, f at level 2) : form_scope.
#[global] Hint Extern 0 (set_fun _ _ _) => solve [apply: funS] : core.
#[global] Hint Extern 0 (prop_in1 _ _) => solve [apply: funS] : core.

Definition ( : set aT) ( : set rT) ( : {fun A >-> B}) :=
  image_subP.2 (@funS _ _ _ _ f).
Arguments fun_image_sub {aT rT A B}.
#[global] Hint Extern 0 (_ @` _ `<=` _) => solve [apply: fun_image_sub] : core.

Definition ( : set aT) ( : set rT) ( : {fun A >-> B}) :=
  homo_setP.2 (@funS _ _ _ _ f).
#[global] Hint Extern 0 (prop_in1 _ _) => solve [apply: mem_fun] : core.

Definition ( : set aT) ( : set rT)
  ( : {fun A >-> B}) & phantom (_ -> _) f := homo_setP.2 (@funS _ _ _ _ f).
Notation := (phant_mem_fun (Phantom (_ -> _) f))
  (at level 8, f at level 2) : form_scope.

Lemma { } ( : {inv aT >-> rT}) : Some (f^-1 x) = 'oinv_f x.

Proof.

by rewrite -oliftV. Qed.

Definition ( : set aT) ( : set rT)
   ( : {surj A >-> B}) & phantom (_ -> _) f := @oinvK _ _ _ _ f.
Notation := (phant_oinvK (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve oinvK : core.

Definition ( : set aT) ( : set rT)
   ( : {surj A >-> B}) & phantom (_ -> _) f := @oinvS _ _ _ _ f.
Notation := (phant_oinvS (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve oinvS : core.

Variant {} {} { : set aT} { : set rT} ( : {surj A >-> B}) :
   rT -> option aT -> Type :=
   ( : aT) of A x & f x = y : oinv_spec f y (f x) (Some x).

Lemma ( : set aT) ( : set rT) ( : {surj A >-> B}) :
  B y -> oinv_spec f y y ('oinv_f y).

Proof.

move=> By; have :='oinvK_f (mem_set By).
by have /cid2 [x Ax <-] := 'oinvS_f By => <-; constructor.
Qed.

Definition ( : set aT) ( : set rT)
( : {surj A >-> B}) & phantom (_ -> _) f := @oinvP _ _ _ _ f.
Notation := (phant_oinvP (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve oinvP : core.

Lemma { } { : set aT} { : set rT} { : {surj A >-> B}} :
B x -> 'oinv_f x.

Proof.

by move=> /'oinvS_f [a Aa <-]. Qed.

Definition ( : set aT) ( : set rT)
( : {surj A >-> B}) & phantom (_ -> _) f := @oinvT _ _ _ _ f.
Notation := (phant_oinvT (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve oinvT : core.

Lemma { } { : set aT} { : set rT} { : {splitsurj A >-> B}} :
{in B, cancel f^-1 f}.

Proof.

by move=> x Bx; rewrite -[x in RHS]'oinvK_f// -some_inv/=. Qed.

Definition ( : set aT) ( : set rT)
( : {splitsurj A >-> B}) & phantom (_ -> _) f := @invK _ _ _ _ f.
Notation := (phant_invK (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve invK : core.

Lemma { } { : set aT} { : set rT} { : {splitsurj A >-> B}} :
{homo f^-1 : / B x >-> A x}.

Proof.

by move=> x /'oinvS_f/= [a Aa]; rewrite -some_inv => -[<-]. Qed.

Definition ( : set aT) ( : set rT)
   { : {splitsurjfun A >-> B}} & phantom (_ -> _) f := @invS _ _ _ _ f.
Notation := (phant_invS (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve invS : core.

Definition ( : set aT) ( : {inj A >-> rT})
  & phantom (_ -> _) f := @funoK _ _ _ f.
Notation := (phant_funoK (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve funoK : core.

Definition { : nonPropType} { : set aT} { : {inj A >-> rT}} :
   {in A &, injective f} := pcan_in_inj funoK.
Definition ( : set aT) ( : {inj A >-> rT}) &
   phantom (_ -> _) f := @inj _ _ _ f.
Notation := (phant_inj (Phantom (_ -> _) f)) : form_scope.

Definition { } { : set aT} { : {inj A >-> rT}} :
   {in A &, injective f} := inj.
#[global] Hint Extern 0 {in _ &, injective _} => solve [apply: inj_hint] : core.
#[global] Hint Extern 0 (set_inj _ _) => solve [apply: inj_hint] : core.

Lemma { } { : {inj [set: aT] >-> rT}} : injective f.

Proof.

by apply: in2TT; apply: inj. Qed.

#[global] Hint Extern 0 (injective _) => solve [apply: injT] : core.

Lemma { : Type} { : set aT} { : {splitinj A >-> rT}} :
{in A, cancel s s^-1}.

Proof.

by move=> x Ax; apply: Some_inj; rewrite some_inv funoK. Qed.

Definition ( : set aT) ( : {splitinj A >-> rT})
& phantom (_ -> _) f := @funK _ _ _ f.
Notation := (phant_funK (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Resolve funK : core.

Structure Equality

Lemma { } { : set aT} { : set rT} ( : {fun A >-> B}) :
f = g <-> f =1 g.

Proof.

case: f g => [f [[ffun]]] [g [[gfun]]]/=; split=> [[->//]|/funext eqfg].
rewrite eqfg in ffun *; congr {| Fun.sort := _; Fun.class := {|
Fun.functions_isFun_mixin := {|isFun.funS := _|}|}|}.
exact: Prop_irrelevance.
Qed.

Preliminary Builders

. aT} (f : aT -> rT) & Inv _ _ f :=
{ funK : {in A, cancel f f^-1} }.
. ( -> rT) & @Inv_Can _ _ A f.
Local Lemma : {in A, pcancel f 'oinv_f}.

Proof.

by rewrite -oliftV/=; apply: can_in_pcan; apply: funK. Qed.

  ..Build _ _ A f funoK.
..

. aT} {B : set rT} (f : aT -> rT)
     & Inv aT rT f := {
  invS : {homo f^-1 : / B x >-> A x};
  invK : {in B, cancel f^-1 f};
}.
. aT} {B : set rT} (f : aT -> rT)
    & Inv_CanV _ _ A B f.
  #[local] Lemma : {in B, ocancel 'oinv_f f}.

Proof.

by move=> x Bx; rewrite -some_inv/= invK. Qed.

#[local] Lemma : {homo 'oinv_f : / B x >-> (some @` A) x}.

Proof.

by move=> x /invS Af'x; exists (f^-1 x); rewrite // -some_inv. Qed.

..Build _ _ _ _ f oinvS oinvK.
..

Trivial instances

Section OInverse.
Context { : Type} { : set aT} { : set rT}.

. aT >-> rT}} :=
OInv.Build _ _ 'oinv_f (omap f).

Lemma { : {oinv aT >-> rT}} : 'oinv_('oinv_f) = omap f.

Proof.

by []. Qed.

. ( A >-> B}) :=
isFun.Build rT (option aT) B (some @` A) 'oinv_f oinvS.

Lemma ( : {surj A >-> B}) : OInv_Can _ _ B 'oinv_f.

Proof.

split=> x Bx/=; rewrite -[x in RHS]('oinvK_f Bx).
by have := 'oinvT_f (set_mem Bx); case: 'oinv_f.
Qed.

. f.

Lemma ( : {injfun A >-> B}) :
OInv_CanV _ _ B (some @` A) 'oinv_f.

Proof.

split=> [_|_ /set_mem] [a Aa <-]/=; last by rewrite funoK ?inE.
by exists (f a) => //; apply: funS.
Qed.

. ( A >-> B}) := injoinv_surj_subproof f.

. A >-> B}} := InjFun.on 'oinv_f.

End OInverse.

Section Inverse.
Context { : Type} { : set aT} { : set rT}.

. ( aT >-> rT}) := Inv.Build rT aT f^-1 f.
. ( aT >-> rT}) := Inversible.copy inv f^-1.

Lemma ( : {inv aT >-> rT}) : f^-1^-1 = f

Proof.

by []. Qed.

. ( A >-> B}) :=
  isFun.Build rT aT B A f^-1 invS.
. ( A >-> B}) := Fun.copy inv f^-1.
. A >-> B}} :=
  Inv_Can.Build _ _ _ f^-1 'invK_f.
. ( A >-> B}) :=
  Inv_CanV.Build _ _ _ _ f^-1 funS funK.
. A >-> B}} := InjFun.on f^-1.

End Inverse.

Section Some.
Context {} { : set T}.

..Build _ _ (@Some T) id.

Lemma : 'oinv_(@Some T) = id

Proof.

by []. Qed.

Lemma : @OInv_Can _ _ A (@Some T)

Proof.

by split. Qed.

..

Lemma : OInv_CanV _ _ A (some @` A) (@Some T).

Proof.

by split=> [x|x /set_mem] [a Aa <-]//=; exists a. Qed.

. .

Lemma : isFun _ _ A (some @` A) (@Some T).

Proof.

by split=> x; exists x. Qed.

..

End Some.

Section OApply.
Context { } { : set aT} { : set rT} { : rT}.
Local Notation f := (oapp f b0).

. aT >-> rT}} :=
Inv.Build _ _ (oapp f) 'oinv_f.

Lemma { : {oinv aT >-> rT}} : (oapp f)^-1 = 'oinv_f.

Proof.

by []. Qed.

Lemma { : {oinv aT >-> rT}} : 'oinv_(oapp f) = olift 'oinv_f.

Proof.

by rewrite -inv_oapp. Qed.

Lemma { : {inv aT >-> rT}} : olift f^-1 = (oapp f)^-1.

Proof.

by rewrite inv_oapp -oliftV. Qed.

Lemma ( : {inj A >-> rT}) : Inv_Can _ _ (some @` A) (oapp f).

Proof.

by split=> x /set_mem[a Aa <-]/=; rewrite inv_oapp funoK ?inE. Qed.

. f.

Lemma ( : {surj A >-> B}) : Inv_CanV _ _ (some @` A) B (oapp f).

Proof.

by split=> [b|b /set_mem] Bb/=; rewrite inv_oapp; case: oinvP => // x; exists x.
Qed.

. f.

Lemma ( : {fun A >-> B}) : isFun _ _ (some @` A) B (oapp f).

Proof.

by split=> x [a Aa <-] /=; apply: funS. Qed.

. f.
. ( A >-> B}) := Fun.on (oapp f).
. ( A >-> B}) := Fun.on (oapp f).
. ( A >-> B}) := Fun.on (oapp f).
. ( A >-> B}) := Fun.on (oapp f).

End OApply.

Section OBind.
Context { } { : set aT} { : set (option rT)}.
Local Notation f := (oapp f None).
Local Notation := (option rT).

. aT >-> orT}} :=
Inv.Build _ _ (obind f) 'oinv_f.

Lemma { : {oinv aT >-> orT}} : (obind f)^-1 = 'oinv_f.

Proof.

by []. Qed.

Lemma { : {oinv aT >-> orT}} : 'oinv_(obind f) = olift 'oinv_f.

Proof.

by []. Qed.

Lemma { : {inv aT >-> orT}} : (obind f)^-1 = olift f^-1.

Proof.

by rewrite inv_obind -oliftV. Qed.

. ( A >-> B}) := Fun.copy (obind f) (b f).
. ( A >-> orT}) := Inject.copy (obind f) (b f).
. ( A >-> B}) := Fun.on (obind f).
. ( A >-> B}) := Surject.copy (obind f) (b f).
. ( A >-> B}) := Fun.on (obind f).
. ( A >-> B}) := Fun.on (obind f).
End OBind.

Section Composition.
Context { } { : set aT} { : set rT} { : set sT}.

Local Lemma ( : {fun A >-> B}) ( : {fun B >-> C}) :
isFun _ _ A C (g \o f).

Proof.

by split => x /'funS_f; apply: funS. Qed.

. f g.

Section OInv.
Context { : {oinv aT >-> rT}} { : {oinv rT >-> sT}}.
..Build _ _ (g \o f) (obind 'oinv_f \o 'oinv_g).
Lemma : 'oinv_(g \o f) = (obind 'oinv_f) \o 'oinv_g.

Proof.

by []. Qed.

End OInv.

Section OInv.
Context { : {inv aT >-> rT}} { : {inv rT >-> sT}}.
Lemma : olift (f^-1 \o g^-1) = 'oinv_(g \o f).

Proof.

by rewrite funeqE => x; rewrite oinv_comp -!oliftV. Qed.

..Build aT sT (g \o f) some_comp_inv.
Lemma : (g \o f)^-1 = f^-1 \o g^-1

Proof.

by []. Qed.

End OInv.

Lemma ( : {injfun A >-> B}) ( : {inj B >-> sT}) :
OInv_Can aT sT A (g \o f).

Proof.

by split=> x Ax; rewrite oinv_comp/= funoK ?mem_fun//= funoK. Qed.

. f g.

. ( A >-> B}) (g : {injfun B >-> C}) :=
  Inject.on (g \o f).
. ( A >-> B})
  (g : {splitinj B >-> sT}) := Inject.on (g \o f).
. ( A >-> B})
  (g : {splitinjfun B >-> C}) := Inject.on (g \o f).
End Composition.

Section Composition.
Context { } { : set aT} { : set rT} { : set sT}.

Lemma ( : {surj A >-> B}) ( : {surj B >-> C}) :
  OInv_CanV _ _ A C (g \o f).

Proof.

split; first exact: funS.
apply: (@ocan_in_comp _ _ _ (mem B)) oinvK oinvK.
by move=> ? /set_mem; rewrite pred_oapp_set inE; apply: funS.
Qed.

. f g.
. ( A >-> B}) (g : {splitsurj B >-> C}) :=
  Surject.on (g \o f).
. ( A >-> B}) (g : {surjfun B >-> C}) :=
  Surject.on (g \o f).
. ( A >-> B})
  (g : {splitsurjfun B >-> C}) := Surject.on (g \o f).
. ( A >-> B}) (g : {bij B >-> C}) :=
  Surject.on (g \o f).
. ( A >-> B}) (g : {splitbij B >-> C}) :=
  Surject.on (g \o f).

End Composition.

Section totalfun.
Context { : Type}.
Definition ( : set aT) ( : aT -> rT) := f.
Context { : set aT}.
Local Notation := (totalfun_ A).
. ( -> rT) :=
  isFun.Build _ _ A setT (totalfun f) (fun _ _ => I).
. ( A >-> rT}) := Inject.on (totalfun f).
. ( A >-> rT}) := SplitInj.on (totalfun f).
. ( A >-> [set: rT]}) :=
  Surject.on (totalfun f).
. ( A >-> [set: rT]}) :=
  SplitSurj.on (totalfun f).
End totalfun.
Notation := (totalfun_ A) : form_scope.
Notation := (totalfun_ setT).

Section Olift.
Context { } { : set aT} { : set rT}.

. aT >-> rT}} := OInversible.copy (olift f)
  (Some \o f).

Lemma { : {oinv aT >-> rT}} : 'oinv_(olift f) = obind 'oinv_f.

Proof.

by []. Qed.

. ( A >-> rT}) :=
  Inject.copy (olift f) (Some \o ('totalfun_A f)).
. ( A >-> B}) :=
  Surject.copy (olift f) (Some \o f).
. ( A >-> B}) := Fun.copy (olift f) (Some \o f).
. ( A >-> B}) := Fun.on (olift f).
. ( A >-> B}) := Fun.on (olift f).
. ( A >-> B}) := Fun.on (olift f).
. ( A >-> B}) := Fun.on (olift f).

End Olift.

Section Map.
Context { } { : set aT} { : set rT}.
Local Notation f := (obind (olift f)).

. ( A >-> B}) := Fun.copy (omap f) (m f).

. aT >-> rT}} :=
  Inv.Build _ _ (omap f) (obind 'oinv_f).

Lemma { : {oinv aT >-> rT}} : (omap f)^-1 = obind 'oinv_f.

Proof.

by []. Qed.

Lemma { : {oinv aT >-> rT}} : 'oinv_(omap f) = olift (obind 'oinv_f).

Proof.

by []. Qed.

Lemma { : {inv aT >-> rT}} : omap f^-1 = (omap f)^-1.

Proof.

by rewrite inv_omap -oliftV. Qed.

. ( A >-> B}) := Fun.on (omap f).
. ( A >-> rT}) := Inject.copy (omap f) (m f).
. ( A >-> B}) := Fun.on (omap f).
. ( A >-> B}) := Surject.copy (omap f) (m f).
. ( A >-> B}) := Fun.on (omap f).
. ( A >-> B}) := Fun.on (omap f).
End Map.

Builders

. aT} {B : set rT} (f : aT -> rT) :=
  { inv; invS : {homo inv : / B x >-> A x}; invK : {in B, cancel inv f}; }.
. aT} {B : set rT} (f : aT -> rT) & CanV _ _ A B f.
..Build _ _ f inv.
..Build _ _ _ _ f invS invK.
..

. aT} {B : set rT} (f : aT -> rT) &
  @OInv _ _ f :=
  {
    funS : {homo f : / A x >-> B x};
    oinvS : {homo 'oinv_f : / B x >-> (some @` A) x};
    funoK : {in A, pcancel f 'oinv_f};
    oinvK : {in B, ocancel 'oinv_f f};
  }.
. ( -> rT) & OInv_Can2 _ _ A B f.
  ..Build aT rT _ _ f funS.
  ..Build aT rT _ f funoK.
  ..Build aT rT _ _ f oinvS oinvK.
..

. aT} {B : set rT} (f : aT -> rT) :=
   { oinv; funS : {homo f : / A x >-> B x};
           oinvS : {homo oinv : / B x >-> (some @` A) x};
           funoK : {in A, pcancel f oinv};
           oinvK : {in B, ocancel oinv f};
   }.
. ( -> rT) & OCan2 _ _ A B f.
  ..Build aT rT f oinv.
  ..Build aT rT _ _ f funS oinvS funoK oinvK.
..

. aT} (f : aT -> rT) :=
  { inv; funK : {in A, cancel f inv} }.
. ( -> rT) & @Can _ _ A f.
..Build _ _ f inv.
..Build _ _ _ f funK.
..

. aT} {B : set rT} (f : aT -> rT) &
   Inv _ _ f :=
   { funS : {homo f : / A x >-> B x};
     invS : {homo f^-1 : / B x >-> A x};
     funK : {in A, cancel f f^-1};
     invK : {in B, cancel f^-1 f};
   }.
. ( -> rT) & Inv_Can2 _ _ A B f.
  ..Build aT rT A B f funS.
  ..Build aT rT A f funK.
  ..Build aT rT A B f invS invK.
..

. aT} {B : set rT} (f : aT -> rT) :=
  { inv; funS : {homo f : / A x >-> B x};
         invS : {homo inv : / B x >-> A x};
         funK : {in A, cancel f inv};
         invK : {in B, cancel inv f};
   }.
. ( -> rT) & Can2 _ _ A B f.
  ..Build aT rT f inv.
  ..Build aT rT A B f funS invS funK invK.
..

. aT} {B : set rT} (f : aT -> rT) &
     @SplitInjFun _ _ A B f :=
  { invS : {homo f^-1 : / B x >-> A x}; injV : {in B &, injective f^-1} }.
. aT} {B : set rT} (f : aT -> rT) & SplitInjFun_CanV _ _ A B f.
  Let := homo_setP.2 invS.
  Local Lemma : {in B, cancel f^-1 f}.

Proof.

by move=> x Bx; apply: injV; rewrite ?funK ?(mem_fun, mem_inv). Qed.

..Build aT rT A B f invS invK.
..

. ( -> rT) := { bij : bijective f }.
. aT rT f.
Local Lemma : { | cancel f g /\ cancel g f}.

Proof.

by apply: cid; case: bij => g; exists g. Qed.

  ..Build aT rT setT setT f
    (fun => y) (fun => y)
    (in1W (projT2 exg).1) (in1W (projT2 exg).2).
..

Fun in

Section surj_oinv.
Context { } { : set aT} { : set rT} { : aT -> rT} ( : set_surj A B f).

Let ( : rT) :=
if pselect (B y) is left By then some (projT1 (cid2 (fsurj By))) else None.

Lemma : {in B, ocancel surjective_oinv f}.

Proof.

by rewrite /surjective_oinv => x /set_mem ?; case: pselect => // ?; case: cid2.
Qed.

Lemma : set_fun B (some @` A) surjective_oinv.

Proof.

move=> y By /=; rewrite /surjective_oinv; case: pselect => // By'.
by case: cid2 => //= x Ax fxy; exists x.
Qed.

End surj_oinv.
Coercion { } { : set aT} { : set rT} { : aT -> rT}
( : set_surj A B f) :=
OCanV.Build aT rT A B f (surjective_oinvS fS) (surjective_oinvK fS).

Section Psurj.
Context { } { : set aT} { : set rT} { : aT -> rT} ( : set_surj A B f).

. _ _ A B f := fsurj.
Definition := [surj of f].

Lemma : { : {surj A >-> B} | f = s}

Proof.

by exists [surj of f]. Qed.

End Psurj.
Coercion surjection_of_surj : set_surj >-> Surject.type.

Lemma { } { : set aT} { : set rT} { : aT -> rT}
( : set_surj A B f) :
'oinv_fS y = if pselect (B y) is left By then some (projT1 (cid2 (fS y By))) else None.

Proof.

by []. Qed.

Lemma { } { : set aT} { : set rT} { : {surj A >-> B}} : set_surj A B f.

Proof.

by move=> b /'oinvP_f[x Ax _]; exists x. Qed.

Definition ( : set aT) ( : set rT) ( : {surj A >-> B})
& phantom (_ -> _) f := @surj _ _ _ _ f.
Notation := (phant_surj (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Extern 0 (set_surj _ _ _) => solve [apply: surj] : core.

Section funin_surj.
Context { : Type}.

Definition ( : set aT) ( : aT -> rT) := f.

Context { : set aT} { : set rT} ( : aT -> rT).

Lemma : set_fun A (f @` A) f.

Proof.

exact/image_subP. Qed.

.
.Build _ _ _ _ (funin A f) set_fun_image.

. _ _ A (f @` A) (funin A f) :=
((fun _ => id) : set_surj A (f @` A) f).

End funin_surj.
Notation := (funin A f) : function_scope.
#[global] Hint Resolve set_fun_image : core.

Partial injection

Section split.
Context { } ( : set aT) ( : set rT).
Definition ( : rT -> aT) ( : aT -> rT) := f.

Context ( : rT -> aT).
Local Notation := (split_ dflt).

. ( A >-> B}) := Fun.on (split f).

Section oinv.
Context ( : {oinv aT >-> rT}).
Let := odflt (dflt y) ('oinv_f y).
. .Build _ _ (split f) g.
Lemma : (split f)^-1 = g

Proof.

by []. Qed.

End oinv.
. ( A >-> B}) := Fun.on (split f).

Lemma ( : {inj A >-> rT}) : Inv_Can _ _ A (split f).

Proof.

by split=> x Ax; rewrite splitV funoK. Qed.

. f.
. ( A >-> B}) := Inject.on (split f).

Lemma ( : {splitinjfun A >-> B}) : (split f)^-1 = f^-1.

Proof.

by apply/funext => x; apply: Some_inj; rewrite splitV -oliftV. Qed.

Lemma ( : {surj A >-> B}) : Inv_CanV _ _ A B (split f).

Proof.

by split=> [+|+ /set_mem] => b Bb; rewrite splitV; case: oinvP. Qed.

. f.
. ( A >-> B}) := Surject.on (split f).
. ( A >-> B}) := Surject.on (split f).

End split.
Notation := (split_ a) : form_scope.
Notation := 'split_(fun=> point).

More Builders

. ( aT) (f : aT -> rT) :=
   { inj : {in A &, injective f} }.
. ( -> rT) & Inj _ _ A f.
  ..copy f [fun f in A].
  Lemma : {in A, pcancel f 'oinv_f}.

Proof.

  move=> x /set_mem Ax; rewrite oinv_surj.
  case: pselect => //=; last by case; exists x.
  by move=> ?; case: cid2 => //= y Ay /inj; rewrite !inE => ->.
  Qed.

  ..Build _ _ _ f funoK.
..

. aT} {B : set rT} (f : aT -> rT) &
   @SurjFun _ _ A B f := { inj : {in A &, injective f} }.
. aT} {B : set rT} (f : aT -> rT) &
    @SurjFun_Inj _ _ A B f.
  Let := f.
  ..Build _ _ A g inj.
  Let : OInv_Can aT rT A f.

Proof.

  split=> x /set_mem Ax; apply: 'inj_(omap g); rewrite ?mem_fun ?inE//=.
  by rewrite /g -oinvV/= funoK// ?mem_fun ?inE.
  Qed.

..
..

. aT} {B : set rT} (f : aT -> rT) &
     @SplitSurjFun _ _ A B f :=
   { inj : {in A &, injective f} }.
. aT} {B : set rT} (f : aT -> rT) &
    @SplitSurjFun_Inj _ _ A B f.
  Local Lemma : {in A, cancel f f^-1%FUN}.

Proof.

by move=> x Ax; apply: inj; rewrite ?invK ?mem_fun. Qed.

..Build aT rT _ f funK.
..

Section Inverses.
Context { : set aT} { : set rT}.
. ( A >-> rT}) :=
SurjFun_Inj.Build _ _ _ _ [fun f in A] 'inj_f.
End Inverses.

## Simple Factories

Section Pinj.
Context { } { : set aT} { : aT -> rT} ( : {in A &, injective f}).
..Build _ _ _ f finj.
Lemma : { : {inj A >-> rT} | f = i}

Proof.

by exists [inj of f]. Qed.

End Pinj.

Section Pfun.
Context { } { : set aT} { : set rT} { : aT -> rT}
( : {homo f : / A x >-> B x}).
Let : _ -> _ := f.
..Build _ _ _ _ g ffun.
Lemma : { : {fun A >-> B} | f = i}

Proof.

by exists [fun of g]. Qed.

End Pfun.

Section injPfun.
Context { } { : set aT} { : set rT} { : {inj A >-> rT}}
( : {homo f : / A x >-> B x}).
Let : _ -> _ := f.
..on g.
..Build _ _ A B g ffun.
Lemma : { : {injfun A >-> B} | f = i :> (_ -> _)}.

Proof.

by exists [injfun of g]. Qed.

End injPfun.

Section funPinj.
Context { } { : set aT} { : set rT} { : {fun A >-> B}}
( : {in A &, injective f}).
Let : _ -> _ := f.
..on g.
..Build _ _ _ g finj.
Lemma : { : {injfun A >-> B} | f = i}.

Proof.

by exists [injfun of g]; apply/funP. Qed.

End funPinj.

Section funPsurj.
Context { } { : set aT} { : set rT} { : {fun A >-> B}}
( : set_surj A B f).
Let : _ -> _ := f.
..on g.
. _ _ A B g := fsurj.
Lemma : { : {surjfun A >-> B} | f = s}.

Proof.

by exists [surjfun of g]; apply/funP. Qed.

End funPsurj.

Section surjPfun.
Context { } { : set aT} { : set rT} { : {surj A >-> B}}
( : {homo f : / A x >-> B x}).
Let : _ -> _ := f.
..on g.
..Build _ _ A B g ffun.
Lemma : { : {surjfun A >-> B} | f = s :> (_ -> _)}.

Proof.

by exists [surjfun of g]. Qed.

End surjPfun.

Section Psplitinj.
Context { } { : set aT} { : aT -> rT} {} ( : {in A, cancel f g}).
..Build _ _ A f funK.
Lemma : { : {splitinj A >-> rT} | f = i}.

Proof.

by exists [splitinj of f]. Qed.

End Psplitinj.

Section funPsplitinj.
Context { } { : set aT} { : set rT} { : {fun A >-> B}}.
Context {} ( : {in A, cancel f g}).
Let : _ -> _ := f.
..on f'.
..Build _ _ A f' funK.
Lemma : { : {splitinjfun A >-> B} | f = i}.

Proof.

by exists [splitinjfun of f']; apply/funP. Qed.

End funPsplitinj.

Lemma { } { : aT -> rT} {} : cancel f g ->
{ : {splitinj [set: aT] >-> rT} | f = i}.

Proof.

by move/in1W/Psplitinj. Qed.

Section funPsplitsurj.
Context { } { : set aT} { : set rT} { : {fun A >-> B}}.
Context { : {fun B >-> A}} ( : {in B, cancel g f}).
Let : _ -> _ := f.
..on f'.
..Build _ _ A B f' funS funK.
Lemma : { : {splitsurjfun A >-> B} | f = s :> (_ -> _)}.

Proof.

by exists [splitsurjfun of f']. Qed.

End funPsplitsurj.

Lemma { } { : aT -> rT} {} : cancel g f ->
{ : {splitsurjfun [set: aT] >-> [set: rT]} | f = s}.

Proof.

by move/in1W/(@funPsplitsurj _ _ _ _ [fun of totalfun f] [fun of totalfun g]).
Qed.

## Instances

The identity is a split bijection

..Build T T A A idfun idfun
(fun => y) (fun => y) (fun _ _ => erefl) (fun _ _ => erefl).

Iteration preserves Fun, Injectivity, and Surjectivity

Section iter_inv.

Context {} { : set aT}.

Local Lemma ( : {fun A >-> A}) : isFun _ _ A A (iter n f).

Proof.

split => x; elim: n => // n /[apply] ?; apply/(fun_image_sub f).
by exists (iter n f x).
Qed.

. n f.

Section OInv.
Context { : {oinv aT >-> aT}}.
..Build _ _ (iter n f)
(iter n (obind 'oinv_f) \o some).
Lemma : 'oinv_(iter n f) = iter n (obind 'oinv_f) \o some.

Proof.

by []. Qed.

End OInv.

Section OInv.
Context { : {inv aT >-> aT}}.
Lemma : olift (iter n f^-1) = 'oinv_(iter n f).

Proof.

elim: n => // n IH; rewrite iterfSr olift_comp IH ?oinv_iter -compA.
rewrite (_ : Some \o f^-1 = 'oinv_f); last by rewrite iterfSr; congr (_ \o _).
by apply/funeqP => ? /=; rewrite some_inv.
Qed.

..Build _ _ (iter n f) (some_iter_inv n).
Lemma : (iter n f)^-1 = iter n f^-1

Proof.

by []. Qed.

End OInv.

Lemma ( : {injfun A >-> A}) : OInv_Can aT aT A (iter n f).

Proof.

split=> x Ax; rewrite oinv_iter /=; elim: n=> // n IH.
by rewrite iterfSr /= funoK //; exact: mem_fun.
Qed.

. f g.
. ( A >-> A}) := Inject.on (iter n f).
. ( A >-> A}) := Inject.on (iter n f).
End iter_inv.

Section iter_surj.
Context {} { : set aT}.

Lemma ( : {surj A >-> A}) : OInv_CanV _ _ A A (iter n f).

Proof.

split; first exact: funS.
elim: n=> // n IH; rewrite oinv_iter iterfSr iterfS.
apply: (@ocan_in_comp _ _ _ (mem A)) => //; last exact: oinvK.
elim: n {IH} => // n IH x Ax; move: (IH _ Ax); rewrite pred_oapp_set ?inE.
case=> y Ay /= ynf; case: (@oinvS _ _ _ _ f _ Ay) => z ? zfinv; exists z => //.
by rewrite zfinv /= -ynf.
Qed.

. n f.
. ( A >-> A}) := Surject.on (iter n f).
. ( A >-> A}) := Surject.on (iter n f).
. ( A >-> A}) :=
Surject.on (iter n f).
. ( A >-> A}) := Surject.on (iter n f).
. ( A >-> A}) := Surject.on (iter n f).

End iter_surj.

Unbind

Section Unbind.
Context { } { : set aT} { : set rT} ( : aT -> rT).
Definition ( : aT -> option rT) := odflt (dflt x) (f x).

Lemma ( : {fun A >-> some @` B}) : isFun _ _ A B (unbind f).

Proof.

by rewrite /unbind; split=> x /'funS_f [y Bu <-]. Qed.

. f.

Section Oinv.
Context ( : {oinv aT >-> option rT}).
..Build _ _ (unbind f) ('oinv_f \o some).

Lemma : 'oinv_(unbind f) = 'oinv_f \o some

Proof.

by []. Qed.

End Oinv.
. ( A >-> some @` B}) := Fun.on (unbind f).

Section Inv.
Context ( : {inv aT >-> option rT}).
Lemma : olift (f^-1 \o some) = 'oinv_(unbind f).

Proof.

by rewrite olift_comp oliftV. Qed.

..Build _ _ (unbind f) inv_unbind_subproof.

Lemma : (unbind f)^-1 = f^-1 \o some

Proof.

by []. Qed.

End Inv.
. ( A >-> some @` B}) := Fun.on (unbind f).

Lemma ( : {injfun A >-> some @` B}) :
@OInv_Can _ _ A (unbind f).

Proof.

split=> x Ax; rewrite oinv_unbind /unbind/=; have <- := 'funoK_f Ax.
by have [y By /= <-] := 'funS_f (set_mem Ax).
Qed.

. f.
. ( A >-> some @` B}) :=
Inject.on (unbind f).

Lemma ( : {surj A >-> some @` B}) :
@OInv_CanV _ _ A B (unbind f).

Proof.

split=> [b|b /set_mem] Bb; rewrite oinv_unbind /unbind/=.
by case: oinvP => [|a]; [exists b | exists a].
by case: oinvP => [|a Aa /= ->]; first by exists b.
Qed.

. f.
. ( A >-> some @` B}) :=
  Surject.on (unbind f).
. ( A >-> some @` B}) :=
  Surject.on (unbind f).
. ( A >-> some @` B}) :=
  Surject.on (unbind f).
. ( A >-> some @` B}) := Surject.on (unbind f).
. ( A >-> some @` B}) := Bij.on (unbind f).

End Unbind.

Odflt

Section Odflt.
Context {} { : set T} ( : T).

Lemma : odflt x = unbind (fun=> x) idfun

Proof.

by []. Qed.

..Build _ _ (odflt x) some.

..copy (odflt x)
[the {splitbij some @` A >-> A} of @unbind (option T) T (fun=> x) idfun].

End Odflt.

Subtypes

Section SubType.
Context { : Type} { : pred T} ( : subType P) ( : sT).

..Build sT T val insub.

Lemma : 'oinv_val = insub

Proof.

by []. Qed.

Lemma : OInv_Can2 sT T setT [set` P] val.

Proof.

apply: (OInv_Can2.Build _ _ _ _ val (fun _ => valP x)
_ (in1W valK) (in1W (insubK _))).
by move=> x Px /=; exists (Sub x Px) => //; rewrite oinv_val insubT.
Qed.

..

..copy insub 'oinv_val.
..copy (insubd x0)
(odflt x0 \o 'split_(fun=> val x0) insub).

Lemma : (insubd x0)^-1 = val

Proof.

by []. Qed.

End SubType.

To setT

Definition {} ( : T) : [set: T] :=
  @SigSub _ _ _ x (mem_set I : x \in setT).
..Build T [set: T] setT to_setT
  ((fun _ _ => erefl) : {in setT, cancel to_setT val}).
..Build T _ setT setT to_setT (fun _ _ => I).
.
  SplitInjFun_CanV.Build T _ _ _ to_setT (fun => I) inj.
Definition {} := [splitbij of @to_setT T].

Lemma : (@to_setT T)^-1 = val

Proof.

by []. Qed.

Subfun

Section subfun.
Context {} { : set T}.

Definition ( : A `<=` B) ( : A) : B :=
SigSub (mem_set (AB _ (set_valP a))).

Lemma { : A `<=` B} : injective (subfun AB).

Proof.

by move=> x y /(congr1 val)/= /val_inj. Qed.

. ( `<=` B) :=
SurjFun.copy (subfun AB) [fun subfun AB in setT].
. ( `<=` B) :=
SurjFun_Inj.Build A B setT (subfun AB @` setT) (subfun AB) (in2W subfun_inj).

End subfun.

Section subfun_eq.
Context {} { : set T}.

Lemma ( : A `<=` B) ( : B `<=` A) : subfun AB @` setT = setT.

Proof.

by apply/seteqP; split=> x //= _; exists (subfun BA x) => //; exact/val_inj.
Qed.

Lemma ( : A = B) :
olift (subfun (subsetCW AB)) = 'oinv_(subfun (subsetW AB)).

Proof.

set g := subfun _; set f := subfun _; apply/funext => x /=.
apply: 'inj_(oapp f x) => //=.
- by rewrite inE/=; eexists.
- by rewrite inE/=; apply: 'oinvS_f; exists (g x) => //; apply/val_inj.
rewrite oinvK ?inE//=; last exact/val_inj.
by exists (g x) => //; apply/val_inj.
Qed.

. ( = B) :=
OInv_Inv.Build A B (subfun (subsetW AB)) (subfun_inv_subproof AB).

End subfun_eq.

Section seteqfun.
Context { : Type}.

Definition { : set T} ( : A = B) := subfun (subsetW AB).

Context { : set T} ( : A = B).
..Build A B (seteqfun AB) (seteqfun (esym AB)).

Lemma : Inv_Can2 A B setT setT (seteqfun AB).

Proof.

by split; rewrite /seteqfun//; move=> x _; apply/val_inj. Qed.

..

End seteqfun.

Inclusion

Section incl.
Context {} { : set T}.
Definition ( : A `<=` B) := @id T.

. ( `<=` B) := Inv.Build _ _ (incl AB) id.
. ( `<=` B) := isFun.Build _ _ A B (incl AB) AB.
. ( `<=` B) :=
Inv_Can.Build _ _ A (incl AB) (fun _ _ => erefl).

Definition ( : A = B) := incl (subsetW AB).
..on (eqincl AB).
Lemma : Inv_Can2 _ _ A B (eqincl AB).

Proof.

by split=> // x; rewrite /eqincl /incl/= /(_^-1)/inv/= AB. Qed.

. AB.

End incl.
Notation A := (incl (@subsetT _ _)).

Ad hoc function

Section mkfun.
Context {} {} { : set aT} { : set rT}.
Notation f := {homo f : / A x >-> B x}.
Definition ( : isfun f) := f.
..Build _ _ A B (@mkfun f fAB) fAB.
Definition := [fun of @mkfun f fAB].
. ( A >-> rT}) fAB := Inject.on (@mkfun f fAB).
. ( A >-> rT}) fAB :=
  SplitInj.on (@mkfun f fAB).
. ( A >-> B}) fAB :=
  Surject.on (@mkfun f fAB).
. ( A >-> B}) fAB :=
  SplitSurj.on (@mkfun f fAB).
End mkfun.

set_val

Section set_val.
Context {} { : set T}.
Definition : A -> T := eqincl (set_mem_set A) \o val.
..on set_val.
Lemma : 'oinv_set_val = insub

Proof.

by []. Qed.

Lemma : set_val = val

Proof.

by []. Qed.

End set_val.

#[global]
Hint Extern 0 (is_true (set_val _ \in _)) => solve [apply: valP] : core.

Squash

..Build T $|T| setT setT squash (fun _ _ => I)
(in1W unsquashK).
..copy (@unsquash T) squash^-1%FUN.
Definition {} := [splitsurj of @squash T].

pickle and unpickle

. () :=
Inj.Build _ _ setT (@choice.pickle T) (in2W (pcan_inj choice.pickleK)).
. () :=
isFun.Build _ _ setT setT (@choice.pickle T) (fun _ _ => I).

set0fun

Lemma { } : injective (@set0fun P T).

Proof.

by case=> x x0; have := set_mem x0. Qed.

.
Inj.Build (@set0 T) P setT set0fun (in2W set0fun_inj).
.
isFun.Build _ _ setT setT (@set0fun P T) (fun _ _ => I).

cast_ord

. = n} :=
  Can2.Build 'I_m 'I_n setT setT (cast_ord eq_mn)
    (fun _ _ => I) (fun _ _ => I)
    (in1W (cast_ordK _)) (in1W (cast_ordKV _)).

enum_val & enum_rank

. () :=
  Can2.Build T _ setT setT enum_rank (fun _ _ => I) (fun _ _ => I)
                                    (in1W enum_rankK) (in1W enum_valK).

. () :=
  Can2.Build _ T setT setT enum_val (fun _ _ => I) (fun _ _ => I)
                                    (in1W enum_valK) (in1W enum_rankK).

Finset val

Definition { : choiceType} { : {fset T}} ( : X) : [set` X] :=
  exist (fun => x \in [set` X]) (val x) (mem_set (valP x)).
Definition { : choiceType} { : {fset T}} ( : [set` X]) : X :=
  [` set_mem (valP x)]%fset.

Lemma { : choiceType} { : {fset T}} :
  cancel (@finset_val T X) val_finset.

Proof.

by move=> x; apply/val_inj. Qed.

Lemma { : choiceType} { : {fset T}} :
cancel (@val_finset T X) finset_val.

Proof.

by move=> x; apply/val_inj. Qed.

. {X : {fset T}} :=
  Can2.Build X _ setT setT finset_val (fun _ _ => I) (fun _ _ => I)
             (in1W finset_valK) (in1W val_finsetK).
. {X : {fset T}} :=
  Can2.Build _ X setT setT val_finset (fun _ _ => I) (fun _ _ => I)
             (in1W val_finsetK) (in1W finset_valK).

'I_n and `I_n

..Build _ _ setT setT (@ordII n)
(fun _ _ => I) (fun _ _ => I) (in1W ordIIK) (in1W IIordK).
..copy (@IIord n) (ordII^-1).

## Glueing

Definition { } { : set T} { : set T'}
& [disjoint X & Y] & [disjoint A & B] :=
fun ( : T -> T') ( : T) => if u \in X then f u else g u.

Section Glue12.
Context { } { : set T} { : set T'}.
Context { : [disjoint X & Y]} { : [disjoint A & B]}.
Local Notation := (glue XY AB).

Definition ( : T -> T') : {in X, gl f g =1 f}.

Proof.

by move=> x; rewrite /glue => ->. Qed.

Definition ( : T -> T') : {in Y, gl f g =1 g}.

Proof.

move=> x /set_mem Yx; rewrite /glue; case: ifPn => // /set_mem Xx.
by move: XY => /disj_setPS/(_ x (conj Xx Yx)).
Qed.

End Glue12.

Section Glue.
Context { } { : set T} { : set T'}.
Context { : [disjoint X & Y]} { : [disjoint A & B]}.
Local Notation := (glue XY AB).

Lemma ( : {fun X >-> A}) ( : {fun Y >-> B}) :
isFun T T' (X `|` Y) (A `|` B) (gl f g).

Proof.

by split=> x []xP; [left; rewrite glue1|right; rewrite glue2];
rewrite ?inE//; apply: funS.
Qed.

. f g.

. ( T >-> T'}) :=
  OInv.Build _ _ (gl f g) (glue AB (eqbRL disj_set_some XY) 'oinv_f 'oinv_g).

. ( X >-> A}) (g : {oinvfun Y >-> B}) :=
  OInversible.on (gl f g).

Lemma ( : {oinv T >-> T'}) ( : {oinv T >-> T'}) :
  'oinv_(gl f g) = glue AB (eqbRL disj_set_some XY) 'oinv_f 'oinv_g.

Proof.

by []. Qed.

Lemma ( : {inv T >-> T'}) :
some \o (glue AB XY f^-1 g^-1) = 'oinv_(gl f g).

Proof.

by apply/funext => y; rewrite oinv_glue /glue /= [LHS]fun_if !some_inv.
Qed.

. ( T >-> T'}) :=
  OInv_Inv.Build T T' (gl f g) (some_inv_glue_subproof f g).

. ( X >-> A}) (g : {invfun Y >-> B}) :=
  Inversible.on (gl f g).

Lemma ( : {invfun X >-> A}) ( : {invfun Y >-> B}) :
  (gl f g)^-1 = glue AB XY f^-1 g^-1.

Proof.

by []. Qed.

Lemma ( : {injfun X >-> A}) ( : {injfun Y >-> B}) :
OInv_Can _ _ (X `|` Y) (gl f g).

Proof.

split=> x; rewrite inE => -[] xP; rewrite oinv_glue.
by rewrite [glue _ _ _ _ x]glue1 ?inE// glue1 ?funoK ?inE//; apply: funS.
by rewrite [glue _ _ _ _ x]glue2 ?inE// glue2 ?funoK ?inE//; apply: funS.
Qed.

. f g.

. ( X >-> A})
(g : {splitinjfun Y >-> B}) := Inject.on (gl f g).

Lemma ( : {surj X >-> A}) ( : {surj Y >-> B}) :
OInv_CanV _ _ (X `|` Y) (A `|` B) (gl f g).

Proof.

split=> [z|y /set_mem [] yP]; rewrite oinv_glue.
- by move=> [] zP /=; [rewrite glue1|rewrite glue2]; rewrite ?inE//;
case: oinvP=> // x xX _; exists x => //; [left|right].
- by rewrite glue1 ?inE//; case: oinvP=> //= x xX _; rewrite glue1 ?inE.
- by rewrite glue2 ?inE//; case: oinvP=> //= x xX _; rewrite glue2 ?inE.
Qed.

. f g.
. ( X >-> A}) (g : {surjfun Y >-> B}) :=
  Surject.on (gl f g).
. ( X >-> A}) (g : {splitsurj Y >-> B}) :=
  Surject.on (gl f g).
. ( X >-> A}) (g : {splitsurjfun Y >-> B}) :=
  Surject.on (gl f g).
. ( X >-> A}) (g : {bij Y >-> B}) :=
  Surject.on (gl f g).
. ( X >-> A}) (g : {splitbij Y >-> B}) :=
  Surject.on (gl f g).

End Glue.

Z-module addition is a bijection

Section addition.
Context { : zmodType} ( : V).

..Build V V (+%R x) (+%R (- x)).

Lemma : (+%R x)^-1 = (+%R (- x))

Proof.

by []. Qed.

Lemma : Inv_Can2 V V setT setT (+%R x).

Proof.

by split => // y _; rewrite inv_addr ?GRing.addKr ?GRing.addNKr. Qed.

..

End addition.

Z-module opposite is a bijection

Section addition.
Context { : zmodType} ( : V).
Local Open Scope ring_scope.

..Build V V (-%R) (-%R).

Lemma : (-%R)^-1%FUN = (-%R)

Proof.

by []. Qed.

Lemma : Inv_Can2 V V setT setT (-%R).

Proof.

by split => // y _; rewrite inv_oppr ?GRing.opprK. Qed.

..

End addition.

emtpyType

Section empty.
Context { : emptyType} { : Type} { : set T}.
Implicit Type Y : set T'.

..Build _ _ (@any T T') (fun=> None).

Lemma : OInv_Can T T' X any.

Proof.

by split=> x; rewrite empty_eq0 inE. Qed.

..

Lemma : isFun T T' X Y any.

Proof.

by split=> x; rewrite empty_eq0. Qed.

. Y.

Lemma : OInv_CanV T T' X set0 any

Proof.

by split. Qed.

..

End empty.

## Theory of surjection

Section surj_lemmas.
Variables : Type.
Implicit Types (A : set aT) (B : set rT) (f : aT -> rT).

Lemma : set_surj A A (@idfun aT)

Proof.

exact: surj. Qed.

Lemma : set_surj set0 B f -> B = set0.

Proof.

by move=> Bf; rewrite predeqE => u; split => // /Bf [t []]. Qed.

Lemma : set_surj A B f = (B `<=` f @` A)

Proof.

by []. Qed.

Lemma : f @` A `<=` B -> set_surj A B f -> f @` A = B.

Proof.

by move=> fAB; rewrite eqEsubset => BfA. Qed.

Lemma : A `<=` A' -> set_surj A B f -> set_surj A' B f.

Proof.

by move=> /(@image_subset _ _ f)/(subset_trans _); apply. Qed.

Lemma : B' `<=` B -> set_surj A B f -> set_surj A B' f.

Proof.

exact: subset_trans. Qed.

Lemma ( : set aT) ( : set rT) :
{in B, cancel g f} -> g @` B `<=` A ->
set_surj A B f.

Proof.

move=> gK gBA y By; suff : A (g y) by exists (g y); rewrite ?gK ?inE.
by have := image_subP.1 gBA y; apply.
Qed.

Lemma ( : aT -> rT) ( : rT -> sT) :
set_surj A B f -> {in A, g \o f =1 g' \o f} -> {in B, g =1 g'}.

Proof.

move=> fS eqfg y /set_mem By; suff: B `<=` [set | g y = g' y] by exact.
by apply: subset_trans fS _ => _ [a /mem_set Aa <-] /=; rewrite [LHS]eqfg.
Qed.

Lemma ( : aT -> rT) : set_surj A B f <->
forall ( : rT -> sT), {in A, g \o f =1 g' \o f} -> {in B, g =1 g'}.

Proof.

split=> [*| f_epi y By]; first exact: (@surj_epi _ A B f).
have -> // := f_epi _ [set f x | in A] setT; last exact: mem_set.
by move=> x /set_mem xA; apply/propT; exists x.
Qed.

End surj_lemmas.
Arguments can_surj {aT rT} g [f A B].
Arguments surj_epi {aT rT sT} A {B} f {g}.

Lemma ( : set T1) ( : set T2) ( : set T3) :
set_surj A B f -> set_surj B C g -> set_surj A C (g \o f).

Proof.

by move=> fS gS; apply: 'surj_(gS \o fS). Qed.

Lemma { } { : set aT} { : set rT} ( : {surjfun A >-> B}) : f @` A = B.

Proof.

exact: surj_image_eq. Qed.

Lemma { : Type} { : set aT} { : set rT}
( : {surj A >-> B}) { : set rT} :
C `<=` B -> 'oinv_f @` C `<=` some @` (f @^-1` C).

Proof.

move=> CB x [/= y Cy <-]; case: 'oinvP_f => [|a Aa fay]; first exact: CB.
by exists a => //; rewrite fay.
Qed.

Arguments oinv_image_sub {aT rT A B} f {C} _.

Lemma { : Type} { : set aT} ( : {inj A >-> rT}) { : set rT} :
C `<=` f @` A -> some @` (A `&` f @^-1` C) `<=` 'oinv_f @` C.

Proof.

by move=> ? _ [a [? ?] <-]; exists (f a) => //; rewrite funoK ?inE. Qed.

Arguments oinv_Iimage_sub {aT rT A} f {C} _.

Lemma { } { : set aT} { : set rT} { : {bij A >-> B}}
{ : set rT} ( : C `<=` B) : 'oinv_f @` C = some @` (A `&` f @^-1` C).

Proof.

apply/seteqP; split; last by apply: oinv_Iimage_sub; rewrite image_eq.
rewrite some_setI subsetI; split; last by apply: oinv_image_sub.
by apply: (subset_trans (image_subset CB)); rewrite image_eq.
Qed.

Arguments oinv_sub_image {aT rT A B} f {C} _.

Lemma { } { : set rT} { : {bij [set: aT] >-> B}}
{ : set rT} ( : C `<=` B) : some @` (f @^-1` C) = 'oinv_f @` C.

Proof.

by rewrite oinv_sub_image// setTI. Qed.

Arguments preimageEoinv {aT rT B} f {C} _.

Lemma { : Type} { : set aT} { : set rT}
( : {splitsurj A >-> B}) { : set rT} :
C `<=` B -> f^-1 @` C `<=` f @^-1` C.

Proof.

by move=> CB x [/= y Cy <-]; rewrite invK// mem_set//; apply: CB. Qed.

Arguments inv_image_sub {aT rT A B} f {C} _.

Lemma { : Type} { : set aT} ( : {splitinj A >-> rT}) { : set rT} :
C `<=` f @` A -> A `&` f @^-1` C `<=` f^-1 @` C.

Proof.

by move=> CB x [Ax Cfx]; exists (f x) => //; rewrite funK// mem_set. Qed.

Arguments inv_Iimage_sub {aT rT A} f {C} _.

Lemma { } { : set aT} { : set rT} { : {splitbij A >-> B}}
{ : set rT} ( : C `<=` B) :
f^-1 @` C = A `&` f @^-1` C.

Proof.

by apply: image_some_inj; rewrite image_comp [Some \o _]oliftV oinv_sub_image.
Qed.

Arguments inv_sub_image {aT rT A B} f {C} _.

Lemma { } { : set rT} { : {splitbij [set: aT] >-> B}}
{ : set rT} ( : C `<=` B) : f @^-1` C = f^-1 @` C.

Proof.

by rewrite inv_sub_image// setTI. Qed.

Arguments preimageEinv {aT rT B} f {C} _.

Lemma { } ( : aT -> I) ( : set aT) ( : set I)
( : I -> set rT) : set_fun P Q f -> set_surj P Q f ->
\bigcup_( in Q) F x = \bigcup_( in P) F (f x).

Proof.

by move=> /image_subP fPQ /(surj_image_eq fPQ) QE; rewrite -[Q]QE bigcup_image.
Qed.

Arguments reindex_bigcup {aT rT I} f P Q.

Lemma { } ( : aT -> I) ( : set aT) ( : set I)
( : I -> set rT) : set_fun P Q f -> set_surj P Q f ->
\bigcap_( in Q) F x = \bigcap_( in P) F (f x).

Proof.

by move=> /image_subP fPQ /(surj_image_eq fPQ) QE; rewrite -[Q]QE bigcap_image.
Qed.

Arguments reindex_bigcap {aT rT I} f P Q.

Lemma ( : set I) ( : set J) ( : I -> J -> set T) :
  J ->
  \bigcap_( in D) \bigcup_( in E) F i j =
  \bigcup_( in set_fun D E) \bigcap_( in D) F i (f i).

Proof.

move=> j; apply/seteqP; split=> x.
  move=> /(_ _ _)/cid2 ff.
  have /(all_sig2_cond j) ( : I) : i \in D -> { : J | E x0 & F i x0 x}.
    by move=> /set_mem; apply: ff.
  by move=> [f /(_ _ (mem_set _))Ef /(_ _ (mem_set _))Ff]; exists f.
by move=> [f fDE fF i Fi]; exists (f i); [apply: fDE|apply: fF].
Qed.

Injections

Lemma ( : set I) ( : I -> set T) :
(forall , D i -> F i !=set0) -> trivIset D F -> set_inj D F.

Proof.

move=> FN0 Ftriv i j; rewrite !inE => Di Dj Fij.
by apply: Ftriv Di (Dj) _; rewrite Fij setIid; apply: FN0.
Qed.

Bijections

Section set_bij_lemmas.
Context { : Type} { : set aT} { : set rT} { : aT -> rT}.
Definition & set_bij A B f := f.
Context ( : set_bij A B f).
Local Notation := (fun_set_bij fbij).

Lemma : {in A &, injective f}

Proof.

by case: fbij. Qed.

Lemma : {homo f : / A x >-> B x}

Proof.

by case: fbij. Qed.

Lemma : f @` A `<=` B

Proof.

exact/image_subP/set_bij_homo. Qed.

Lemma : set_surj A B f

Proof.

by case: fbij. Qed.

. _ _ _ _ g := set_bij_surj.
..Build _ _ A B g set_bij_homo.
..Build _ _ A B g set_bij_inj.

End set_bij_lemmas.
Coercion fun_set_bij : set_bij >-> Funclass.

Coercion ( : set aT) ( : set rT) ( : aT -> rT)
( : set_bij A B f) := Bij.on (fun_set_bij fS).

Section Pbij.
Context { } { : set aT} { : set rT} { : aT -> rT} ( : set_bij A B f).
. _ _ A B f := fbij.
Definition := [bij of f].
Lemma : { : {bij A >-> B} | f = s}

Proof.

by exists [bij of f]. Qed.

End Pbij.
Coercion bij_of_set_bijection : set_bij >-> Bij.type.

Lemma { } { : set aT} { : set rT} { : {bij A >-> B}} : set_bij A B f.

Proof.

split=> //. Qed.

Definition ( : set aT) ( : set rT) ( : {bij A >-> B}) &
phantom (_ -> _) f := @bij _ _ _ _ f.
Notation := (phant_bij (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Extern 0 (set_bij _ _ _) => solve [apply: bij] : core.

Section PbijTT.
Context { } { : aT -> rT} ( : bijective f).
..Build _ _ f fbijTT.
Definition := [splitbij of f].
Lemma : { : {splitbij [set: aT] >-> [set: rT]} | f = s}.

Proof.

by exists [splitbij of f]. Qed.

End PbijTT.

Lemma ( : aT -> rT) :
set_bij [set: aT] [set: rT] f = bijective f.

Proof.

apply/propext; split=> [[]|/PbijTT[{}f ->]].
move=> _ fI /(_ _ I)-/(_ _)/cid2-/all_sig2[g _ gK].
by exists g => // x; apply: fI; rewrite ?inE.
by split=> // [x y _ _ /'inj_f//|y _]; exists (f^-1 y) => //; rewrite funK.
Qed.

Lemma { } { : {bij [set: aT] >-> [set: rT]}} : bijective f.

Proof.

by rewrite -setTT_bijective. Qed.

Definition ( : {bij [set: aT] >-> [set: rT]})
& phantom (_ -> _) f := @bijTT _ _ f.
Notation := (phant_bijTT (Phantom (_ -> _) f)) : form_scope.
#[global] Hint Extern 0 (bijective _) => solve [apply: bijTT] : core.

## Patching and restrictions

Section patch.
Context { : Type} ( : aT -> rT) ( : set aT).
Definition ( : aT -> rT) := if u \in A then f u else d u.

Lemma : {in A, patch f =1 f}

Proof.

by rewrite /patch => x ->. Qed.

Lemma : {in [predC A], patch f =1 d}.

Proof.

by rewrite /patch => x /negPf/= ->. Qed.

Lemma : {in ~` A, patch f =1 d}.

Proof.

by move=> u /set_mem/= NAu; rewrite patchN ?inE//= notin_setE. Qed.

.
SurjFun.copy (patch f) [fun patch f in A].

Section inj.
Context ( : {inj A >-> rT}).
Let := patch f.
Lemma : Inj aT rT A g.

Proof.

by split=> x y xA yA; rewrite /g !patchT//; apply: inj. Qed.

..
..copy (patch f) [fun g in A].
End inj.

End patch.
Notation := (patch (fun=> point)).
Notation := (restrict D f) : function_scope.

Lemma ( : pointedType) ( : aT -> rT) ( : set aT) :
(f \_ B) x = if x \in B then f x else point.

Proof.

by []. Qed.

Lemma { } ( : {pred I}) ( : I -> T) :
patch d D f = fun => if D i then f i else d i.

Proof.

by apply/funext => i; rewrite /patch mem_setE. Qed.

Lemma ( : Type) ( : pointedType)
( : aT -> rT) ( : set aT) ( : set rT) :
(f \_ D) @^-1` B = (if point \in B then ~` D else set0) `|` D `&` f @^-1` B.

Proof.

rewrite /preimage/= /patch; apply/predeqP => x /=; split.
case: ifPn; rewrite ?(inE, notin_setE); first by right.
by move=> NDx Bp; rewrite ifT ?inE//=; left.
move=> [|[Dx Bfx]]; last by rewrite ifT ?inE.
by case: ifP; rewrite // inE => Bp NDx; case: ifPn; rewrite // inE.
Qed.

Lemma { : Type} ( : aT -> rT) ( : aT -> rT) ( : rT -> sT) :
h \o patch g D f = patch (h \o g) D (h \o f).

Proof.

by apply/funext => x; rewrite /patch/=; case: ifP. Qed.

Lemma { : Type} ( : aT -> rT) ( : aT -> rT) :
patch g (D `&` D') f = patch g D (patch g D' f).

Proof.

apply/funext => x; rewrite /patch/= in_setI.
by case: (x \in D) (x \in D') => [] [].
Qed.

Lemma { : Type} ( : aT -> rT) ( : aT -> rT) :
patch g set0 f = g.

Proof.

by apply/funext => x; rewrite /patch in_set0. Qed.

Lemma { : Type} ( : aT -> rT) ( : aT -> rT) :
patch g setT f = f.

Proof.

by apply/funext => x; rewrite /patch in_setT. Qed.

Lemma {} { : pointedType} ( : rT -> sT) ( : aT -> rT) :
h point = point -> (h \o f) \_ D = h \o (f \_ D).

Proof.

by move=> hp; apply/funext => x; rewrite /patch/=; case: ifP. Qed.

Arguments restrict_comp {aT rT sT} h f D.

Lemma ( : Type) ( : set I) ( : I -> set T) :
trivIset D' (F \_ D) = trivIset (D `&` D') F.

Proof.

apply/propext; split=> FDtriv i j.
move=> [Di D'i] [Dj D'j] [x [Fix Fjx]]; apply: FDtriv => //.
by exists x; split => /=; rewrite ?patchT ?in_setE.
move=> D'i D'j [x []]; rewrite /patch.
do 2![case: ifPn => //]; rewrite !in_setE => Di Dj Fix Fjx.
by apply: FDtriv => //; exists x.
Qed.

## Restriction of domain and codomain

Section RestrictionLeft.
Context { : Type} ( : V) { : set U} { : set V}.

Local Notation := (patch (fun=> v) A).

Definition ( : U -> V) : A -> V := f \o set_val.

Lemma ( : {fun A >-> B}) : isFun _ _ [set: A] B (sigL f).

Proof.

by split=> x _; apply: funS. Qed.

. ( A >-> B}) := sigL_isfun f.

Definition ( : {fun A >-> B}) := [fun of sigL f].
Definition ( : A -> V) : U -> V := ((@oapp _ _)^~ v) f \o 'oinv_set_val.

Lemma ( : {fun [set: A] >-> B}) :
isFun _ _ A B (valL_ (f : _ -> _)).

Proof.

by split=> x Ax; apply: funS. Qed.

. ( [set: A] >-> B}) := valL_isfun f.
Definition ( : {fun [set: A] >-> B}) := [fun of valL_ f].

Lemma ( : U -> V) ( : x \in A) :
sigL f (SigSub xA) = f x.

Proof.

done. Qed.

Lemma ( : U -> V):
{in A, f =1 g} <-> sigL f = sigL g.

Proof.

split=> [eq_f_g | Rfg u uA]; first by apply/funext => -[x]; apply: eq_f_g.
by have := congr1 (@^~ (exist _ u uA)) Rfg.
Qed.

Lemma ( : {fun A >-> B}) :
{in A, f =1 g} <-> sigLfun f = sigLfun g.

Proof.

by rewrite eq_sigLP funP funeqP. Qed.

Lemma : valL_ \o sigL = restrict.

Proof.

rewrite funeq2E => f u; rewrite /valL_ /sigL /restrict.
by rewrite oinv_set_val/=; case: ifPn => uA; [rewrite insubT|rewrite insubN].
Qed.

Lemma : cancel valL_ sigL.

Proof.

move=> f; rewrite /valL_ /sigL /restrict oinv_set_val.
apply/funext=> a /=; have aA : set_val a \in A by apply: valP.
by rewrite insubT//=; congr f; apply/val_inj.
Qed.

Lemma : cancel valLfun_ sigLfun.

Proof.

by move=> f; apply/funP/funeqP; exact: valLK. Qed.

Lemma : sigL \o valL_ = id.

Proof.

exact/funext/valLK. Qed.

Lemma : sigLfun \o valLfun_ = id.

Proof.

exact/funext/valLfunK. Qed.

Lemma : sigL \o restrict = sigL.

Proof.

rewrite funeq2E => f -[u Au] /=.
by rewrite /sigL /restrict /valL_ /patch /= Au.
Qed.

Lemma : range sigL = setT.

Proof.

rewrite eqEsubset; split=> //= f _; exists (valL_ f)=>//.
exact: valLK.
Qed.

Lemma ( : U -> V): {in A, f =1 g} <-> restrict f = restrict g.

Proof.

by rewrite eq_sigLP -sigLK/=; split => [->//|/(can_inj valLK)]. Qed.

End RestrictionLeft.
Arguments sigL {U V} A f u /.
Arguments sigLE {U V} A f x.
Arguments valL_ {U V} v {A} f u /.
Notation := (valL_ v) : form_scope.
Notation := (valLfun_ v) : form_scope.
Notation := (valL_ point).

Section RestrictionRight.
Context { : Type} { : set V}.

Definition ( : {fun [set: U] >-> A}) ( : U) : A :=
SigSub (mem_set ('funS_f I) : f u \in A).
..copy (sigR f) (totalfun _).

Definition ( : U -> A) := set_val \o totalfun f.
..on (valR f).

Definition ( : U -> A) : {fun [set: U] >-> A} := [fun of valR f].

Lemma ( : {fun [set: U] >-> A}) : valR (sigR f) = f.

Proof.

by []. Qed.

Lemma ( : {fun [set: U] >-> A}) : valR_fun (sigR f) = f.

Proof.

by apply/funP/funeqP; apply: sigRK. Qed.

Lemma ( : U -> A) : A (valR f x)

Proof.

exact: set_valP. Qed.

Lemma : cancel valR_fun sigR.

Proof.

by move=> f; apply/funext => x; apply/val_inj. Qed.

End RestrictionRight.
Arguments sigR {U V A} f u /.

Section RestrictionLeftInv.
Context { : Type} ( : V) { : set U} { : set V}.
Local Notation := (sigL A).
Local Notation := sigR.
Local Notation := 'valL_v.
Local Notation := valR.

. ( U >-> V}) :=
@OInv.Build _ _ (rl f) (obind insub \o 'oinv_f).
. ( A >-> B}) := Fun.on (rl f).

Lemma ( : {oinv U >-> V}) : 'oinv_(rl f) = obind insub \o 'oinv_f.

Proof.

by []. Qed.

Lemma ( : {inj A >-> V}) : @OInv_Can _ _ setT (rl f).

Proof.

by split=> x _; rewrite oinv_sigL/= funoK//= [insub _]'funoK_val ?inE.
Qed.

. f.
. ( A >-> B}) := Fun.on (rl f).

Lemma ( : {surj A >-> B}) : @OInv_CanV _ _ setT B (rl f).

Proof.

split=> [b|b /set_mem] Bb; rewrite ?oinv_sigL/=.
   have [x /mem_set Ax <-]/= := 'oinvS_f Bb; exists (SigSub Ax) => //=.
   case: insubP => [a Aa/= eqx|]; last by rewrite Ax.
   by congr Some; apply/val_inj.
by rewrite /rl/= oapp_comp/= -oinv_val -inv_omap/= invK ?oinvK ?mem_fun ?inE.
Qed.

. f.
. ( A >-> B}) := Fun.on (rl f).
. ( A >-> B}) := Fun.on (rl f).

. ( [set: V] >-> A}) :=
@OInv.Build _ _ (rr f) (rl 'oinv_f).

Lemma ( : {oinvfun [set: V] >-> A}) :
'oinv_(rr f) = (rl 'oinv_f).

Proof.

by []. Qed.

Lemma ( : {injfun [set: V] >-> A}) :
@OInv_Can _ _ setT (rr f).

Proof.

by split=> x _; rewrite oinv_sigR/= set_valE/= funoK ?inE. Qed.

. f.

Lemma ( : {surjfun [set: V] >-> A}) :
@OInv_CanV _ _ setT setT (rr f).

Proof.

split=> a _; rewrite ?oinv_sigL/=.
by have [x _ xeq] := 'oinvS_f (set_valP a); exists x.
apply/val_inj=> /=; rewrite oinv_sigR/=.
by case: oinvP=> //=; apply: set_valP.
Qed.

. f.

Lemma ( : {invfun [set: V] >-> A}) :
olift (rl f^-1) = 'oinv_(rr f).

Proof.

by rewrite oinv_sigR olift_comp oliftV. Qed.

. ( [set: V] >-> A}) := Fun.on (rr f).

. ( [set: V] >-> A}) :=
@OInv_Inv.Build _ _ (rr f) (rl f^-1) (sigR_some_inv f).

Lemma ( : {invfun [set: V] >-> A}) : (rr f)^-1 = (rl f^-1).

Proof.

by []. Qed.

. ( [set: V] >-> A}) := Inject.on (rr f).
. ( [set: V] >-> A}) := Surject.on (rr f).
. ( [set: V] >-> A}) := Fun.on (rr f).

Lemma ( : {splitbij A >-> [set: V]}) :
olift (rr [fun of f^-1]) = 'oinv_(rl f).

Proof.

apply/funext=> x /=; rewrite oinv_sigL /= /sigR/= /olift/=.
case: oinvP => //= u Au _; rewrite insubT ?inE// => memAu.
by congr (Some _); apply/val_inj=> /=; rewrite funK.
Qed.

. ( A >-> [set: V]}) :=
OInv_Inv.Build _ _ (rl f) (sigL_some_inv f).

Lemma ( : {splitbij A >-> [set: V]}) :
(rl f)^-1 = (rr [fun of f^-1]).

Proof.

by []. Qed.

. ( A >-> V}) :=
@OInv.Build _ _ (el f) (omap set_val \o 'oinv_f).
. ( [set: A] >-> B}) := Fun.on (el f).

Lemma ( : {oinv A >-> V}) :
'oinv_(el f) = omap set_val \o 'oinv_f.

Proof.

by []. Qed.

Lemma { } ( : aT -> rT) ( : rT -> sT) ( : rT) :
oapp (g \o f) (g x) y = g (oapp f x y).

Proof.

by case: y. Qed.

Lemma ( : {inj [set: A] >-> V}) : @OInv_Can _ _ A (el f).

Proof.

split=> x /set_mem xA; rewrite oinv_valL/= -oapp_comp_x.
by case: oinvP=> //= a _ _; rewrite funoK ?inE.
Qed.

. f.
. ( [set: A] >-> B}) := Inject.on (el f).

Lemma ( : {surj [set: A] >-> B}) : @OInv_CanV _ _ A B (el f).

Proof.

split=> [b|b /set_mem] Bb; rewrite ?oinv_valL/=.
by case: oinvP => // => a; exists (set_val a) => //; apply: set_valP.
by case: oinvP => //= a _ _; rewrite funoK// inE.
Qed.

. f.
. ( [set: A] >-> B}) := Surject.on (el f).
. ( [set: A] >-> B}) := Surject.on (el f).

Lemma ( : {inv A >-> V}) : olift (er f^-1) = 'oinv_(el f).

Proof.

by rewrite oinv_valL/= olift_comp -oliftV. Qed.

. ( A >-> V}) :=
OInv_Inv.Build _ _ (el f) (valL_some_inv f).
. ( [set: A] >-> B}) := Fun.on (el f).

Lemma ( : {inv A >-> V}) : (el f)^-1 = er f^-1.

Proof.

by []. Qed.

. ( [set: A] >-> V}) := Inject.on (el f).
. ( [set: A] >-> B}) := Fun.on (el f).
. ( [set: A] >-> B}) := Surject.on (el f).
. ( [set: A] >-> B}) := Fun.on (el f).
. ( [set: A] >-> B}) := Fun.on (el f).

Lemma ( : U -> V) :
injective (rl f) <-> {in A &, injective f}.

Proof.

split=> [f_inj x y Ax Ay|/Pinj[{}f-> //]]; last first.
by move=> eqfxy; suff [->] : SigSub Ax = SigSub Ay by []; apply: f_inj.
Qed.

Lemma ( : U -> V) :
set_surj [set: A] B (rl f) <-> set_surj A B f.

Proof.

split=> [fsurj b Bb/=|/Psurj[{}f->]//].
by have [a _ <-] := fsurj _ Bb; exists (set_val a) => //; apply: set_valP.
Qed.

Lemma ( : U -> V) :
set_fun [set: A] B (rl f) <-> set_fun A B f.

Proof.

split=> [ffun u Au/=|/Pfun[{}f->]//].
exact: (ffun (SigSub (mem_set Au))).
Qed.

Lemma ( : U -> V) :
set_bij [set: A] B (rl f) <-> set_bij A B f.

Proof.

split=> [[F /in2TT I S]|/Pbij[{}f->]//].
by split; [exact/sigL_funP|exact/sigL_injP|exact/sigL_surjP].
Qed.

Lemma ( : A -> V) : {in A &, injective (el f)} <-> injective f.

Proof.

by rewrite -sigL_injP valLK. Qed.

Lemma ( : A -> V) :
set_surj A B (el f) <-> set_surj setT B f.

Proof.

by rewrite -sigL_surjP valLK. Qed.

Lemma ( : A -> V) :
set_fun A B (el f) <-> set_fun setT B f.

Proof.

by rewrite -sigL_funP valLK. Qed.

Lemma ( : A -> V) :
set_bij A B (el f) <-> set_bij setT B f.

Proof.

by rewrite -sigL_bijP valLK. Qed.

End RestrictionLeftInv.

Section ExtentionLeftInv.
Context { : Type} { : set U} { : set V}.
Local Notation := 'valL_None.
Local Notation := valR.

. ( V >-> A}) :=
@OInv.Build _ _ (er f) (el 'oinv_f).

Lemma ( : {oinv V >-> A}) : 'oinv_(er f) = (el 'oinv_f).

Proof.

by []. Qed.

Lemma ( : {inj [set: V] >-> A}) :
@OInv_Can _ _ setT (er f).

Proof.

by split=> x _; rewrite /er oinv_valR/= funoK/= ?funoK ?inE. Qed.

. f.

Lemma ( : {surj [set: V] >-> [set: A]}) :
@OInv_CanV _ _ setT A (er f).

Proof.

split=> [a|a /set_mem] Aa; rewrite ?oinv_valR/= oinv_set_val.
by rewrite insubT ?inE// => memaA /=; case: oinvP => //= x; exists x.
rewrite insubT ?inE// => memaA/=; case: oinvP => //= x _.
by rewrite /er/= /totalfun => ->.
Qed.

. f.
. ( [set: V] >-> [set: A]}) := Fun.on (er f).

End ExtentionLeftInv.

Section Restrictions2.
Context { : Type} ( : V) { : set U} { : set V}.

Local Notation := 'valL_v.
Local Notation := 'valLfun_v.

Definition := sigR \o (@sigLfun U V A B).

. ( A >-> B}) :=
Fun.copy (sigLR f) (totalfun _).

Definition : (A -> B) -> U -> V := valL \o valR_fun.
Definition : (A -> B) -> {fun A >-> B} := valLfun \o valR_fun.

Lemma ( : A -> B) : valLR f = valL (valR f)

Proof.

by []. Qed.

Lemma ( : A -> B) : valLRfun f = [fun of valLR f]

Proof.

by []. Qed.

Lemma ( : {fun A >-> B}) : {in A, valLR (sigLR f) =1 f}.

Proof.

by apply/eq_sigLP; rewrite valLK sigR_funK. Qed.

Lemma : cancel valLRfun sigLR.

Proof.

by move=> f; rewrite /sigLR /valLR /= valLfunK valRK. Qed.

Lemma : injective valLRfun.

Proof.

by move=> f g eqefg; rewrite -[LHS]valLRK eqefg valLRK. Qed.

. ( A >-> B}) := OInversible.on (sigLR f).
. ( A >-> B}) := Inject.on (sigLR f).
. ( A >-> B}) := Surject.on (sigLR f).
. ( A >-> B}) := Fun.on (sigLR f).

. ( A >-> B}) := OInvFun.on (valLR f).
. ( [set: A] >-> B}) := Inject.on (valLR f).
. ( [set: A] >-> [set: B]}) := Surject.on (valLR f).
. ( [set: A] >-> [set: B]}) := Fun.on (valLR f).

Lemma ( : {fun A >-> B}) :
injective (sigLR f) <-> {in A &, injective f}.

Proof.

split=> [f_inj x y Ax Ay|/funPinj[{}f-> //]]; last first.
move=> eqfxy; suff [->] : SigSub Ax = SigSub Ay by [].
by apply: f_inj; apply/val_inj.
Qed.

Lemma ( : A -> B) :
{in A &, injective (valLR f)} <-> injective f.

Proof.

by rewrite -sigLR_injP valLRK. Qed.

Lemma ( : {fun A >-> B}) :
set_surj setT setT (sigLR f) <-> set_surj A B f.

Proof.

split=> [fsurj b Bb/=|/funPsurj[{}f->]//].
have [x _ /(congr1 val)/= <-] := fsurj (SigSub (mem_set Bb)) I.
by exists (set_val x) => //; apply: set_valP.
Qed.

Lemma ( : A -> B) :
set_surj A B (valLR f) <-> set_surj setT setT f.

Proof.

by rewrite -sigLR_surjP valLRK. Qed.

Lemma ( : U -> V) :
  set_bij A B f <->
  exists ( : {homo f : / A x >-> B x}),
    bijective (sigLR [fun of mkfun fAB]).

Proof.

split=> [[F I S]|[fAB]].
exists F; rewrite -setTT_bijective.
by split; [|apply: in2W; apply/sigLR_injP|apply/sigLR_surjP].
rewrite -setTT_bijective /set_bij.
set g := [fun of mkfun fAB] => -[_ /in2TT I S]; pose h : _ -> _ := g.
rewrite -[f]/h {}/h; move: g => g in I S *.
by split; [apply/image_subP|apply/sigLR_injP|apply/sigLR_surjP].
Qed.

Lemma : bijective (sigLR f) <-> set_bij A B f.

Proof.

rewrite sigLR_bijP; split=> [fbij|[fAB]]; [exists funS|];
by rewrite (_ : [fun of _] = f)//; apply/funP.
Qed.

Lemma : set_bij A B (valLR f) <-> bijective f.

Proof.

by rewrite -sigLRfun_bijP valLRK. Qed.

End Restrictions2.

Section set_bij_basic_lemmas.
Context { : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT -> rT).

Lemma : {in A, f =1 g} -> set_bij A B f -> set_bij A B g.

Proof.

by move=> /eq_sigLP + /sigL_bijP => -> /sigL_bijP. Qed.

Lemma : {in A, f =1 g} -> set_bij A B g -> set_bij A B f.

Proof.

by move=> /eq_sigLP + /sigL_bijP => <- /sigL_bijP. Qed.

Lemma : {in A, f =1 g} -> set_bij A B f = set_bij A B g.

Proof.

by move=> eqfg; apply/propeqP; split; [apply: eq_set_bijRL | apply: eq_set_bijLR].
Qed.

Lemma :
set_bij (some @` A) (some @` B) (omap f) <-> set_bij A B f.

Proof.

split=> [/Pbij[b mapfb]|/Pbij[{}f->//]].
suff -> : f = unbind f (b \o some) :> (_ -> _) by [].
by apply/funext=> x; rewrite -mapfb.
Qed.

Lemma : set_bij A (some @` B) (olift f) <-> set_bij A B f.

Proof.

split=> [/Pbij[b liftfb]|/Pbij[{}f->//]].
suff -> : f = unbind f b :> (_ -> _) by [].
by apply/funext=> x; rewrite -liftfb.
Qed.

End set_bij_basic_lemmas.

Lemma { } { : set aT} { : set rT}
( : {bij A >-> B}) : C `<=` A -> D `<=` B ->
set_bij D (some @` C) 'oinv_f <-> set_bij C D f.

Proof.

move=> CA DB; gen have oinv_bij : aT rT A C B D CA DB f /
    set_bij C D f -> set_bij D (some @` C) 'oinv_f; last first.
  split=> bij_oinv; last exact: oinv_bij.
  by apply/bij_omap; rewrite -oinvV; apply: oinv_bij => //; apply: image_subset.
move=> /Pbij[fC ffC]; suff /eq_set_bij-> : {in D, 'oinv_f =1 'oinv_fC} by [].
move=> x xD; apply: 'inj_(oapp f x); rewrite ?mem_fun//=.
- by apply/subsetP : x xD.
- by have := mem_set ((image_subset CA) _ ('oinvS_fC (set_mem xD))).
by rewrite oinvK ?ffC ?oinvK// ?(subsetP.2 _ _ xD).
Qed.

Lemma { } { : set aT} { : set rT}
( : {splitbij A >-> B}) : C `<=` A -> D `<=` B ->
set_bij D C f^-1 <-> set_bij C D f.

Proof.

by move=> CA DB; rewrite -bij_sub_sym// -oliftV bij_olift. Qed.

Section set_bij_lemmas.
Context { : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT -> rT).

Lemma ( : T -> U) : set_bij set0 set0 f.

Proof.

by split=> [_ []//|x y|//]; rewrite inE. Qed.

Hint Resolve set_bij00 : core.

Lemma : {in A &, injective f} -> set_bij A (f @` A) f.

Proof.

by move=> /Pinj[{}f->]; apply: 'bij_[fun f in A]. Qed.

Lemma ( : {bij A >-> B}) : C `<=` A -> f @` C = D ->
set_bij C D f.

Proof.

by move=> /homo_setP CA <-; split=> // x y /CA + /CA +; apply: inj. Qed.

End set_bij_lemmas.

Section set_bij_lemmas.
Context { : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT -> rT).

Lemma ( : {bij A >-> B}) : C = A `&` (f @^-1` D) -> D `<=` B ->
set_bij C D f.

Proof.

move=> -> DB; apply/bij_sub_sym=> //; apply: bij_subl => //=.
by rewrite oinv_sub_image.
Qed.

Lemma ( : {bij A >-> B}) : C `<=` A -> D `<=` B ->
    {homo f : / C x >-> D x} ->
    {homo 'oinv_f : / D x >-> (some @` C) x} ->
  set_bij C D f.

Proof.

move=> CA DB fCD fDC; apply: bij_subl => //; apply/seteqP; split.
by apply/image_subP.
move=> y /[dup]/[dup] Dy /DB By /fDC [x Cx]/= xfy; exists x => //; move: xfy.
by case: oinvP => // a Aa _ [->].
Qed.

Lemma ( : {splitbij A >-> B}) : C `<=` A -> D `<=` B ->
    {homo f : / C x >-> D x} ->
    {homo f^-1 : / D x >-> C x} ->
  set_bij C D f.

Proof.

move=> CA DB /(bij_sub CA DB) /[swap] fDC; apply=> x Dx.
by rewrite -some_inv/=; exists (f^-1 x) => //; apply: fDC.
Qed.

Lemma ( : {fun A >-> B}) ( : {fun B >-> A}) :
{in A, cancel f g} -> {in B, cancel g f} -> set_bij A B f.

Proof.

by move=> /can_in_inj finj /can_surj gK; split => //; apply: gK. Qed.

Lemma : [disjoint B & B'] ->
set_bij A (B `|` B') f -> set_bij (A `\` f @^-1` B') B f.

Proof.

move=> /disj_setPS BB' /Pbij[{}f->]; apply: bij_subr; last exact: subsetUl.
apply/seteqP; split=> x /= [Ax Bfx]; split=> //; first by have [] := 'funS_f Ax.
by move=> B'fx; apply: (BB' (f x)).
Qed.

Lemma : [disjoint B & B'] ->
set_bij A (B `|` B') f -> set_bij (A `\` f @^-1` B) B' f.

Proof.

by rewrite setUC disj_set_sym; apply: bij_sub_setUrl. Qed.

Lemma : [disjoint A & A'] ->
set_bij (A `|` A') B f -> set_bij A (B `\` f @` A') f.

Proof.

move=> /disj_setPS AA' /Pbij[{}f->].
apply: bij_sub => [|? []//||]; first exact: subsetUl.
  move=> x Ax /=; split; first by apply: funS; left.
  move=> [y] A'y /inj; rewrite !inE/= =>yx; apply: (AA' x).
  by split=> //; rewrite -yx //; [right|left].
move=> z [Bz /= /not_exists2P /contrapT] A'fxz.
case: oinvP=> // x AA'x fxz; exists x => //.
by have := A'fxz x; rewrite fxz => -[|//]; case: AA'x.
Qed.

Lemma : [disjoint A & A'] ->
set_bij (A `|` A') B f -> set_bij A' (B `\` f @` A) f.

Proof.

by rewrite setUC disj_set_sym; apply: bij_sub_setUll. Qed.

End set_bij_lemmas.

Lemma ( : set T) ( : nat -> T) :
set_bij `I_n.+1 A f -> set_bij `I_n (A `\ f n) f.

Proof.

rewrite IIS -[[set f n]]image_set1; apply: bij_sub_setUll.
by apply/disj_setPS => i [/= /[swap]->]; rewrite ltnn.
Qed.

Lemma ( : set T1) ( : set T2) ( : set T3) :
set_bij A B f -> set_bij B C g -> set_bij A C (g \o f).

Proof.

by move=> /Pbij[{}f->] /Pbij[{}g->]; apply: 'bij_(g \o f). Qed.

Section pointed_inverse.
Context { } ( : U -> T) ( : set T).
Implicit Types (f : T -> U) (i : {inj A >-> U}).

Definition := ('split_dflt [fun f in A])^-1.
Local Notation := pinv_.
..Build _ _ (pinv f) f.
..on (pinv f).
..on (pinv f).
..on (pinv i).

Lemma : {in f @` A, cancel (pinv f) f}.

Proof.

exact: 'funK_(pinv f). Qed.

Lemma : {in A &, injective f} -> {in A, cancel f (pinv f)}.

Proof.

by move=> /Pinj[{}f->]; apply: funK. Qed.

Lemma : {in A &, injective f} ->
set_surj (f @` A) A (pinv f).

Proof.

by move=> /Pinj[{}f->]; apply: surj. Qed.

Lemma : {in A &, injective f} ->
pinv f @` (f @` A) = A.

Proof.

by move=> /Pinj[{}f->]; rewrite image_eq. Qed.

Lemma : {in A &, injective f} ->
set_bij (f @` A) A (pinv f).

Proof.

by move=> /Pinj[{}f->]; apply: bij. Qed.

Lemma : set_surj A B f -> {in B, cancel (pinv f) f}.

Proof.

by move=> /homo_setP BfA; move=> x /BfA xfA; rewrite pinvK. Qed.

Lemma : set_surj A B f -> pinv f @` B `<=` A.

Proof.

by move=> fsurj; apply: (subset_trans (image_subset fsurj)). Qed.

Lemma : set_surj A B f -> {in B &, injective (pinv f)}.

Proof.

by move=> /homo_setP/sub_in2; apply. Qed.

Lemma ( := pinv f) : set_surj A B f ->
set_bij B (g @` B) g.

Proof.

by move=> f_surj; split=> //; apply: surjpinv_inj. Qed.

Lemma : set_bij A B f -> set_bij B A (pinv f).

Proof.

by move=> /Pbij[{}f->]; have /= := 'bij_(pinv f); rewrite image_eq. Qed.

Section pPbij.
Context {: set U} { : T -> U} ( : set_bij A B f).
Lemma : { : {splitbij A >-> B} | f = s}.

Proof.

pose h := [splitbij of 'split_dflt [fun fbij in A]]; have : f = h by [].
by move: h; rewrite /= (image_eq fbij) => h; exists h.
Qed.

End pPbij.

Section pPinj.
Context { : T -> U} ( : {in A &, injective f}).
Lemma : { : {splitinj A >-> U} | f = i}.

Proof.

by move: finj => /Pinj[g ->]; exists [splitinj of 'split_dflt [fun g in A]].
Qed.

End pPinj.

Section injpPfun.
Context { : set U} { : {inj A >-> U}} ( : {homo f : / A x >-> B x}).
Let : _ -> _ := f.
..copy g ('split_dflt [fun g in A]).
..Build _ _ _ _ g ffun.
Lemma : { : {splitinjfun A >-> B} | f = i :> (_ -> _)}.

Proof.

by exists [splitinjfun of g]. Qed.

End injpPfun.

Section funpPinj.
Context { : set U} { : {fun A >-> B}} ( : {in A &, injective f}).
Lemma : { : {splitinjfun A >-> B} | f = i :> (_ -> _)}.

Proof.

by move: finj 'funS_f => /pPinj_[g ->]/injpPfun_. Qed.

End funpPinj.

End pointed_inverse.
Notation := (pinv_ dflt) : form_scope.
Notation := 'pinv_(fun=> point).
Notation := (pPbij_ dflt) : form_scope.
Notation := 'pPbij_(fun=> point).
Notation := 'pPbij_id.
Notation := (pPinj_ dflt) : form_scope.
Notation := 'pPinj_(fun=> point).
Notation := (injpPfun_ dflt) : form_scope.
Notation := 'injpPfun_(fun=> point).
Notation := (funpPinj_ dflt) : form_scope.
Notation := 'funpPinj_(fun=> point).

Section function_space.
Local Open Scope ring_scope.
Import GRing.Theory.

Definition { : Type} ( : T') : T -> T' := fun=> x.

Lemma { : Type} ( : aT) ( : set aT) :
@cst rT _ a @^-1` A = if a \in A then setT else set0.

Proof.

apply/seteqP; rewrite /preimage; split; first by move=> *; rewrite mem_set.
by case: ifPn => [/[!inE] ?//|_]; exact: sub0set.
Qed.

Obligation Tactic := idtac.

Section fct_nmodType.
Variables ( : Type) ( : nmodType).
Implicit Types f g h : T -> M.

Let : associative (fun => f \+ g).

Proof.

by move=> f g h; rewrite funeqE=> x /=; rewrite addrA. Qed.

Let : commutative (fun => f \+ g).

Proof.

by move=> f g; rewrite funeqE=> x /=; rewrite addrC. Qed.

Let : left_id \0 (fun => f \+ g).

Proof.

by move=> f; rewrite funeqE=> x /=; rewrite add0r. Qed.

.
.isNmodule.Build (T -> M) \0 (fun => f \+ g) addrA addrC add0r.

End fct_nmodType.

Section fct_zmodType.
Variables ( : Type) ( : zmodType).
Implicit Types f : T -> M.

Let : left_inverse 0 (fun => \- f) +%R.

Proof.

by move=> f; rewrite funeqE=> x /=; rewrite [LHS]addNr. Qed.

.
.Nmodule_isZmodule.Build (T -> M) (fun => \- f) addNr.

End fct_zmodType.

Section fct_pzRingType.
Variables ( : Type) ( : pzRingType).
Implicit Types f g h : T -> M.

Let : associative (fun => f \* g).

Proof.

by move=> f g h; rewrite funeqE=> x /=; rewrite mulrA. Qed.

Let : left_id (cst 1) (fun => f \* g).

Proof.

by move=> f; rewrite funeqE=> x /=; rewrite mul1r. Qed.

Let : right_id (cst 1) (fun => f \* g).

Proof.

by move=> f; rewrite funeqE=> x /=; rewrite mulr1. Qed.

Let : left_distributive (fun => f \* g) +%R.

Proof.

by move=> f g h; rewrite funeqE=> x/=; rewrite mulrDl. Qed.

Let : right_distributive (fun => f \* g) +%R.

Proof.

by move=> f g h; rewrite funeqE=> x/=; rewrite mulrDr. Qed.

..Zmodule_isPzRing.Build (T -> M) (cst 1)
(fun => f \* g) mulrA mul1r mulr1 mulrDl mulrDr.

End fct_pzRingType.

Section fct_nzRingType.
Variables ( : pointedType) ( : nzRingType).

Let : cst 1 != 0 :> (T -> M).

Proof.

by apply/eqP; rewrite funeqE => /(_ point) /eqP; rewrite oner_eq0. Qed.

.
.PzSemiRing_isNonZero.Build (T -> M) oner_neq0.

End fct_nzRingType.

Section fct_comPzRingType.
Variables ( : Type) ( : comPzRingType).

Let : commutative (@GRing.mul (T -> M)).

Proof.

by move=> f g; rewrite funeqE => x; rewrite /GRing.mul/= mulrC. Qed.

.
  GRing.SemiRing_hasCommutativeMul.Build (T -> M) mulrC.

End fct_comPzRingType.

. () (M : comNzRingType) :=
  GRing.ComPzRing.on (T -> M).

Section fct_lmod.
Variables ( : Type) ( : pzRingType) ( : lmodType R).
Program Definition := @GRing.Zmodule_isLmodule.Build R (U -> V)
  (fun => k \*: f) _ _ _ _.

Next Obligation.

by move=> k f v; rewrite funeqE=> x; exact: scalerA. Qed.

Next Obligation.

by move=> f; rewrite funeqE=> x /=; rewrite scale1r. Qed.

Next Obligation.

by move=> f g h; rewrite funeqE => x /=; rewrite scalerDr.
Qed.

Next Obligation.

by move=> f g h; rewrite funeqE => x /=; rewrite scalerDl.
Qed.

..
End fct_lmod.

Lemma ( : Type) ( : nmodType) ( : {pred I}) ( : I -> T -> M) :
\sum_( <- r | P i) f i = fun => \sum_( <- r | P i) f i x.

Proof.

by apply/funext => ?; elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma ( : Type) ( : pzRingType) ( : {pred I})
( : I -> T -> M) :
\prod_( <- r | P i) f i = fun => \prod_( <- r | P i) f i x.

Proof.

by apply/funext => ?; elim/big_rec2: _ => //= i y ? Pi <-. Qed.

Lemma ( : Type) { : comPzSemiRingType} ( : T -> R) ( : R) :
r \*o f = r \o* f.

Proof.

by apply/funext => x/=; rewrite mulrC. Qed.

Lemma ( : Type) ( : numDomainType) ( : T -> T') :
(f \min g) = (f + g) - (f \max g).

Proof.

by apply/funext=> x/=; rewrite Num.Theory.minr_to_max. Qed.

Lemma ( : Type) ( : numDomainType) ( : T -> T') :
(f \max g) = (f + g) - (f \min g).

Proof.

by apply/funext => x/=; rewrite Num.Theory.maxr_to_min. Qed.

Lemma ( : Type) ( : orderType d) ( : T -> T') :
f \max g = g \max f.

Proof.

by apply/funext => z/=; rewrite Order.TotalTheory.maxC. Qed.

Lemma ( : Type) ( : orderType d) ( : T -> T') :
f \min g = g \min f.

Proof.

by apply/funext => z/=; rewrite Order.TotalTheory.minC. Qed.

End function_space.

Section function_space_lemmas.
Local Open Scope ring_scope.
Import GRing.Theory.

Lemma ( : Type) ( : nmodType) ( : T -> K) :
f + g = (fun => f x + g x).

Proof.

by []. Qed.

Lemma ( : Type) ( : nmodType) ( : seq (T -> K)) :
\sum_( <- s) f = (fun => \sum_( <- s) f x).

Proof.

exact: fct_sumE. Qed.

Lemma ( : Type) ( : pzRingType) ( : seq (T -> K)) :
\prod_( <- s) f = (fun => \prod_( <- s) f x).

Proof.

exact: fct_prodE. Qed.

Lemma ( : Type) ( : nmodType) ( : U -> K) :
f *+ n = (fun => f x *+ n).

Proof.

by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.

Lemma ( : Type) ( : zmodType) ( : T -> K) : - f = (fun => - f x).

Proof.

by []. Qed.

Lemma ( : Type) ( : zmodType) :
@interchange (U -> K) (fun => a - b) (fun => a + b).

Proof.

by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed.

Lemma ( : Type) ( : pzRingType) ( : T -> K) :
f * g = (fun => f x * g x).

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) ( : lmodType K)
( : T -> L) :
k *: f = (fun : T => k *: f x).

Proof.

by []. Qed.

Lemma ( : Type) ( : nmodType) : (0 : T -> K) x = 0.

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) : (1 : T -> K) x = 1.

Proof.

by []. Qed.

Lemma ( : Type) ( : T) : cst x = fun _: T' => x.

Proof.

by []. Qed.

Lemma ( : Type) ( : pzRingType) ( : T -> K) :
f ^+ n = (fun => f x ^+ n).

Proof.

by elim: n => [|n h]; rewrite funeqE=> ?; rewrite ?expr0 ?exprS ?h. Qed.

Lemma ( : Type) ( : T1 -> T2) ( : T2 -> T3) :
g \o f = fun => g (f x).

Proof.

by []. Qed.

Definition :=
  (cstE, compE, opprfctE, addrfctE, mulrfctE, scalerfctE, exprfctE,
   zerofctE, onefctE).

Lemma { : Type} { : zmodType} ( : T -> Z) ( : Z) :
  (f \+ g) @^-1`[set z] =
  \bigcup_( in range f) (f @^-1` [set a] `&` g @^-1` [set z - a]).

Proof.

rewrite eqEsubset; split => [x <-|x [a _ /= [<- ->]]].
by exists (f x) => /=; [exact/imageT|rewrite addrC addKr].
by rewrite subrKC.
Qed.

End function_space_lemmas.

#[deprecated(since="mathcomp-analysis 1.17.0", use=scalerfctE)]
Notation := scalerfctE.

Lemma ( : unitRingType) ( : T -> R) : (f\^-1\^-1)%R = f.

Proof.

by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.

Local Open Scope ring_scope.
Import GRing.Theory.

Section linfun_pred.
Context { : numDomainType} { : lmodType K} { : lmodType K}
{ : K -> F -> F}.

Beware that `lfun` is reserved for vector types, hence this one has been named `linfun`

Definition : {pred E -> F} := mem [set | linear_for s f ].

Definition : pred_key linfun

Proof.

exact. Qed.

Canonical := KeyedPred linfun_key.

End linfun_pred.

Section linfun.
Context { : numDomainType} { : lmodType R}
  { : lmodType R} { : GRing.Scale.law R F}.

Notation := {linear E -> F | s}.

Notation := (@linfun _ E F s).

Section Sub.
Context ( : E -> F) ( : f \in linfun).

#[local] Definition :=
  @GRing.isLinear.Build _ E F s f (set_mem fP).

..
Definition : {linear _ -> _ | _ } := f.
End Sub.

Let ( : T -> Type) :
  (forall ( : f \in linfun), K (linfun_Sub Pf)) -> forall : T, K u.

Proof.

move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
set G := (G in K G).
have Pf : f \in linfun by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
suff -> : G = linfun_Sub Pf by apply: Ksub.
rewrite {}/G.
congr (GRing.Linear.Pack (GRing.Linear.Class _ _)).
- by congr GRing.isNmodMorphism.Axioms_; exact: Prop_irrelevance.
- by congr GRing.isScalable.Axioms_; exact: Prop_irrelevance.
Qed.

Let ( : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).

Proof.

by []. Qed.

..Build _ _ T linfun_rect linfun_valP.

Lemma ( : {linear E -> F | s}) : f = g <-> f =1 g.

Proof.

by split=> [->//|fg]; exact/val_inj/funext. Qed.

. of {linear E -> F | s} by <:].

Variant ( : E -> F) : (E -> F) -> bool -> Type :=
| ( : {linear E -> F | s}) : linfun_spec f l true.

Lemma ( : E -> F) : f \in linfun -> linfun_spec f f (f \in linfun).

Proof.

move=> /[dup] f_lc ->.
have {2}-> : f = linfun_Sub f_lc by rewrite linfun_valP.
by constructor.
Qed.

End linfun.

Section linfun_lmodtype.
Context { : numDomainType} { : lmodType R}.
Import GRing.Theory.

Let : submod_closed (@linfun R E F *:%R).

Proof.

split; first by rewrite inE; exact/linearP.
move=> r /= _ _ /linfunP[f] /linfunP[g].
by rewrite inE /=; exact: linearP.
Qed.

.
  .isSubmodClosed.Build _ _ linfun linfun_submod_closed.

.
  [SubChoice_isSubLmodule of {linear E -> F } by <:].

End linfun_lmodtype.

. (E F : lmodType R) :=
  isPointed.Build {linear E -> F} 0.

Files

Module mathcomp.classical.functions