diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.ssreflect.finfun.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.finfun.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.finfun.html | 378 |
1 files changed, 253 insertions, 125 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.finfun.html b/docs/htmldoc/mathcomp.ssreflect.finfun.html index 7af1bac..c0de196 100644 --- a/docs/htmldoc/mathcomp.ssreflect.finfun.html +++ b/docs/htmldoc/mathcomp.ssreflect.finfun.html @@ -21,28 +21,57 @@ <div class="code"> <span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> Distributed under the terms of CeCILL-B. *)</span><br/> -<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> <br/> </div> <div class="doc"> This file implements a type for functions with a finite domain: - {ffun aT -> rT} where aT should have a finType structure. + {ffun aT -> rT} where aT should have a finType structure, + {ffun forall x : aT, rT} for dependent functions over a finType aT, + and {ffun funT} where funT expands to a product over a finType. Any eqType, choiceType, countType and finType structures on rT extend to {ffun aT -> rT} as Leibnitz equality and extensional equalities coincide. (T ^ n)%type is notation for {ffun 'I_n -> T}, which is isomorphic - to n.-tuple T. - For f : {ffun aT -> rT}, we define + to n.-tuple T, but is structurally positive and thus can be used to + define inductive types, e.g., Inductive tree := node n of tree ^ n (see + mid-file for an expanded example). +> More generally, {ffun fT} is always structurally positive. + {ffun fT} inherits combinatorial structures of rT, i.e., eqType, + choiceType, countType, and finType. However, due to some limitations of + the Coq 8.9 unification code the structures are only inherited in the + NON dependent case, when rT does not depend on x. + For f : {ffun fT} with fT := forall x : aT, rT we define f x == the image of x under f (f coerces to a CiC function) - fgraph f == the graph of f, i.e., the #|aT|.-tuple rT of the - values of f over enum aT. - finfun lam == the f such that f =1 lam; this is the RECOMMENDED - interface to build an element of {ffun aT -> rT}. - [ffun x => expr] == finfun (fun x => expr) - [ffun => expr] == finfun (fun _ => expr) - f \in ffun_on R == the range of f is a subset of R +> The coercion is structurally decreasing, e.g., Coq will accept + Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1. + as structurally decreasing on t of the inductive tree type above. + {dffun fT} == alias for {ffun fT} that inherits combinatorial + structures on rT, when rT DOES depend on x. + total_fun g == the function induced by a dependent function g of type + forall x, rT on the total space {x : aT & rT}. + := fun x => Tagged (fun x => rT) (g x). + tfgraph f == the total function graph of f, i.e., the #|aT|.-tuple + of all the (dependent pair) values of total_fun f. + finfun g == the f extensionally equal to g, and the RECOMMENDED + interface for building elements of {ffun fT}. + [ffun x : aT => E] := finfun (fun x : aT => E). + There should be an explicit type constraint on E if + type does not depend on x, due to the Coq unification + limitations referred to above. + ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. f \in family F == f belongs to the family F (f x \in F x for all x) + There are addidional operations for non-dependent finite functions, + i.e., f in {ffun aT -> rT}. + [ffun x => E] := finfun (fun x => E). + The type of E must not depend on x; this restriction + is a mitigation of the aforementioned Coq unification + limitations. + [ffun=> E] := [ffun _ => E] (E should not have a dependent type). + fgraph f == the function graph of f, i.e., the #|aT|.-tuple + listing the values of f x, for x ranging over enum aT. + Finfun G == the finfun f whose (simple) function graph is G. + f \in ffun_on R == the range of f is a subset of R. y.-support f == the y-support of f, i.e., [pred x | f x != y]. Thus, y.-support f \subset D means f has y-support D. We will put Notation support := 0.-support in ssralg. @@ -60,143 +89,262 @@ <span class="id" title="keyword">Section</span> <a name="Def"><span class="id" title="section">Def</span></a>.<br/> <br/> -<span class="id" title="keyword">Variables</span> (<a name="Def.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Def.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="Def.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Def.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span>).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="finfun_type"><span class="id" title="inductive">finfun_type</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> := <a name="Finfun"><span class="id" title="constructor">Finfun</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a>.<br/> +<span class="id" title="keyword">Inductive</span> <a name="finfun_on"><span class="id" title="inductive">finfun_on</span></a> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> +| <a name="finfun_nil"><span class="id" title="constructor">finfun_nil</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_on"><span class="id" title="inductive">finfun_on</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a><br/> +| <a name="finfun_cons"><span class="id" title="constructor">finfun_cons</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> & <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_on"><span class="id" title="inductive">finfun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#s"><span class="id" title="variable">s</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_on"><span class="id" title="inductive">finfun_on</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#s"><span class="id" title="variable">s</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="finfun_of"><span class="id" title="definition">finfun_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a>.<br/> <br/> -<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_of_finfun</span> : <span class="id" title="var">finfun_of</span> >-> <span class="id" title="var">finfun_type</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="fgraph"><span class="id" title="definition">fgraph</span></a> <span class="id" title="var">f</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.finfun.html#Finfun"><span class="id" title="constructor">Finfun</span></a> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">t</span>.<br/> +<span class="id" title="keyword">Variant</span> <a name="finfun_of"><span class="id" title="inductive">finfun_of</span></a> (<span class="id" title="var">ph</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> :=<br/> + <a name="FinfunOf"><span class="id" title="constructor">FinfunOf</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_on"><span class="id" title="inductive">finfun_on</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum"><span class="id" title="abbreviation">enum</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a>).<br/> <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">newType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="dfinfun_of"><span class="id" title="definition">dfinfun_of</span></a> <span class="id" title="var">ph</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="inductive">finfun_of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ph"><span class="id" title="variable">ph</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> <span class="id" title="var">ph</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="inductive">finfun_of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ph"><span class="id" title="variable">ph</span></a>) <span class="id" title="var">x</span> :=<br/> + <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunOf"><span class="id" title="constructor">FinfunOf</span></a> <span class="id" title="var">f_aT</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_rec"><span class="id" title="definition">fun_of_fin_rec</span></a> <span class="id" title="var">f_aT</span> (<a class="idref" href="mathcomp.ssreflect.fintype.html#mem_enum"><span class="id" title="lemma">mem_enum</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>).<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def"><span class="id" title="section">Def</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">"</span></a>{ 'ffun' fT }" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="definition">finfun_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">fT</span>))<br/> +<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">finfun_of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">Funclass</span></a>.<br/> +<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">unfold_dfinfun_of</span> : <span class="id" title="var">dfinfun_of</span> >-> <span class="id" title="var">finfun_of</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">"</span></a>{ 'ffun' fT }" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="inductive">finfun_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">fT</span>))<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'ffun' '[hv' fT ']' }") : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#ordinal_finType"><span class="id" title="definition">ordinal_finType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#n"><span class="id" title="variable">n</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="cd1bca6dfdb74a6b15c6c8969f27472a"><span class="id" title="notation">"</span></a>T ^ n" := (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="definition">finfun_of</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> <span class="id" title="var">n</span>) <span class="id" title="var">T</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)) : <span class="id" title="var">type_scope</span>.<br/> <br/> +<span class="id" title="keyword">Notation</span> <a name="15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">"</span></a>{ 'dffun' fT }" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#dfinfun_of"><span class="id" title="definition">dfinfun_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">fT</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'dffun' '[hv' fT ']' }") : <span class="id" title="var">type_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#ordinal_finType"><span class="id" title="definition">ordinal_finType</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="c93a2e1bb8503fc4a9598804b268d1be"><span class="id" title="notation">"</span></a>T ^ n" :=<br/> + (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="inductive">finfun_of</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> <span class="id" title="var">n</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">T</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)) : <span class="id" title="var">type_scope</span>.<br/> <br/> <br/> -<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/> -<span class="id" title="keyword">Parameter</span> <a name="FunFinfunSig.fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>.<br/> -<span class="id" title="keyword">Parameter</span> <a name="FunFinfunSig.finfun"><span class="id" title="axiom">finfun</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) <span class="id" title="var">rT</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Axiom</span> <a name="FunFinfunSig.fun_of_finE"><span class="id" title="axiom">fun_of_finE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig.fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>.<br/> -<span class="id" title="keyword">Axiom</span> <a name="FunFinfunSig.finfunE"><span class="id" title="axiom">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig.finfun"><span class="id" title="axiom">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/> +<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="FinfunDefSig"><span class="id" title="module">FinfunDefSig</span></a>.<br/> +<span class="id" title="keyword">Parameter</span> <a name="FinfunDefSig.finfun"><span class="id" title="axiom">finfun</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#finPi"><span class="id" title="abbreviation">finPi</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finPi"><span class="id" title="abbreviation">finPi</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Axiom</span> <a name="FinfunDefSig.finfunE"><span class="id" title="axiom">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunDefSig.finfun"><span class="id" title="axiom">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunDefSig"><span class="id" title="module">FinfunDefSig</span></a>.<br/> <br/> -<span class="id" title="keyword">Module</span> <a name="FunFinfun"><span class="id" title="module">FunFinfun</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="FunFinfun.fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="FunFinfun.finfun"><span class="id" title="definition">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="FunFinfun.fun_of_finE"><span class="id" title="lemma">fun_of_finE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun.fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="FunFinfun.finfunE"><span class="id" title="lemma">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun.finfun"><span class="id" title="definition">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>. <br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun"><span class="id" title="module">FunFinfun</span></a>.<br/> +<span class="id" title="keyword">Module</span> <a name="FinfunDef"><span class="id" title="module">FinfunDef</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunDefSig"><span class="id" title="module">FinfunDefSig</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FinfunDef.finfun"><span class="id" title="definition">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FinfunDef.finfunE"><span class="id" title="lemma">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunDef.finfun"><span class="id" title="definition">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>. <br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinfunDef"><span class="id" title="module">FinfunDef</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="fun_of_fin"><span class="id" title="abbreviation">fun_of_fin</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">FunFinfun.fun_of_fin</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="finfun"><span class="id" title="abbreviation">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="axiom">FunFinfun.finfun</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">>-></span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">Funclass</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fun_of_fin_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_finE"><span class="id" title="axiom">FunFinfun.fun_of_finE</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfunE"><span class="id" title="axiom">FunFinfun.finfunE</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="finfun"><span class="id" title="abbreviation">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="axiom">FinfunDef.finfun</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfunE"><span class="id" title="axiom">FinfunDef.finfunE</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">"</span></a>[ 'ffun' x : aT => F ]" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">aT</span> ⇒ <span class="id" title="var">F</span>))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="e4e2ffb93b77700f7a723d1db6d75bdf"><span class="id" title="notation">"</span></a>[ 'ffun' x : aT => E ]" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">aT</span> ⇒ <span class="id" title="var">E</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>) : <span class="id" title="var">fun_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">"</span></a>[ 'ffun' : aT => F ]" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> : <span class="id" title="var">aT</span> ⇒ <span class="id" title="var">F</span>))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">"</span></a>[ 'ffun' x => E ]" := (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">_</span>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <span class="id" title="var">E</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "[ 'ffun' x => E ]") : <span class="id" title="var">fun_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="71fbd02a8ba525d8dcd88d59800c905e"><span class="id" title="notation">"</span></a>[ 'ffun' x => F ]" := <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">ffun</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">:</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">F</span><a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">]</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">format</span> "[ 'ffun' x => F ]") : <span class="id" title="var">fun_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="765311140842c5fd14103e5433ef110e"><span class="id" title="notation">"</span></a>[ 'ffun' => E ]" := <a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">ffun</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">E</span><a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">]</span></a><br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'ffun' => E ]") : <span class="id" title="var">fun_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="ce31ffdcdad2ff7a7492eb6a19fd59e9"><span class="id" title="notation">"</span></a>[ 'ffun' => F ]" := <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">:</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">F</span><a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">]</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'ffun' => F ]") : <span class="id" title="var">fun_scope</span>.<br/> +<span class="comment">(* Example outcommented.<br/> +<span class="comment">(** Examples of using finite functions as containers in recursive inductive <br/> + types, and making use of the fact that the type and accessor are <br/> + structurally positive and decreasing, respectively. **)</span><br/> +Unset Elimination Schemes.<br/> +Inductive tree := node n of tree ^ n.<br/> +Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1.<br/> +Example tree_step (K : tree -> Type) :=<br/> + forall n st (t := node st) & forall i : 'I_n, K (st i), K t.<br/> +Example tree_rect K (Kstep : tree_step K) : forall t, K t.<br/> +Proof. by fix IHt 1 => -<span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode"><span class="id" title="var">st</span></span>; apply/Kstep=> i; apply: IHt. Defined.<br/> +<br/> +<span class="comment">(** An artificial example use of dependent functions. **)</span><br/> +Inductive tri_tree n := tri_row of {ffun forall i : 'I_n, tri_tree i}.<br/> +Fixpoint tri_size n (t : tri_tree n) :=<br/> + let: tri_row f := t in sumn <span class="inlinecode"><span class="id" title="var">seq</span></span> <span class="inlinecode"><span class="id" title="var">tri_size</span></span> <span class="inlinecode">(<span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">i</span>)</span> <span class="inlinecode">|</span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode">:</span> <span class="inlinecode">'<span class="id" title="var">I_n</span></span> + 1.<br/> +Example tri_tree_step (K : forall n, tri_tree n -> Type) :=<br/> + forall n st (t := tri_row st) & forall i : 'I_n, K i (st i), K n t.<br/> +Example tri_tree_rect K (Kstep : tri_tree_step K) : forall n t, K n t.<br/> +Proof. by fix IHt 2 => n <span class="inlinecode"><span class="id" title="var">st</span></span>; apply/Kstep=> i; apply: IHt. Defined.<br/> +Set Elimination Schemes.<br/> +<span class="comment">(** End example. *)</span> **)</span><br/> <br/> </div> <div class="doc"> - Helper for defining notation for function families. + The correspondance between finfun_of and CiC dependent functions. </div> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="DepPlainTheory"><span class="id" title="section">DepPlainTheory</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="DepPlainTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="DepPlainTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finPi"><span class="id" title="abbreviation">finPi</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="ffun0"><span class="id" title="lemma">ffun0</span></a> (<span class="id" title="var">aT0</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0) : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ffunE"><span class="id" title="lemma">ffunE</span></a> <span class="id" title="var">g</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ffunP"><span class="id" title="lemma">ffunP</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ffunK"><span class="id" title="lemma">ffunK</span></a> : @<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finPi"><span class="id" title="abbreviation">finPi</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_dffun"><span class="id" title="lemma">eq_dffun</span></a> (<span class="id" title="var">g1</span> <span class="id" title="var">g2</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g2"><span class="id" title="variable">g2</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g2"><span class="id" title="variable">g2</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="total_fun"><span class="id" title="definition">total_fun</span></a> <span class="id" title="var">g</span> <span class="id" title="var">x</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#Tagged"><span class="id" title="definition">Tagged</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="tfgraph"><span class="id" title="definition">tfgraph</span></a> <span class="id" title="var">f</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#codom_tuple"><span class="id" title="definition">codom_tuple</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#total_fun"><span class="id" title="definition">total_fun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="codom_tffun"><span class="id" title="lemma">codom_tffun</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#total_fun"><span class="id" title="definition">total_fun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#tfgraph"><span class="id" title="definition">tfgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>. <br/> + +<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="tfgraph_inj"><span class="id" title="lemma">tfgraph_inj</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#tfgraph"><span class="id" title="definition">tfgraph</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="family_mem"><span class="id" title="definition">family_mem</span></a> <span class="id" title="var">mF</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fbeb549dcb6350fb8ceb1bda39acce60"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fbeb549dcb6350fb8ceb1bda39acce60"><span class="id" title="notation">pred</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fbeb549dcb6350fb8ceb1bda39acce60"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fbeb549dcb6350fb8ceb1bda39acce60"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">∀</span></a> <span class="id" title="var">x</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#ce8c9a990e3e773a56ef37417d3761c6"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#fbeb549dcb6350fb8ceb1bda39acce60"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="DepPlainTheory.pT"><span class="id" title="variable">pT</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)) (<a name="DepPlainTheory.F"><span class="id" title="variable">F</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>).<br/> <br/> </div> <div class="doc"> - Lemmas on the correspondance between finfun_type and CiC functions. + Helper for defining notation for function families. </div> <div class="code"> -<span class="id" title="keyword">Section</span> <a name="PlainTheory"><span class="id" title="section">PlainTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Variables</span> (<a name="PlainTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="PlainTheory.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/> -<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> +<span class="id" title="keyword">Lemma</span> <a name="familyP"><span class="id" title="lemma">familyP</span></a> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory.F"><span class="id" title="variable">F</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#DepPlainTheory"><span class="id" title="section">DepPlainTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="tnth_fgraph"><span class="id" title="lemma">tnth_fgraph</span></a> <span class="id" title="var">f</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>).<br/> - +<span class="id" title="keyword">Notation</span> <a name="family"><span class="id" title="abbreviation">family</span></a> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>)).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="InheritedStructures"><span class="id" title="section">InheritedStructures</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="InheritedStructures.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="dffun_aT"><span class="id" title="abbreviation">dffun_aT</span></a> <span class="id" title="var">rT</span> <span class="id" title="var">rS</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">dffun</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT"><span class="id" title="variable">aT</span></a>, <span class="id" title="var">rT</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <span class="id" title="var">rS</span><a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> + <span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_eqType</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#eqMixin"><span class="id" title="lemma">eqMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>)).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dfinfun_eqType</span> <span class="id" title="var">rT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#dffun_aT"><span class="id" title="abbreviation">dffun_aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#eqMixin"><span class="id" title="lemma">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> + +<br/> + <span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_choiceType</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#choiceMixin"><span class="id" title="lemma">choiceMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>)).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dfinfun_choiceType</span> <span class="id" title="var">rT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#dffun_aT"><span class="id" title="abbreviation">dffun_aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#choiceMixin"><span class="id" title="lemma">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> + +<br/> + <span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_countType</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#countMixin"><span class="id" title="lemma">countMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>)).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dfinfun_countType</span> <span class="id" title="var">rT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#dffun_aT"><span class="id" title="abbreviation">dffun_aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#countMixin"><span class="id" title="lemma">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_finType</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finMixin"><span class="id" title="definition">finMixin</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">fun</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#94502d422d70bbaf4f390946d9885b7c"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>)).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">dfinfun_finType</span> <span class="id" title="var">rT</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#dffun_aT"><span class="id" title="abbreviation">dffun_aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#finMixin"><span class="id" title="definition">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#InheritedStructures"><span class="id" title="section">InheritedStructures</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="FunPlainTheory"><span class="id" title="section">FunPlainTheory</span></a>.<br/> + <br/> -<span class="id" title="keyword">Lemma</span> <a name="ffunE"><span class="id" title="lemma">ffunE</span></a> (<span class="id" title="var">g</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) : <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="FunPlainTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="FunPlainTheory.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="fgraph_codom"><span class="id" title="lemma">fgraph_codom</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#codom_tuple"><span class="id" title="definition">codom_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="fgraph"><span class="id" title="definition">fgraph</span></a> <span class="id" title="var">f</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#codom_tuple"><span class="id" title="definition">codom_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="codom_ffun"><span class="id" title="lemma">codom_ffun</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Finfun"><span class="id" title="definition">Finfun</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">ffun</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_rank"><span class="id" title="definition">enum_rank</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.ssreflect.finfun.html#486743bb05c6aa8b9d64fd3cec29ee79"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="tnth_fgraph"><span class="id" title="lemma">tnth_fgraph</span></a> <span class="id" title="var">f</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="ffunP"><span class="id" title="lemma">ffunP</span></a> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FinfunK"><span class="id" title="lemma">FinfunK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Finfun"><span class="id" title="definition">Finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="ffunK"><span class="id" title="lemma">ffunK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (@<a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="abbreviation">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> +<span class="id" title="keyword">Lemma</span> <a name="fgraphK"><span class="id" title="lemma">fgraphK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Finfun"><span class="id" title="definition">Finfun</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="family_mem"><span class="id" title="definition">family_mem</span></a> <span class="id" title="var">mF</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">pred</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">∀</span></a> <span class="id" title="var">x</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="fgraph_ffun0"><span class="id" title="lemma">fgraph_ffun0</span></a> <span class="id" title="var">aT0</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#ffun0"><span class="id" title="lemma">ffun0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT0"><span class="id" title="variable">aT0</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="codom_ffun"><span class="id" title="lemma">codom_ffun</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>. <br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="familyP"><span class="id" title="lemma">familyP</span></a> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) <span class="id" title="var">f</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a>)).<br/> +<span class="id" title="keyword">Lemma</span> <a name="tagged_tfgraph"><span class="id" title="lemma">tagged_tfgraph</span></a> <span class="id" title="var">f</span> : @<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#tagged"><span class="id" title="definition">tagged</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#tfgraph"><span class="id" title="definition">tfgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> <span class="id" title="var">mR</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.finfun.html#mR"><span class="id" title="variable">mR</span></a>).<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_ffun"><span class="id" title="lemma">eq_ffun</span></a> (<span class="id" title="var">g1</span> <span class="id" title="var">g2</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a>) : <a class="idref" href="mathcomp.ssreflect.finfun.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g2"><span class="id" title="variable">g2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g2"><span class="id" title="variable">g2</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="fgraph_codom"><span class="id" title="lemma">fgraph_codom</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#codom_tuple"><span class="id" title="definition">codom_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> (<span class="id" title="var">mR</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem_pred"><span class="id" title="inductive">mem_pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory.aT"><span class="id" title="variable">aT</span></a> ⇒ <a class="idref" href="mathcomp.ssreflect.finfun.html#mR"><span class="id" title="variable">mR</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="ffun_onP"><span class="id" title="lemma">ffun_onP</span></a> <span class="id" title="var">R</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/> +<span class="id" title="keyword">Lemma</span> <a name="ffun_onP"><span class="id" title="lemma">ffun_onP</span></a> <span class="id" title="var">R</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/> <br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory"><span class="id" title="section">PlainTheory</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunPlainTheory"><span class="id" title="section">FunPlainTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="family"><span class="id" title="abbreviation">family</span></a> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fun_of_simpl"><span class="id" title="definition">fun_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>))).<br/> -<span class="id" title="keyword">Notation</span> <a name="ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/> <br/> +<span class="id" title="keyword">Notation</span> <a name="ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="445fe95595384a6d39644c554d9b4997"><span class="id" title="notation">"</span></a>@ 'ffun_on' aT R" :=<br/> + (<a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#simpl_pred"><span class="id" title="definition">simpl_pred</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="inductive">finfun_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> (<span class="id" title="var">aT</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span>))))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 10, <span class="id" title="var">aT</span>, <span class="id" title="var">R</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 9).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="nth_fgraph_ord"><span class="id" title="lemma">nth_fgraph_ord</span></a> <span class="id" title="var">T</span> <span class="id" title="var">n</span> (<span class="id" title="var">x0</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a>) <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x0"><span class="id" title="variable">x0</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="nth_fgraph_ord"><span class="id" title="lemma">nth_fgraph_ord</span></a> <span class="id" title="var">T</span> <span class="id" title="var">n</span> (<span class="id" title="var">x0</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a>) <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x0"><span class="id" title="variable">x0</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Support"><span class="id" title="section">Support</span></a>.<br/> @@ -205,16 +353,16 @@ <span class="id" title="keyword">Variables</span> (<a name="Support.aT"><span class="id" title="variable">aT</span></a> : <span class="id" title="keyword">Type</span>) (<a name="Support.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="support_for"><span class="id" title="definition">support_for</span></a> <span class="id" title="var">y</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#Support.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Support.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="support_for"><span class="id" title="definition">support_for</span></a> <span class="id" title="var">y</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#Support.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Support.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="supportE"><span class="id" title="lemma">supportE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#support_for"><span class="id" title="definition">support_for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="supportE"><span class="id" title="lemma">supportE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#support_for"><span class="id" title="definition">support_for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>. <br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#Support"><span class="id" title="section">Support</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="5be79ec294433194842565db57cbc361"><span class="id" title="notation">"</span></a>y .-support" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#support_for"><span class="id" title="definition">support_for</span></a> <span class="id" title="var">y</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="698544468b858f103778b531f3023430"><span class="id" title="notation">"</span></a>y .-support" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#support_for"><span class="id" title="definition">support_for</span></a> <span class="id" title="var">y</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "y .-support") : <span class="id" title="var">fun_scope</span>.<br/> <br/> @@ -222,99 +370,79 @@ <br/> <span class="id" title="keyword">Variables</span> (<a name="EqTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="EqTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>).<br/> -<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">D</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">D</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>).<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="supportP"><span class="id" title="lemma">supportP</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">g</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="finfun_eqMixin"><span class="id" title="definition">finfun_eqMixin</span></a> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_eqMixin"><span class="id" title="definition">finfun_eqMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> <span class="id" title="var">mD</span> (<span class="id" title="var">mF</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem_pred"><span class="id" title="inductive">mem_pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#mD"><span class="id" title="variable">mD</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_of_simpl"><span class="id" title="definition">pred_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#pred1"><span class="id" title="definition">pred1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a name="pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> <span class="id" title="var">mD</span> (<span class="id" title="var">mF</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem_pred"><span class="id" title="inductive">mem_pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#mD"><span class="id" title="variable">mD</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred_of_simpl"><span class="id" title="definition">pred_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#pred1"><span class="id" title="definition">pred1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="pfamilyP"><span class="id" title="lemma">pfamilyP</span></a> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) <span class="id" title="var">y</span> <span class="id" title="var">D</span> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) <span class="id" title="var">f</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>)<br/> - (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a>)).<br/> +<span class="id" title="keyword">Lemma</span> <a name="pfamilyP"><span class="id" title="lemma">pfamilyP</span></a> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) <span class="id" title="var">y</span> <span class="id" title="var">D</span> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) <span class="id" title="var">f</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>)<br/> + (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a>)).<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <span class="id" title="var">y</span> <span class="id" title="var">mD</span> <span class="id" title="var">mR</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#mD"><span class="id" title="variable">mD</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.finfun.html#mR"><span class="id" title="variable">mR</span></a>).<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="pffun_onP"><span class="id" title="lemma">pffun_onP</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> <span class="id" title="var">f</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#image"><span class="id" title="abbreviation">image</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a>)<br/> - (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#698544468b858f103778b531f3023430"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#image"><span class="id" title="abbreviation">image</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a>)<br/> + (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory"><span class="id" title="section">EqTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="pfamily"><span class="id" title="abbreviation">pfamily</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fun_of_simpl"><span class="id" title="definition">fun_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>))).<br/> -<span class="id" title="keyword">Notation</span> <a name="pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="finfun_choiceMixin"><span class="id" title="definition">finfun_choiceMixin</span></a> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_choiceType</span> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_choiceMixin"><span class="id" title="definition">finfun_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_choiceType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="pfamily"><span class="id" title="abbreviation">pfamily</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="finfun_countMixin"><span class="id" title="definition">finfun_countMixin</span></a> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_countType</span> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_countMixin"><span class="id" title="definition">finfun_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_countType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subCountType</span> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subCountType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="FinDepTheory"><span class="id" title="section">FinDepTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Section</span> <a name="FinTheory"><span class="id" title="section">FinTheory</span></a>.<br/> +<span class="id" title="keyword">Variables</span> (<a name="FinDepTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="FinDepTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">dffun</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.aT"><span class="id" title="variable">aT</span></a>, <a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#15e3a46a8a60865a7b5408d87034cd4e"><span class="id" title="notation">}</span></a>.<br/> <br/> -<span class="id" title="keyword">Variables</span> <a name="FinTheory.aT"><span class="id" title="variable">aT</span></a> <a name="FinTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="ffT"><span class="id" title="abbreviation">ffT</span></a> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">D</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_family"><span class="id" title="lemma">card_family</span></a> (<span class="id" title="var">F</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)) :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#simpl_pred"><span class="id" title="definition">simpl_pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">)|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="finfun_finMixin"><span class="id" title="definition">finfun_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_finMixin"><span class="id" title="definition">finfun_finMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_finType"><span class="id" title="definition">finfun_finType</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/> - +<span class="id" title="keyword">Lemma</span> <a name="card_dep_ffun"><span class="id" title="lemma">card_dep_ffun</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#2ea807d068496425ebd93f2c454c8460"><span class="id" title="notation">]</span></a>.<br/> + <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_pfamily"><span class="id" title="lemma">card_pfamily</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">D</span> <span class="id" title="var">F</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily"><span class="id" title="abbreviation">pfamily</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinDepTheory"><span class="id" title="section">FinDepTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_family"><span class="id" title="lemma">card_family</span></a> <span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Section</span> <a name="FinFunTheory"><span class="id" title="section">FinFunTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_pffun_on"><span class="id" title="lemma">card_pffun_on</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> +<span class="id" title="keyword">Variables</span> <a name="FinFunTheory.aT"><span class="id" title="variable">aT</span></a> <a name="FinFunTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">D</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.rT"><span class="id" title="variable">rT</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_ffun_on"><span class="id" title="lemma">card_ffun_on</span></a> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_pfamily"><span class="id" title="lemma">card_pfamily</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">D</span> <span class="id" title="var">F</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily"><span class="id" title="abbreviation">pfamily</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#c3ff8d84d4e3e273bebfcf7502deb41a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#c3ff8d84d4e3e273bebfcf7502deb41a"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#c3ff8d84d4e3e273bebfcf7502deb41a"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#c3ff8d84d4e3e273bebfcf7502deb41a"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#c3ff8d84d4e3e273bebfcf7502deb41a"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_ffun"><span class="id" title="lemma">card_ffun</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> - +<span class="id" title="keyword">Lemma</span> <a name="card_pffun_on"><span class="id" title="lemma">card_pffun_on</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> + <br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory"><span class="id" title="section">FinTheory</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_ffun_on"><span class="id" title="lemma">card_ffun_on</span></a> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#445fe95595384a6d39644c554d9b4997"><span class="id" title="notation">@</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#445fe95595384a6d39644c554d9b4997"><span class="id" title="notation">ffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> <br/> +<span class="id" title="keyword">Lemma</span> <a name="card_ffun"><span class="id" title="lemma">card_ffun</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinFunTheory"><span class="id" title="section">FinFunTheory</span></a>.<br/> </div> </div> |