diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.ssreflect.finfun.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.ssreflect.finfun.html | 456 |
1 files changed, 0 insertions, 456 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.finfun.html b/docs/htmldoc/mathcomp.ssreflect.finfun.html deleted file mode 100644 index c0de196..0000000 --- a/docs/htmldoc/mathcomp.ssreflect.finfun.html +++ /dev/null @@ -1,456 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.ssreflect.finfun</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.ssreflect.finfun</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><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 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, 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) -> 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. - f \in pffun_on y D R == f is a y-partial function from D to R: - f has y-support D and f x \in R for all x \in D. - f \in pfamily y D F == f belongs to the y-partial family from D to F: - f has y-support D and f x \in F x for all x \in D. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<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> : <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_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/> - -<br/> - -<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">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">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/> - -<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="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="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="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="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="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="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="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"> - The correspondance between finfun_of and CiC dependent functions. -</div> -<div class="code"> -<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"> - Helper for defining notation for function families. -</div> -<div class="code"> - -<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/> - -<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">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">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">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="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="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">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="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">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/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#FunPlainTheory"><span class="id" title="section">FunPlainTheory</span></a>.<br/> - -<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#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/> - -<br/> -<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/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/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="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/> -<span class="id" title="keyword">Section</span> <a name="EqTheory"><span class="id" title="section">EqTheory</span></a>.<br/> - -<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#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/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/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/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/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/> - -<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">Section</span> <a name="FinDepTheory"><span class="id" title="section">FinDepTheory</span></a>.<br/> - -<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">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">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">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">Section</span> <a name="FinFunTheory"><span class="id" title="section">FinFunTheory</span></a>.<br/> - -<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_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_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">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> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |