Library mathcomp.analysis.functions
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From HB Require Import structures.
Require Import boolp mathcomp_extra classical_sets.
Add Search Blacklist "__canonical__".
Add Search Blacklist "__functions_".
Add Search Blacklist "_factory_".
Add Search Blacklist "_mixin_".
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From HB Require Import structures.
Require Import boolp mathcomp_extra 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 whose domain and codomain 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
{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}
funin A f == alias for f : aT -> rT, with A : set aT
[fun f in A] == the function f from the set A to the set f @` A
'split d f == partial injection from aT : Type to rt : Type;
f : aT -> rT, d : rT -> aT
split := 'split_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
pinv := notation for 'pinv_point
Section function_space == canonical ringType and lmodType
structures for functions whose range is
a ringType, comRingType, or lmodType.
fctE == multi-rule for fct
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_funSet Implicit Arguments.
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 "[ '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 {aT rT} (A : set aT) (B : set rT) (f : aT → rT).
Definition set_fun := {homo f : x / A x >-> B x}.
Definition set_surj := B `<=` f @` A.
Definition set_inj := {in A &, injective f}.
Definition set_bij := [/\ set_fun, set_inj & set_surj].
End MainProperties.
Notation "{ 'fun' A >-> B }" := (@Fun.type _ _ A B) : form_scope.
Notation "[ 'fun' 'of' f ]" := [the {fun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'oinv' aT >-> rT }" := (@OInversible.type aT rT) : type_scope.
Notation "[ 'oinv' 'of' f ]" := [the {oinv _ >-> _} of f : _ → _] :
form_scope.
Definition phant_oinv aT rT (f : {oinv aT >-> rT})
of phantom (_ → _) f := @oinv _ _ f.
Notation "''oinv_' f" := (@phant_oinv _ _ _ (Phantom (_ → _) f%FUN)).
Notation "{ 'oinvfun' A >-> B }" := (@OInvFun.type _ _ A B) : type_scope.
Notation "[ 'oinvfun' 'of' f ]" :=
[the {oinvfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'inv' aT >-> rT }" := (@Inversible.type aT rT) : type_scope.
Notation "[ 'inv' 'of' f ]" := [the {inv _ >-> _} of f : _ → _] : form_scope.
Definition phant_inv aT rT (f : {inv aT >-> rT}) of phantom (_ → _) f := @inv _ _ f.
Notation "f ^-1" := (@inv _ _ f%FUN) (only printing) : fun_scope.
Notation "f ^-1" := (@inv _ _ f%function) (only printing) : function_scope.
Notation "f ^-1" := (@phant_inv _ _ _ (Phantom (_ → _) f%FUN)) : fun_scope.
Notation "f ^-1" := (@phant_inv _ _ _ (Phantom (_ → _) f%function)) : function_scope.
Notation "{ 'invfun' A >-> B }" := (@InvFun.type _ _ A B) : type_scope.
Notation "[ 'invfun' 'of' f ]" :=
[the {invfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'surj' A >-> B }" := (@Surject.type _ _ A B) : type_scope.
Notation "[ 'surj' 'of' f ]" :=
[the {surj _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'surjfun' A >-> B }" := (@SurjFun.type _ _ A B) : type_scope.
Notation "[ 'surjfun' 'of' f ]" :=
[the {surjfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'splitsurj' A >-> B }" := (@SplitSurj.type _ _ A B) : type_scope.
Notation "[ 'splitsurj' 'of' f ]" :=
[the {splitsurj _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'splitsurjfun' A >-> B }" := (@SplitSurjFun.type _ _ A B) : type_scope.
Notation "[ 'splitsurjfun' 'of' f ]" :=
[the {splitsurjfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'inj' A >-> rT }" := (@Inject.type _ rT A) : type_scope.
Notation "[ 'inj' 'of' f ]" := [the {inj _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'injfun' A >-> B }" := (@InjFun.type _ _ A B) : type_scope.
Notation "[ 'injfun' 'of' f ]" :=
[the {injfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'splitinj' A >-> rT }" := (@SplitInj.type _ rT A) : type_scope.
Notation "[ 'splitinj' 'of' f ]" :=
[the {splitinj _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'splitinjfun' A >-> B }" := (@SplitInjFun.type _ _ A B) : type_scope.
Notation "[ 'splitinjfun' 'of' f ]" :=
[the {splitinjfun _ >-> _} of f : _ → _] : form_scope.
Notation "{ 'bij' A >-> B }" := (@Bij.type _ _ A B) : type_scope.
Notation "[ 'bij' 'of' f ]" := [the {bij _ >-> _} of f] : form_scope.
Notation "{ 'splitbij' A >-> B }" := (@SplitBij.type _ _ A B) : type_scope.
Notation "[ 'splitbij' 'of' f ]" := [the {splitbij _ >-> _} of f] : form_scope.
begin hide
Hint View for move / Inversible.sort inv | 2.
Hint View for apply / Inversible.sort inv | 2.
end hide
Module ShortFunSyntax.
Notation "A ~> B" := {fun A >-> B} (at level 70) : type_scope.
Notation "aT <=> rT" := {oinv aT >-> rT} (at level 70) : type_scope.
Notation "A <~ B" := {oinvfun A >-> B} (at level 70) : type_scope.
Notation "aT <<=> rT" := {inv aT >-> rT} (at level 70) : type_scope.
Notation "A <<~ B" := {invfun A >-> B} (at level 70) : type_scope.
Notation "A =>> B" := {surj A >-> B} (at level 70) : type_scope.
Notation "A ~>> B" := {surjfun A >-> B} (at level 70) : type_scope.
Notation "A ==>> B" := {splitsurj A >-> B} (at level 70) : type_scope.
Notation "A ~~>> B" := {splitsurjfun A >-> B} (at level 70) : type_scope.
Notation "A >=> rT" := {inj A >-> rT} (at level 70) : type_scope.
Notation "A >~> B" := {injfun A >-> B} (at level 70) : type_scope.
Notation "A >>=> rT" := {splitinj A >-> rT} (at level 70) : type_scope.
Notation "A >>~> B" := {splitinjfun A >-> B} (at level 70) : type_scope.
Notation "A <~> B" := {bij A >-> B} (at level 70) : type_scope.
Notation "A <<~> B" := {splitbij A >-> B} (at level 70) : type_scope.
End ShortFunSyntax.
Theory
Definition phant_funS aT rT (A : set aT) (B : set rT)
(f : {fun A >-> B}) of phantom (_ → _) f := @funS _ _ _ _ f.
Notation "'funS_ f" := (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 fun_image_sub aT rT (A : set aT) (B : set rT) (f : {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 mem_fun aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) :=
homo_setP.2 (@funS _ _ _ _ f).
#[global] Hint Extern 0 (prop_in1 _ _) ⇒ solve [apply: mem_fun] : core.
Definition phant_mem_fun aT rT (A : set aT) (B : set rT)
(f : {fun A >-> B}) of phantom (_ → _) f := homo_setP.2 (@funS _ _ _ _ f).
Notation "'mem_fun_ f" := (phant_funS (Phantom (_ → _) f))
(at level 8, f at level 2) : form_scope.
Lemma some_inv {aT rT} (f : {inv aT >-> rT}) x : Some (f^-1 x) = 'oinv_f x.
Definition phant_oinvK aT rT (A : set aT) (B : set rT)
(f : {surj A >-> B}) of phantom (_ → _) f := @oinvK _ _ _ _ f.
Notation "'oinvK_ f" := (phant_oinvK (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve oinvK : core.
Definition phant_oinvS aT rT (A : set aT) (B : set rT)
(f : {surj A >-> B}) of phantom (_ → _) f := @oinvS _ _ _ _ f.
Notation "'oinvS_ f" := (phant_oinvS (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve oinvS : core.
Variant oinv_spec {aT} {rT} {A : set aT} {B : set rT} (f : {surj A >-> B}) y :
rT → option aT → Type :=
OInvSpec (x : aT) of A x & f x = y : oinv_spec f y (f x) (Some x).
Lemma oinvP aT rT (A : set aT) (B : set rT) (f : {surj A >-> B}) y :
B y → oinv_spec f y y ('oinv_f y).
Definition phant_oinvP aT rT (A : set aT) (B : set rT)
(f : {surj A >-> B}) of phantom (_ → _) f := @oinvP _ _ _ _ f.
Notation "'oinvP_ f" := (phant_oinvP (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve oinvP : core.
Lemma oinvT {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}} x :
B x → 'oinv_f x.
Definition phant_oinvT aT rT (A : set aT) (B : set rT)
(f : {surj A >-> B}) of phantom (_ → _) f := @oinvT _ _ _ _ f.
Notation "'oinvT_ f" := (phant_oinvT (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve oinvT : core.
Lemma invK {aT rT} {A : set aT} {B : set rT} {f : {splitsurj A >-> B}} :
{in B, cancel f^-1 f}.
Definition phant_invK aT rT (A : set aT) (B : set rT)
(f : {splitsurj A >-> B}) of phantom (_ → _) f := @invK _ _ _ _ f.
Notation "'invK_ f" := (phant_invK (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve invK : core.
Lemma invS {aT rT} {A : set aT} {B : set rT} {f : {splitsurj A >-> B}} :
{homo f^-1 : x / B x >-> A x}.
Definition phant_invS aT rT (A : set aT) (B : set rT)
{f : {splitsurjfun A >-> B}} of phantom (_ → _) f := @invS _ _ _ _ f.
Notation "'invS_ f" := (phant_invS (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve invS : core.
Definition phant_funoK aT rT (A : set aT) (f : {inj A >-> rT})
of phantom (_ → _) f := @funoK _ _ _ f.
Notation "'funoK_ f" := (phant_funoK (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve funoK : core.
Definition inj {aT rT : nonPropType} {A : set aT} {f : {inj A >-> rT}} :
{in A &, injective f} := pcan_in_inj funoK.
Definition phant_inj aT rT (A : set aT) (f : {inj A >-> rT}) of
phantom (_ → _) f := @inj _ _ _ f.
Notation "'inj_ f" := (phant_inj (Phantom (_ → _) f)) : form_scope.
Definition inj_hint {aT rT} {A : set aT} {f : {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 injT {aT rT} {f : {inj [set: aT] >-> rT}} : injective f.
#[global] Hint Extern 0 (injective _) ⇒ solve [apply: injT] : core.
Lemma funK {aT rT : Type} {A : set aT} {s : {splitinj A >-> rT}} :
{in A, cancel s s^-1}.
Definition phant_funK aT rT (A : set aT) (f : {splitinj A >-> rT})
of phantom (_ → _) f := @funK _ _ _ f.
Notation "'funK_ f" := (phant_funK (Phantom (_ → _) f)) : form_scope.
#[global] Hint Resolve funK : core.
Structure Equality
Preliminary Builders
#[local] Lemma oinvK : {in B, ocancel 'oinv_f f}.
#[local] Lemma oinvS : {homo 'oinv_f : x / B x >-> (some @` A) x}.
Trivial instances
Section OInverse.
Context {aT rT : Type} {A : set aT} {B : set rT}.
Lemma oinvV {f : {oinv aT >-> rT}} : 'oinv_('oinv_f) = omap f.
Lemma surjoinv_inj_subproof (f : {surj A >-> B}) : OInv_Can _ _ B 'oinv_f.
Lemma injoinv_surj_subproof (f : {injfun A >-> B}) :
OInv_CanV _ _ B (some @` A) 'oinv_f.
End OInverse.
Section Inverse.
Context {aT rT : Type} {A : set aT} {B : set rT}.
Lemma invV (f : {inv aT >-> rT}) : f^-1^-1 = f.
End Inverse.
Section Some.
Context {T} {A : set T}.
Lemma oinv_some : 'oinv_(@Some T) = id.
Lemma some_can_subproof : @OInv_Can _ _ A (@Some T).
Lemma some_canV_subproof : OInv_CanV _ _ A (some @` A) (@Some T).
Lemma some_fun_subproof : IsFun _ _ A (some @` A) (@Some T).
End Some.
Section OApply.
Context {aT rT} {A : set aT} {B : set rT} {b0 : rT}.
Lemma inv_oapp {f : {oinv aT >-> rT}} : (oapp f)^-1 = 'oinv_f.
Lemma oinv_oapp {f : {oinv aT >-> rT}} : 'oinv_(oapp f) = olift 'oinv_f.
Lemma inv_oappV {f : {inv aT >-> rT}} : olift f^-1 = (oapp f)^-1.
Lemma oapp_can_subproof (f : {inj A >-> rT}) : Inv_Can _ _ (some @` A) (oapp f).
Lemma oapp_surj_subproof (f : {surj A >-> B}) : Inv_CanV _ _ (some @` A) B (oapp f).
Lemma oapp_fun_subproof (f : {fun A >-> B}) : IsFun _ _ (some @` A) B (oapp f).
End OApply.
Section OBind.
Context {aT rT} {A : set aT} {B : set (option rT)}.
Lemma inv_obind {f : {oinv aT >-> orT}} : (obind f)^-1 = 'oinv_f.
Lemma oinv_obind {f : {oinv aT >-> orT}} : 'oinv_(obind f) = olift 'oinv_f.
Lemma inv_obindV {f : {inv aT >-> orT}} : (obind f)^-1 = olift f^-1.
End OBind.
Section Composition.
Context {aT rT sT} {A : set aT} {B : set rT} {C : set sT}.
Section OInv.
Context {f : {oinv aT >-> rT}} {g : {oinv rT >-> sT}}.
Lemma oinv_comp : 'oinv_(g \o f) = (obind 'oinv_f) \o 'oinv_g.
End OInv.
Section OInv.
Context {f : {inv aT >-> rT}} {g : {inv rT >-> sT}}.
Lemma some_comp_inv : olift (f^-1 \o g^-1) = 'oinv_(g \o f).
Lemma inv_comp : (g \o f)^-1 = f^-1 \o g^-1.
End OInv.
Lemma comp_can_subproof (f : {injfun A >-> B}) (g : {inj B >-> sT}) :
OInv_Can aT sT A (g \o f).
End Composition.
Section Composition.
Context {aT rT sT} {A : set aT} {B : set rT} {C : set sT}.
Lemma comp_surj_subproof (f : {surj A >-> B}) (g : {surj B >-> C}) :
OInv_CanV _ _ A C (g \o f).
End Composition.
Section totalfun.
Context {aT rT : Type}.
Definition totalfun_ (A : set aT) (f : aT → rT) := f.
Context {A : set aT}.
End totalfun.
Notation "''totalfun_' A" := (totalfun_ A) : form_scope.
Notation totalfun := (totalfun_ setT).
Section Olift.
Context {aT rT} {A : set aT} {B : set rT}.
Lemma oinv_olift {f : {oinv aT >-> rT}} : 'oinv_(olift f) = obind 'oinv_f.
End Olift.
Section Map.
Context {aT rT} {A : set aT} {B : set rT}.
Lemma inv_omap {f : {oinv aT >-> rT}} : (omap f)^-1 = obind 'oinv_f.
Lemma oinv_omap {f : {oinv aT >-> rT}} : 'oinv_(omap f) = olift (obind 'oinv_f).
Lemma omapV {f : {inv aT >-> rT}} : omap f^-1 = (omap f)^-1.
End Map.
Builders
Fun in
Section surj_oinv.
Context {aT rT} {A : set aT} {B : set rT} {f : aT → rT} (fsurj : set_surj A B f).
Let surjective_oinv (y : rT) :=
if pselect (B y) is left By then some (projT1 (cid2 (fsurj By))) else None.
Lemma surjective_oinvK : {in B, ocancel surjective_oinv f}.
Lemma surjective_oinvS : set_fun B (some @` A) surjective_oinv.
End surj_oinv.
Coercion surjective_ocanV {aT rT} {A : set aT} {B : set rT} {f : aT → rT}
(fS : set_surj A B f) :=
OCanV.Build aT rT A B f (surjective_oinvS fS) (surjective_oinvK fS).
Section Psurj.
Context {aT rT} {A : set aT} {B : set rT} {f : aT → rT} (fsurj : set_surj A B f).
#[local] HB.instance Definition _ : OCanV _ _ A B f := fsurj.
Definition surjection_of_surj := [surj of f].
Lemma Psurj : {s : {surj A >-> B} | f = s}.
End Psurj.
Coercion surjection_of_surj : set_surj >-> Surject.type.
Lemma oinv_surj {aT rT} {A : set aT} {B : set rT} {f : aT → rT}
(fS : set_surj A B f) y :
'oinv_fS y = if pselect (B y) is left By then some (projT1 (cid2 (fS y By))) else None.
Lemma surj {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}} : set_surj A B f.
Definition phant_surj aT rT (A : set aT) (B : set rT) (f : {surj A >-> B})
of phantom (_ → _) f := @surj _ _ _ _ f.
Notation "'surj_ f" := (phant_surj (Phantom (_ → _) f)) : form_scope.
#[global] Hint Extern 0 (set_surj _ _ _) ⇒ solve [apply: surj] : core.
Section funin_surj.
Context {aT rT : Type}.
Definition funin (A : set aT) (f : aT → rT) := f.
Context {A : set aT} {B : set rT} (f : aT → rT).
Lemma set_fun_image : set_fun A (f @` A) f.
End funin_surj.
Notation "[ 'fun' f 'in' A ]" := (funin A f)
(at level 0, f at next level,
format "[ 'fun' f 'in' A ]") : function_scope.
#[global] Hint Resolve set_fun_image : core.
Partial injection
Section split.
Context {aT rT} (A : set aT) (B : set rT).
Definition split_ (dflt : rT → aT) (f : aT → rT) := f.
Context (dflt : rT → aT).
Section oinv.
Context (f : {oinv aT >-> rT}).
Let g y := odflt (dflt y) ('oinv_f y).
Lemma splitV : (split f)^-1 = g.
End oinv.
Lemma splitis_inj_subproof (f : {inj A >-> rT}) : Inv_Can _ _ A (split f).
Lemma splitid (f : {splitinjfun A >-> B}) : (split f)^-1 = f^-1.
Lemma splitsurj_subproof (f : {surj A >-> B}) : Inv_CanV _ _ A B (split f).
End split.
Notation "''split_' a" := (split_ a) : form_scope.
Notation split := 'split_point.
More Builders
Lemma funoK : {in A, pcancel f 'oinv_f}.
Let g := f.
Let fcan : OInv_Can aT rT A f.
Section Inverses.
Context aT rT {A : set aT} {B : set rT}.
End Inverses.
Simple Factories
Section Pinj.
Context {aT rT} {A : set aT} {f : aT → rT} (finj : {in A &, injective f}).
#[local] HB.instance Definition _ := Inj.Build _ _ _ f finj.
Lemma Pinj : {i : {inj A >-> rT} | f = i}.
End Pinj.
Section Pfun.
Context {aT rT} {A : set aT} {B : set rT} {f : aT → rT}
(ffun : {homo f : x / A x >-> B x}).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := IsFun.Build _ _ _ _ g ffun.
Lemma Pfun : {i : {fun A >-> B} | f = i}.
End Pfun.
Section injPfun.
Context {aT rT} {A : set aT} {B : set rT} {f : {inj A >-> rT}}
(ffun : {homo f : x / A x >-> B x}).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := Inject.on g.
#[local] HB.instance Definition _ := IsFun.Build _ _ A B g ffun.
Lemma injPfun : {i : {injfun A >-> B} | f = i :> (_ → _)}.
End injPfun.
Section funPinj.
Context {aT rT} {A : set aT} {B : set rT} {f : {fun A >-> B}}
(finj : {in A &, injective f}).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := Fun.on g.
#[local] HB.instance Definition _ := Inj.Build _ _ _ g finj.
Lemma funPinj : {i : {injfun A >-> B} | f = i}.
End funPinj.
Section funPsurj.
Context {aT rT} {A : set aT} {B : set rT} {f : {fun A >-> B}}
(fsurj : set_surj A B f).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := Fun.on g.
#[local] HB.instance Definition _ : OCanV _ _ A B g := fsurj.
Lemma funPsurj : {s : {surjfun A >-> B} | f = s}.
End funPsurj.
Section surjPfun.
Context {aT rT} {A : set aT} {B : set rT} {f : {surj A >-> B}}
(ffun : {homo f : x / A x >-> B x}).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := Surject.on g.
#[local] HB.instance Definition _ := IsFun.Build _ _ A B g ffun.
Lemma surjPfun : {s : {surjfun A >-> B} | f = s :> (_ → _)}.
End surjPfun.
Section Psplitinj.
Context {aT rT} {A : set aT} {f : aT → rT} {g} (funK : {in A, cancel f g}).
#[local] HB.instance Definition _ := Can.Build _ _ A f funK.
Lemma Psplitinj : {i : {splitinj A >-> rT} | f = i}.
End Psplitinj.
Section funPsplitinj.
Context {aT rT} {A : set aT} {B : set rT} {f : {fun A >-> B}}.
Context {g} (funK : {in A, cancel f g}).
Let f' : _ → _ := f.
#[local] HB.instance Definition _ := Fun.on f'.
#[local] HB.instance Definition _ := Can.Build _ _ A f' funK.
Lemma funPsplitinj : {i : {splitinjfun A >-> B} | f = i}.
End funPsplitinj.
Lemma PsplitinjT {aT rT} {f : aT → rT} {g} : cancel f g →
{i : {splitinj [set: aT] >-> rT} | f = i}.
Section funPsplitsurj.
Context {aT rT} {A : set aT} {B : set rT} {f : {fun A >-> B}}.
Context {g : {fun B >-> A}} (funK : {in B, cancel g f}).
Let f' : _ → _ := f.
#[local] HB.instance Definition _ := Fun.on f'.
#[local] HB.instance Definition _ := CanV.Build _ _ A B f' funS funK.
Lemma funPsplitsurj : {s : {splitsurjfun A >-> B} | f = s :> (_ → _)}.
End funPsplitsurj.
Lemma PsplitsurjT {aT rT} {f : aT → rT} {g} : cancel g f →
{s : {splitsurjfun [set: aT] >-> [set: rT]} | f = s}.
Instances
The identity is a split bijection
Iteration preserves Fun, Injectivity, and Surjectivity
Section iter_inv.
Context {aT} {A : set aT}.
Section OInv.
Context {f : {oinv aT >-> aT}}.
Lemma oinv_iter n : 'oinv_(iter n f) = iter n (obind 'oinv_f) \o some.
End OInv.
Section OInv.
Context {f : {inv aT >-> aT}}.
Lemma some_iter_inv n : olift (iter n f^-1) = 'oinv_(iter n f).
Lemma inv_iter n : (iter n f)^-1 = iter n f^-1.
End OInv.
Lemma iter_can_subproof n (f : {injfun A >-> A}) : OInv_Can aT aT A (iter n f).
End iter_inv.
Section iter_surj.
Context {aT} {A : set aT}.
Lemma iter_surj_subproof n (f : {surj A >-> A}) : OInv_CanV _ _ A A (iter n f).
End iter_surj.
Unbind
Section Unbind.
Context {aT rT} {A : set aT} {B : set rT} (dflt : aT → rT).
Definition unbind (f : aT → option rT) x := odflt (dflt x) (f x).
Lemma unbind_fun_subproof (f : {fun A >-> some @` B}) : IsFun _ _ A B (unbind f).
Section Oinv.
Context (f : {oinv aT >-> option rT}).
Lemma oinv_unbind : 'oinv_(unbind f) = 'oinv_f \o some.
End Oinv.
Section Inv.
Context (f : {inv aT >-> option rT}).
Lemma inv_unbind_subproof : olift (f^-1 \o some) = 'oinv_(unbind f).
Lemma inv_unbind : (unbind f)^-1 = f^-1 \o some.
End Inv.
Lemma unbind_inj_subproof (f : {injfun A >-> some @` B}) :
@OInv_Can _ _ A (unbind f).
Lemma unbind_surj_subproof (f : {surj A >-> some @` B}) :
@OInv_CanV _ _ A B (unbind f).
End Unbind.
Odflt
Section Odflt.
Context {T} {A : set T} (x : T).
Lemma odflt_unbind : odflt x = unbind (fun⇒ x) idfun.
End Odflt.
Subtypes
Section SubType.
Context {T : Type} {P : pred T} (sT : subType P) (x0 : sT).
Lemma oinv_val : 'oinv_val = insub.
Lemma val_bij_subproof : OInv_Can2 sT T setT [set` P] val.
Lemma inv_insubd : (insubd x0)^-1 = val.
End SubType.
To setT
Definition to_setT {T} (x : T) : [set: T] :=
@SigSub _ _ _ x (mem_set I : x \in setT).
Definition setTbij {T} := [splitbij of @to_setT T].
Lemma inv_to_setT T : (@to_setT T)^-1 = val.
Subfun
Section subfun.
Context {T} {A B : set T}.
Definition subfun (AB : A `<=` B) (a : A) : B :=
SigSub (mem_set (AB _ (set_valP a))).
Lemma subfun_inj {AB : A `<=` B} : injective (subfun AB).
End subfun.
Section subfun_eq.
Context {T} {A B : set T}.
Lemma subfun_imageT (AB : A `<=` B) (BA : B `<=` A) : subfun AB @` setT = setT.
Lemma subfun_inv_subproof (AB : A = B) :
olift (subfun (subsetCW AB)) = 'oinv_(subfun (subsetW AB)).
Add a Inj_Can factory
End subfun_eq.
Section seteqfun.
Context {T : Type}.
Definition seteqfun {A B : set T} (AB : A = B) := subfun (subsetW AB).
Context {A B : set T} (AB : A = B).
Lemma seteqfun_can2_subproof : Inv_Can2 A B setT setT (seteqfun AB).
End seteqfun.
Inclusion
Section incl.
Context {T} {A B : set T}.
Definition incl (AB : A `<=` B) := @id T.
Definition eqincl (AB : A = B) := incl (subsetW AB).
Lemma eqincl_surj AB : Inv_Can2 _ _ A B (eqincl AB).
End incl.
Notation inclT A := (incl (@subsetT _ _)).
Ad hoc function
Section mkfun.
Context {aT} {rT} {A : set aT} {B : set rT}.
Notation isfun f := {homo f : x / A x >-> B x}.
Definition mkfun f (fAB : isfun f) := f.
Definition mkfun_fun f fAB := [fun of @mkfun f fAB].
End mkfun.
set_val
Section set_val.
Context {T} {A : set T}.
Definition set_val : A → T := eqincl (set_mem_set A) \o val.
Lemma oinv_set_val : 'oinv_set_val = insub.
Lemma set_valE : set_val = val.
End set_val.
#[global]
Hint Extern 0 (is_true (set_val _ \in _)) ⇒ solve [apply: valP] : core.
Squash
pickle and unpickle
set0fun
cast_ord
enum_val & enum_rank
Finset val
Definition finset_val {T : choiceType} {X : {fset T}} (x : X) : [set` X] :=
exist (fun x ⇒ x \in [set` X]) (val x) (mem_set (valP x)).
Definition val_finset {T : choiceType} {X : {fset T}} (x : [set` X]) : X :=
[` set_mem (valP x)]%fset.
Lemma finset_valK {T : choiceType} {X : {fset T}} :
cancel (@finset_val T X) val_finset.
Lemma val_finsetK {T : choiceType} {X : {fset T}} :
cancel (@val_finset T X) finset_val.
'I_n and `I_n
Glueing
Definition glue {T T'} {X Y : set T} {A B : set T'}
of [disjoint X & Y] & [disjoint A & B] :=
fun (f g : T → T') (u : T) ⇒ if u \in X then f u else g u.
Section Glue12.
Context {T T'} {X Y : set T} {A B : set T'}.
Context {XY : [disjoint X & Y]} {AB : [disjoint A & B]}.
Definition glue1 (f g : T → T') : {in X, gl f g =1 f}.
Definition glue2 (f g : T → T') : {in Y, gl f g =1 g}.
End Glue12.
Section Glue.
Context {T T'} {X Y : set T} {A B : set T'}.
Context {XY : [disjoint X & Y]} {AB : [disjoint A & B]}.
Lemma glue_fun_subproof (f : {fun X >-> A}) (g : {fun Y >-> B}) :
IsFun T T' (X `|` Y) (A `|` B) (gl f g).
Lemma oinv_glue (f : {oinv T >-> T'}) (g : {oinv T >-> T'}) :
'oinv_(gl f g) = glue AB (eqbRL disj_set_some XY) 'oinv_f 'oinv_g.
Lemma some_inv_glue_subproof (f g : {inv T >-> T'}) :
some \o (glue AB XY f^-1 g^-1) = 'oinv_(gl f g).
Lemma inv_glue (f : {invfun X >-> A}) (g : {invfun Y >-> B}) :
(gl f g)^-1 = glue AB XY f^-1 g^-1.
Lemma glueo_can_subproof (f : {injfun X >-> A}) (g : {injfun Y >-> B}) :
OInv_Can _ _ (X `|` Y) (gl f g).
Lemma glue_canv_subproof (f : {surj X >-> A}) (g : {surj Y >-> B}) :
OInv_CanV _ _ (X `|` Y) (A `|` B) (gl f g).
End Glue.
Z-module addition is a bijection
Section addition.
Context {V : zmodType} (x : V).
Lemma inv_addr : (+%R x)^-1 = (+%R (- x)).
Lemma addr_can2_subproof : Inv_Can2 V V setT setT (+%R x).
End addition.
emtpyType
Section empty.
Context {T : emptyType} {T' : Type} {X : set T}.
Implicit Type Y : set T'.
Lemma empty_can_subproof : OInv_Can T T' X any.
Lemma empty_fun_subproof Y : IsFun T T' X Y any.
Lemma empty_canv_subproof : OInv_CanV T T' X set0 any.
End empty.
Theory of surjection
Section surj_lemmas.
Variables aT rT : Type.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).
Lemma surj_id A : set_surj A A (@idfun aT).
Lemma surj_set0 B f : set_surj set0 B f → B = set0.
Lemma surjE f A B : set_surj A B f = (B `<=` f @` A).
Lemma surj_image_eq B A f : f @` A `<=` B → set_surj A B f → f @` A = B.
Lemma subl_surj A A' B f : A `<=` A' → set_surj A B f → set_surj A' B f.
Lemma subr_surj A B B' f : B' `<=` B → set_surj A B f → set_surj A B' f.
Lemma can_surj g f (A : set aT) (B : set rT) :
{in B, cancel g f} → g @` B `<=` A →
set_surj A B f.
Lemma surj_epi sT A B (f : aT → rT) (g g' : rT → sT) :
set_surj A B f → {in A, g \o f =1 g' \o f} → {in B, g =1 g'}.
Lemma epiP A B (f : aT → rT) : set_surj A B f ↔
∀ sT (g g' : rT → sT), {in A, g \o f =1 g' \o f} → {in B, g =1 g'}.
End surj_lemmas.
Arguments can_surj {aT rT} g [f A B].
Arguments surj_epi {aT rT sT} A {B} f {g}.
Lemma surj_comp T1 T2 T3 (A : set T1) (B : set T2) (C : set T3) f g:
set_surj A B f → set_surj B C g → set_surj A C (g \o f).
Lemma image_eq {aT rT} {A : set aT} {B : set rT} (f : {surjfun A >-> B}) : f @` A = B.
Lemma oinv_image_sub {aT rT : Type} {A : set aT} {B : set rT}
(f : {surj A >-> B}) {C : set rT} :
C `<=` B → 'oinv_f @` C `<=` some @` (f @^-1` C).
Arguments oinv_image_sub {aT rT A B} f {C} _.
Lemma oinv_Iimage_sub {aT rT : Type} {A : set aT} (f : {inj A >-> rT}) {C : set rT} :
C `<=` f @` A → some @` (A `&` f @^-1` C) `<=` 'oinv_f @` C.
Arguments oinv_Iimage_sub {aT rT A} f {C} _.
Lemma oinv_sub_image {aT rT} {A : set aT} {B : set rT} {f : {bij A >-> B}}
{C : set rT} (CB : C `<=` B) : 'oinv_f @` C = some @` (A `&` f @^-1` C).
Arguments oinv_sub_image {aT rT A B} f {C} _.
Lemma inv_image_sub {aT rT : Type} {A : set aT} {B : set rT}
(f : {splitsurj A >-> B}) {C : set rT} :
C `<=` B → f^-1 @` C `<=` f @^-1` C.
Arguments inv_image_sub {aT rT A B} f {C} _.
Lemma inv_Iimage_sub {aT rT : Type} {A : set aT} (f : {splitinj A >-> rT}) {C : set rT} :
C `<=` f @` A → A `&` f @^-1` C `<=` f^-1 @` C.
Arguments inv_Iimage_sub {aT rT A} f {C} _.
Lemma inv_sub_image {aT rT} {A : set aT} {B : set rT} {f : {splitbij A >-> B}}
{C : set rT} (CB : C `<=` B) :
f^-1 @` C = A `&` f @^-1` C.
Arguments inv_sub_image {aT rT A B} f {C} _.
Lemma reindex_bigcup {aT rT I} (f : aT → I) (P : set aT) (Q : set I)
(F : I → set rT) : set_fun P Q f → set_surj P Q f →
\bigcup_(x in Q) F x = \bigcup_(x in P) F (f x).
Arguments reindex_bigcup {aT rT I} f P Q.
Lemma reindex_bigcap {aT rT I} (f : aT → I) (P : set aT) (Q : set I)
(F : I → set rT) : set_fun P Q f → set_surj P Q f →
\bigcap_(x in Q) F x = \bigcap_(x in P) F (f x).
Arguments reindex_bigcap {aT rT I} f P Q.
Lemma bigcap_bigcup T I J (D : set I) (E : set J) (F : I → J → set T) :
J →
\bigcap_(i in D) \bigcup_(j in E) F i j =
\bigcup_(f in set_fun D E) \bigcap_(i in D) F i (f i).
Injections
Lemma trivIset_inj T I (D : set I) (F : I → set T) :
(∀ i, D i → F i !=set0) → trivIset D F → set_inj D F.
Bijections
Section set_bij_lemmas.
Context {aT rT : Type} {A : set aT} {B : set rT} {f : aT → rT}.
Definition fun_set_bij of set_bij A B f := f.
Context (fbij : set_bij A B f).
Lemma set_bij_inj : {in A &, injective f}.
Lemma set_bij_homo : {homo f : x / A x >-> B x}.
Lemma set_bij_sub : f @` A `<=` B.
Lemma set_bij_surj : set_surj A B f.
End set_bij_lemmas.
Coercion fun_set_bij : set_bij >-> Funclass.
Coercion set_bij_bijfun aT rT (A : set aT) (B : set rT) (f : aT → rT)
(fS : set_bij A B f) := Bij.on (fun_set_bij fS).
Section Pbij.
Context {aT rT} {A : set aT} {B : set rT} {f : aT → rT} (fbij : set_bij A B f).
#[local] HB.instance Definition _ : @Bij _ _ A B f := fbij.
Definition bij_of_set_bijection := [bij of f].
Lemma Pbij : {s : {bij A >-> B} | f = s}.
End Pbij.
Coercion bij_of_set_bijection : set_bij >-> Bij.type.
Lemma bij {aT rT} {A : set aT} {B : set rT} {f : {bij A >-> B}} : set_bij A B f.
Definition phant_bij aT rT (A : set aT) (B : set rT) (f : {bij A >-> B}) of
phantom (_ → _) f := @bij _ _ _ _ f.
Notation "''bij_' f" := (phant_bij (Phantom (_ → _) f)) : form_scope.
#[global] Hint Extern 0 (set_bij _ _ _) ⇒ solve [apply: bij] : core.
Section PbijTT.
Context {aT rT} {f : aT → rT} (fbijTT : bijective f).
#[local] HB.instance Definition _ := @BijTT.Build _ _ f fbijTT.
Definition bijection_of_bijective := [splitbij of f].
Lemma PbijTT : {s : {splitbij [set: aT] >-> [set: rT]} | f = s}.
End PbijTT.
Lemma setTT_bijective aT rT (f : aT → rT) :
set_bij [set: aT] [set: rT] f = bijective f.
Lemma bijTT {aT rT} {f : {bij [set: aT] >-> [set: rT]}} : bijective f.
Definition phant_bijTT aT rT (f : {bij [set: aT] >-> [set: rT]})
of phantom (_ → _) f := @bijTT _ _ f.
Notation "''bijTT_' f" := (phant_bijTT (Phantom (_ → _) f)) : form_scope.
#[global] Hint Extern 0 (bijective _) ⇒ solve [apply: bijTT] : core.
Patching and restrictions
Section patch.
Context {aT rT : Type} (d : aT → rT) (A : set aT).
Definition patch (f : aT → rT) u := if u \in A then f u else d u.
Lemma patchT f : {in A, patch f =1 f}.
Lemma patchN f : {in [predC A], patch f =1 d}.
Lemma patchC f : {in ~` A, patch f =1 d}.
Section inj.
Context (f : {inj A >-> rT}).
Let g := patch f.
Lemma patch_inj_subproof : Inj aT rT A g.
End inj.
End patch.
Notation restrict := (patch (fun⇒ point)).
Notation "f \_ D" := (restrict D f) : fun_scope.
Lemma patch_pred {I T} (D : {pred I}) (d f : I → T) :
patch d D f = fun i ⇒ if D i then f i else d i.
Lemma preimage_restrict (aT : Type) (rT : pointedType)
(f : aT → rT) (D : set aT) (B : set rT) :
(f \_ D) @^-1` B = (if point \in B then ~` D else set0) `|` D `&` f @^-1` B.
Lemma comp_patch {aT rT sT : Type} (g : aT → rT) D (f : aT → rT) (h : rT → sT) :
h \o patch g D f = patch (h \o g) D (h \o f).
Lemma patch_setI {aT rT : Type} (g : aT → rT) D D' (f : aT → rT) :
patch g (D `&` D') f = patch g D (patch g D' f).
Lemma patch_set0 {aT rT : Type} (g : aT → rT) (f : aT → rT) :
patch g set0 f = g.
Lemma patch_setT {aT rT : Type} (g : aT → rT) (f : aT → rT) :
patch g setT f = f.
Lemma restrict_comp {aT} {rT sT : pointedType} (h : rT → sT) (f : aT → rT) D :
h point = point → (h \o f) \_ D = h \o (f \_ D).
Arguments restrict_comp {aT rT sT} h f D.
Lemma trivIset_restr (T I : Type) (D D' : set I) (F : I → set T) :
trivIset D' (F \_ D) = trivIset (D `&` D') F.
Restriction of domain and codomain
Section RestrictionLeft.
Context {U V : Type} (v : V) {A : set U} {B : set V}.
Definition sigL (f : U → V) : A → V := f \o set_val.
Lemma sigL_isfun (f : {fun A >-> B}) : IsFun _ _ [set: A] B (sigL f).
Definition sigLfun (f : {fun A >-> B}) := [fun of sigL f].
Definition valL_ (f : A → V) : U → V := ((@oapp _ _)^~ v) f \o 'oinv_set_val.
Lemma valL_isfun (f : {fun [set: A] >-> B}) :
IsFun _ _ A B (valL_ (f : _ → _)).
Definition valLfun_ (f : {fun [set: A] >-> B}) := [fun of valL_ f].
Lemma sigLE (f : U → V) x (xA : x \in A) :
sigL f (SigSub xA) = f x.
Lemma eq_sigLP (f g : U → V):
{in A, f =1 g} ↔ sigL f = sigL g.
Lemma eq_sigLfunP (f g : {fun A >-> B}) :
{in A, f =1 g} ↔ sigLfun f = sigLfun g.
Lemma sigLK : valL_ \o sigL = restrict.
Lemma valLK : cancel valL_ sigL.
Lemma valLfunK : cancel valLfun_ sigLfun.
Lemma sigL_valL : sigL \o valL_ = id.
Lemma sigL_valLfun : sigLfun \o valLfun_ = id.
Lemma sigL_restrict : sigL \o restrict = sigL.
Lemma image_sigL : range sigL = setT.
Lemma eq_restrictP (f g : U → V): {in A, f =1 g} ↔ restrict f = restrict g.
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" := (valL_ v) : form_scope.
Notation "''valLfun_' v" := (valLfun_ v) : form_scope.
Notation valL := (valL_ point).
Section RestrictionRight.
Context {U V : Type} {A : set V}.
Definition sigR (f : {fun [set: U] >-> A}) (u : U) : A :=
SigSub (mem_set ('funS_f I) : f u \in A).
Definition valR (f : U → A) := set_val \o totalfun f.
Definition valR_fun (f : U → A) : {fun [set: U] >-> A} := [fun of valR f].
Lemma sigRK (f : {fun [set: U] >-> A}) : valR (sigR f) = f.
Lemma sigR_funK (f : {fun [set: U] >-> A}) : valR_fun (sigR f) = f.
Lemma valRP (f : U → A) x : A (valR f x).
Lemma valRK : cancel valR_fun sigR.
End RestrictionRight.
Arguments sigR {U V A} f u /.
Section RestrictionLeftInv.
Context {U V : Type} (v : V) {A : set U} {B : set V}.
Lemma oinv_sigL (f : {oinv U >-> V}) : 'oinv_(rl f) = obind insub \o 'oinv_f.
Lemma sigL_inj_subproof (f : {inj A >-> V}) : @OInv_Can _ _ setT (rl f).
Lemma sigL_surj_subproof (f : {surj A >-> B}) : @OInv_CanV _ _ setT B (rl f).
Lemma oinv_sigR (f : {oinvfun [set: V] >-> A}) :
'oinv_(rr f) = (rl 'oinv_f).
Lemma sigR_inj_subproof (f : {injfun [set: V] >-> A}) :
@OInv_Can _ _ setT (rr f).
Lemma sigR_surj_subproof (f : {surjfun [set: V] >-> A}) :
@OInv_CanV _ _ setT setT (rr f).
Lemma sigR_some_inv (f : {invfun [set: V] >-> A}) :
olift (rl f^-1) = 'oinv_(rr f).
Lemma inv_sigR (f : {invfun [set: V] >-> A}) : (rr f)^-1 = (rl f^-1).
HB Bug, if Fun.on instead of Surject.on
Lemma sigL_some_inv (f : {splitbij A >-> [set: V]}) :
olift (rr [fun of f^-1]) = 'oinv_(rl f).
Lemma inv_sigL (f : {splitbij A >-> [set: V]}) :
(rl f)^-1 = (rr [fun of f^-1]).
Lemma oinv_valL (f : {oinv A >-> V}) :
'oinv_(el f) = omap set_val \o 'oinv_f.
Lemma oapp_comp_x {aT rT sT} (f : aT → rT) (g : rT → sT) (x : rT) y :
oapp (g \o f) (g x) y = g (oapp f x y).
Lemma valL_inj_subproof (f : {inj [set: A] >-> V}) : @OInv_Can _ _ A (el f).
Lemma valL_surj_subproof (f : {surj [set: A] >-> B}) : @OInv_CanV _ _ A B (el f).
Lemma valL_some_inv (f : {inv A >-> V}) : olift (er f^-1) = 'oinv_(el f).
Lemma inv_valL (f : {inv A >-> V}) : (el f)^-1 = er f^-1.
HB Bug, if Fun.on instead of Surject.on
Lemma sigL_injP (f : U → V) :
injective (rl f) ↔ {in A &, injective f}.
Lemma sigL_surjP (f : U → V) :
set_surj [set: A] B (rl f) ↔ set_surj A B f.
Lemma sigL_funP (f : U → V) :
set_fun [set: A] B (rl f) ↔ set_fun A B f.
Lemma sigL_bijP (f : U → V) :
set_bij [set: A] B (rl f) ↔ set_bij A B f.
Lemma valL_injP (f : A → V) : {in A &, injective (el f)} ↔ injective f.
Lemma valL_surjP (f : A → V) :
set_surj A B (el f) ↔ set_surj setT B f.
Lemma valLfunP (f : A → V) :
set_fun A B (el f) ↔ set_fun setT B f.
Lemma valL_bijP (f : A → V) :
set_bij A B (el f) ↔ set_bij setT B f.
End RestrictionLeftInv.
Section ExtentionLeftInv.
Context {U V : Type} {A : set U} {B : set V}.
Lemma oinv_valR (f : {oinv V >-> A}) : 'oinv_(er f) = (el 'oinv_f).
Lemma valR_inj_subproof (f : {inj [set: V] >-> A}) :
@OInv_Can _ _ setT (er f).
Lemma valR_surj_subproof (f : {surj [set: V] >-> [set: A]}) :
@OInv_CanV _ _ setT A (er f).
End ExtentionLeftInv.
Section Restrictions2.
Context {U V : Type} (v : V) {A : set U} {B : set V}.
Definition sigLR := sigR \o (@sigLfun U V A B).
Definition valLR : (A → B) → U → V := valL \o valR_fun.
Definition valLRfun : (A → B) → {fun A >-> B} := valLfun \o valR_fun.
Lemma valLRE (f : A → B) : valLR f = valL (valR f).
Lemma valLRfunE (f : A → B) : valLRfun f = [fun of valLR f].
Lemma sigL2K (f : {fun A >-> B}) : {in A, valLR (sigLR f) =1 f}.
Lemma valLRK : cancel valLRfun sigLR.
Lemma valLRfun_inj : injective valLRfun.
Lemma sigLR_injP (f : {fun A >-> B}) :
injective (sigLR f) ↔ {in A &, injective f}.
Lemma valLR_injP (f : A → B) :
{in A &, injective (valLR f)} ↔ injective f.
Lemma sigLR_surjP (f : {fun A >-> B}) :
set_surj setT setT (sigLR f) ↔ set_surj A B f.
Lemma valLR_surjP (f : A → B) :
set_surj A B (valLR f) ↔ set_surj setT setT f.
Lemma sigLR_bijP (f : U → V) :
set_bij A B f ↔
∃ (fAB : {homo f : x / A x >-> B x}),
bijective (sigLR [fun of mkfun fAB]).
Lemma sigLRfun_bijP f : bijective (sigLR f) ↔ set_bij A B f.
Lemma valLR_bijP f : set_bij A B (valLR f) ↔ bijective f.
End Restrictions2.
Lemma subsetP {T} {A B : set T} : {subset A ≤ B} ↔ (A `<=` B).
Section set_bij_basic_lemmas.
Context {aT rT : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).
Lemma eq_set_bijRL A B f g : {in A, f =1 g} → set_bij A B f → set_bij A B g.
Lemma eq_set_bijLR A B f g : {in A, f =1 g} → set_bij A B g → set_bij A B f.
Lemma eq_set_bij A B f g : {in A, f =1 g} → set_bij A B f = set_bij A B g.
Lemma bij_omap A B f :
set_bij (some @` A) (some @` B) (omap f) ↔ set_bij A B f.
Lemma bij_olift A B f : set_bij A (some @` B) (olift f) ↔ set_bij A B f.
End set_bij_basic_lemmas.
Lemma bij_sub_sym {aT rT} {A C : set aT} {B D : set rT}
(f : {bij A >-> B}) : C `<=` A → D `<=` B →
set_bij D (some @` C) 'oinv_f ↔ set_bij C D f.
Lemma splitbij_sub_sym {aT rT} {A C : set aT} {B D : set rT}
(f : {splitbij A >-> B}) : C `<=` A → D `<=` B →
set_bij D C f^-1 ↔ set_bij C D f.
Section set_bij_lemmas.
Context {aT rT : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).
Lemma set_bij00 T U (f : T → U) : set_bij set0 set0 f.
Hint Resolve set_bij00 : core.
Lemma inj_bij A f : {in A &, injective f} → set_bij A (f @` A) f.
Lemma bij_subl A B C D (f : {bij A >-> B}) : C `<=` A → f @` C = D →
set_bij C D f.
End set_bij_lemmas.
Section set_bij_lemmas.
Context {aT rT : Type}.
Implicit Types (A : set aT) (B : set rT) (f : aT → rT).
Lemma bij_subr A B C D (f : {bij A >-> B}) : C = A `&` (f @^-1` D) → D `<=` B →
set_bij C D f.
Lemma bij_sub A B C D (f : {bij A >-> B}) : C `<=` A → D `<=` B →
{homo f : x / C x >-> D x} →
{homo 'oinv_f : x / D x >-> (some @` C) x} →
set_bij C D f.
Lemma splitbij_sub A B C D (f : {splitbij A >-> B}) : C `<=` A → D `<=` B →
{homo f : x / C x >-> D x} →
{homo f^-1 : x / D x >-> C x} →
set_bij C D f.
Lemma can2_bij A B (f : {fun A >-> B}) (g : {fun B >-> A}) :
{in A, cancel f g} → {in B, cancel g f} → set_bij A B f.
Lemma bij_sub_setUrl A B B' f : [disjoint B & B'] →
set_bij A (B `|` B') f → set_bij (A `\` f @^-1` B') B f.
Lemma bij_sub_setUrr A B B' f : [disjoint B & B'] →
set_bij A (B `|` B') f → set_bij (A `\` f @^-1` B) B' f.
Lemma bij_sub_setUll A A' B f : [disjoint A & A'] →
set_bij (A `|` A') B f → set_bij A (B `\` f @` A') f.
Lemma bij_sub_setUlr A A' B f : [disjoint A & A'] →
set_bij (A `|` A') B f → set_bij A' (B `\` f @` A) f.
End set_bij_lemmas.
Lemma bij_II_D1 T n (A : set T) (f : nat → T) :
set_bij `I_n.+1 A f → set_bij `I_n (A `\ f n) f.
Lemma set_bij_comp T1 T2 T3 (A : set T1) (B : set T2) (C : set T3) f g :
set_bij A B f → set_bij B C g → set_bij A C (g \o f).
Section pointed_inverse.
Context {T U} (dflt : U → T) (A : set T).
Implicit Types (f : T → U) (i : {inj A >-> U}).
Definition pinv_ f := ('split_dflt [fun f in A])^-1.
Lemma pinvK f : {in f @` A, cancel (pinv f) f}.
Lemma pinvKV f : {in A &, injective f} → {in A, cancel f (pinv f)}.
Lemma injpinv_surj f : {in A &, injective f} →
set_surj (f @` A) A (pinv f).
Lemma injpinv_image f : {in A &, injective f} →
pinv f @` (f @` A) = A.
Lemma injpinv_bij f : {in A &, injective f} →
set_bij (f @` A) A (pinv f).
Lemma surjpK B f : set_surj A B f → {in B, cancel (pinv f) f}.
Lemma surjpinv_image_sub B f : set_surj A B f → pinv f @` B `<=` A.
Lemma surjpinv_inj B f : set_surj A B f → {in B &, injective (pinv f)}.
Lemma surjpinv_bij B f (g := pinv f) : set_surj A B f →
set_bij B (g @` B) g.
Lemma bijpinv_bij B f : set_bij A B f → set_bij B A (pinv f).
Section pPbij.
Context {B: set U} {f : T → U} (fbij : set_bij A B f).
Lemma pPbij_ : {s : {splitbij A >-> B} | f = s}.
End pPbij.
Section pPinj.
Context {f : T → U} (finj : {in A &, injective f}).
Lemma pPinj_ : {i : {splitinj A >-> U} | f = i}.
End pPinj.
Section injpPfun.
Context {B : set U} {f : {inj A >-> U}} (ffun : {homo f : x / A x >-> B x}).
Let g : _ → _ := f.
#[local] HB.instance Definition _ := SplitInj.copy g ('split_dflt [fun g in A]).
#[local] HB.instance Definition _ := IsFun.Build _ _ _ _ g ffun.
Lemma injpPfun_ : {i : {splitinjfun A >-> B} | f = i :> (_ → _)}.
End injpPfun.
Section funpPinj.
Context {B : set U} {f : {fun A >-> B}} (finj : {in A &, injective f}).
Lemma funpPinj_ : {i : {splitinjfun A >-> B} | f = i :> (_ → _)}.
End funpPinj.
End pointed_inverse.
Notation "''pinv_' dflt" := (pinv_ dflt) : form_scope.
Notation pinv := 'pinv_point.
Notation "''pPbij_' dflt" := (pPbij_ dflt) : form_scope.
Notation pPbij := 'pPbij_point.
Notation selfPbij := 'pPbij_id.
Notation "''pPinj_' dflt" := (pPinj_ dflt) : form_scope.
Notation pPinj := 'pPinj_point.
Notation "''injpPfun_' dflt" := (injpPfun_ dflt) : form_scope.
Notation injpPfun := 'injpPfun_point.
Notation "''funpPinj_' dflt" := (funpPinj_ dflt) : form_scope.
Notation funpPinj := 'funpPinj_point.
Section function_space.
Local Open Scope ring_scope.
Import GRing.Theory.
Definition cst {T T' : Type} (x : T') : T → T' := fun⇒ x.
Lemma preimage_cst {aT rT : Type} (a : aT) (A : set aT) :
@cst rT _ a @^-1` A = if a \in A then setT else set0.
Obligation Tactic := idtac.
Program Definition fct_zmodMixin (T : Type) (M : zmodType) :=
@ZmodMixin (T → M) \0 (fun f x ⇒ - f x) (fun f g ⇒ f \+ g) _ _ _ _.
Canonical fct_zmodType T (M : zmodType) := ZmodType (T → M) (fct_zmodMixin T M).
Program Definition fct_ringMixin (T : pointedType) (M : ringType) :=
@RingMixin [zmodType of T → M] (cst 1) (fun f g ⇒ f \* g)
_ _ _ _ _ _.
Canonical fct_ringType (T : pointedType) (M : ringType) :=
RingType (T → M) (fct_ringMixin T M).
Program Canonical fct_comRingType (T : pointedType) (M : comRingType) :=
ComRingType (T → M) _.
Program Definition fct_lmodMixin (U : Type) (R : ringType) (V : lmodType R)
:= @LmodMixin R [zmodType of U → V] (fun k f ⇒ k \*: f) _ _ _ _.
Canonical fct_lmodType U (R : ringType) (V : lmodType R) :=
LmodType _ (U → V) (fct_lmodMixin U V).
Lemma fct_sumE (I T : Type) (M : zmodType) r (P : {pred I}) (f : I → T → M)
(x : T) :
(\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
End function_space.
Section function_space_lemmas.
Local Open Scope ring_scope.
Import GRing.Theory.
Lemma addrfctE (T : Type) (K : zmodType) (f g : T → K) :
f + g = (fun x ⇒ f x + g x).
Lemma opprfctE (T : Type) (K : zmodType) (f : T → K) : - f = (fun x ⇒ - f x).
Lemma mulrfctE (T : pointedType) (K : ringType) (f g : T → K) :
f × g = (fun x ⇒ f x × g x).
Lemma scalrfctE (T : pointedType) (K : ringType) (L : lmodType K)
k (f : T → L) :
k *: f = (fun x : T ⇒ k *: f x).
Lemma cstE (T T': Type) (x : T) : cst x = fun _: T' ⇒ x.
Lemma exprfctE (T : pointedType) (K : ringType) (f : T → K) n :
f ^+ n = (fun x ⇒ f x ^+ n).
Lemma compE (T1 T2 T3 : Type) (f : T1 → T2) (g : T2 → T3) :
g \o f = fun x ⇒ g (f x).
Definition fctE :=
(cstE, compE, opprfctE, addrfctE, mulrfctE, scalrfctE, exprfctE).
End function_space_lemmas.