generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.finfun.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 328 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.ssreflect.finfun.html b/docs/htmldoc/mathcomp.ssreflect.finfun.html
new file mode 100644
index 0000000..7af1bac
--- /dev/null
+++ b/docs/htmldoc/mathcomp.ssreflect.finfun.html
@@ -0,0 +1,328 @@
+<!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">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This file implements a type for functions with a finite domain:            
+    {ffun aT -&gt; rT} where aT should have a finType structure.               
+ Any eqType, choiceType, countType and finType structures on rT extend to   
+ {ffun aT -&gt; rT} as Leibnitz equality and extensional equalities coincide.  
+     (T ^ n)%type is notation for {ffun 'I_n -&gt; T}, which is isomorphic     
+                     to n.-tuple T.                                         
+  For f : {ffun aT -&gt; rT}, we define                                        
+              f x == the image of x under f (f coerces to a CiC function)   
+         fgraph f == the graph of f, i.e., the #|aT|.-tuple rT of the       
+                     values of f over enum aT.                              
+       finfun lam == the f such that f =1 lam; this is the RECOMMENDED      
+                     interface to build an element of {ffun aT -&gt; rT}.      
+ [ffun x =&gt; expr] == finfun (fun x =&gt; expr)                                 
+   [ffun =&gt; expr] == finfun (fun _ =&gt; expr)                                 
+  f \in ffun_on R == the range of f is a subset of R                        
+   f \in family F == f belongs to the family F (f x \in F x for all x)      
+     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> : <span class="id" title="keyword">Type</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Inductive</span> <a name="finfun_type"><span class="id" title="inductive">finfun_type</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> := <a name="Finfun"><span class="id" title="constructor">Finfun</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finfun_of"><span class="id" title="definition">finfun_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#Def.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_of_finfun</span> : <span class="id" title="var">finfun_of</span> &gt;-&gt; <span class="id" title="var">finfun_type</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="fgraph"><span class="id" title="definition">fgraph</span></a> <span class="id" title="var">f</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.ssreflect.finfun.html#Finfun"><span class="id" title="constructor">Finfun</span></a> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">t</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">newType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#Def"><span class="id" title="section">Def</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">&quot;</span></a>{ 'ffun' fT }" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="definition">finfun_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">fT</span>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'ffun'  '[hv' fT ']' }") : <span class="id" title="var">type_scope</span>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.ssreflect.fintype.html#ordinal_finType"><span class="id" title="definition">ordinal_finType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#n"><span class="id" title="variable">n</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="cd1bca6dfdb74a6b15c6c8969f27472a"><span class="id" title="notation">&quot;</span></a>T ^ n" := (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_of"><span class="id" title="definition">finfun_of</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#exp_finIndexType"><span class="id" title="definition">exp_finIndexType</span></a> <span class="id" title="var">n</span>) <span class="id" title="var">T</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">_</span>)) : <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/>
+<span class="id" title="keyword">Parameter</span> <a name="FunFinfunSig.fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>.<br/>
+<span class="id" title="keyword">Parameter</span> <a name="FunFinfunSig.finfun"><span class="id" title="axiom">finfun</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) <span class="id" title="var">rT</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Axiom</span> <a name="FunFinfunSig.fun_of_finE"><span class="id" title="axiom">fun_of_finE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig.fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>.<br/>
+<span class="id" title="keyword">Axiom</span> <a name="FunFinfunSig.finfunE"><span class="id" title="axiom">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig.finfun"><span class="id" title="axiom">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Module</span> <a name="FunFinfun"><span class="id" title="module">FunFinfun</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfunSig"><span class="id" title="module">FunFinfunSig</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="FunFinfun.fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="FunFinfun.finfun"><span class="id" title="definition">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="FunFinfun.fun_of_finE"><span class="id" title="lemma">fun_of_finE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun.fun_of_fin"><span class="id" title="definition">fun_of_fin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin_def"><span class="id" title="abbreviation">fun_of_fin_def</span></a>.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="FunFinfun.finfunE"><span class="id" title="lemma">finfunE</span></a> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun.finfun"><span class="id" title="definition">finfun</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_def"><span class="id" title="abbreviation">finfun_def</span></a>.  <br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FunFinfun"><span class="id" title="module">FunFinfun</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="fun_of_fin"><span class="id" title="abbreviation">fun_of_fin</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">FunFinfun.fun_of_fin</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="finfun"><span class="id" title="abbreviation">finfun</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="axiom">FunFinfun.finfun</span></a>.<br/>
+<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="axiom">Funclass</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fun_of_fin_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_finE"><span class="id" title="axiom">FunFinfun.fun_of_finE</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfunE"><span class="id" title="axiom">FunFinfun.finfunE</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">&quot;</span></a>[ 'ffun' x : aT =&gt; F ]" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <span class="id" title="var">aT</span> ⇒ <span class="id" title="var">F</span>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">ident</span>, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">&quot;</span></a>[ 'ffun' : aT =&gt; F ]" := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> : <span class="id" title="var">aT</span> ⇒ <span class="id" title="var">F</span>))<br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">fun_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="71fbd02a8ba525d8dcd88d59800c905e"><span class="id" title="notation">&quot;</span></a>[ 'ffun' x =&gt; F ]" := <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">ffun</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">:</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">F</span><a class="idref" href="mathcomp.ssreflect.finfun.html#42aa76d2f66b49268bafac6d56a51249"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;(<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  =&gt;  F ]") : <span class="id" title="var">fun_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="ce31ffdcdad2ff7a7492eb6a19fd59e9"><span class="id" title="notation">&quot;</span></a>[ 'ffun' =&gt; F ]" := <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">:</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">F</span><a class="idref" href="mathcomp.ssreflect.finfun.html#e62970ec167bfaf02a37fd9fda643a97"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'ffun' =&gt;  F ]") : <span class="id" title="var">fun_scope</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Helper for defining notation for function families.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Lemmas on the correspondance between finfun_type and CiC functions.  
+</div>
+<div class="code">
+<span class="id" title="keyword">Section</span> <a name="PlainTheory"><span class="id" title="section">PlainTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="PlainTheory.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="PlainTheory.rT"><span class="id" title="variable">rT</span></a> : <span class="id" title="keyword">Type</span>).<br/>
+<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="tnth_fgraph"><span class="id" title="lemma">tnth_fgraph</span></a> <span class="id" title="var">f</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffunE"><span class="id" title="lemma">ffunE</span></a> (<span class="id" title="var">g</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) : <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="fgraph_codom"><span class="id" title="lemma">fgraph_codom</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#codom_tuple"><span class="id" title="definition">codom_tuple</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="codom_ffun"><span class="id" title="lemma">codom_ffun</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffunP"><span class="id" title="lemma">ffunP</span></a> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f2"><span class="id" title="variable">f2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffunK"><span class="id" title="lemma">ffunK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (@<a class="idref" href="mathcomp.ssreflect.finfun.html#fun_of_fin"><span class="id" title="abbreviation">fun_of_fin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) (@<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="family_mem"><span class="id" title="definition">family_mem</span></a> <span class="id" title="var">mF</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">pred</span></a> <span class="id" title="var">f</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">∀</span></a> <span class="id" title="var">x</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#6f09da91da7950fd65c31195ac4a5d3e"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ba4e2de877832f7c061554da0cb06dd3"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="familyP"><span class="id" title="lemma">familyP</span></a> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) <span class="id" title="var">f</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a>)).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> <span class="id" title="var">mR</span> := <a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.finfun.html#mR"><span class="id" title="variable">mR</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="ffun_onP"><span class="id" title="lemma">ffun_onP</span></a> <span class="id" title="var">R</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#PlainTheory"><span class="id" title="section">PlainTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="family"><span class="id" title="abbreviation">family</span></a> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#family_mem"><span class="id" title="definition">family_mem</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fun_of_simpl"><span class="id" title="definition">fun_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>))).<br/>
+<span class="id" title="keyword">Notation</span> <a name="ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on_mem"><span class="id" title="definition">ffun_on_mem</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="nth_fgraph_ord"><span class="id" title="lemma">nth_fgraph_ord</span></a> <span class="id" title="var">T</span> <span class="id" title="var">n</span> (<span class="id" title="var">x0</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_n</span></a>) <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x0"><span class="id" title="variable">x0</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fgraph"><span class="id" title="definition">fgraph</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a>) <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>.<br/>
+
+<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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#Support.rT"><span class="id" title="variable">rT</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="supportE"><span class="id" title="lemma">supportE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">f</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#support_for"><span class="id" title="definition">support_for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.  <br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#Support"><span class="id" title="section">Support</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="5be79ec294433194842565db57cbc361"><span class="id" title="notation">&quot;</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/>
+&nbsp;&nbsp;(<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#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">y</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">D</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a>).<br/>
+
+<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/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finfun_eqMixin"><span class="id" title="definition">finfun_eqMixin</span></a> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_eqMixin"><span class="id" title="definition">finfun_eqMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> <span class="id" title="var">mD</span> (<span class="id" title="var">mF</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem_pred"><span class="id" title="inductive">mem_pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in_mem"><span class="id" title="definition">in_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#mD"><span class="id" title="variable">mD</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_of_simpl"><span class="id" title="definition">pred_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#mF"><span class="id" title="variable">mF</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#pred1"><span class="id" title="definition">pred1</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="pfamilyP"><span class="id" title="lemma">pfamilyP</span></a> (<span class="id" title="var">pT</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#predType"><span class="id" title="record">predType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.rT"><span class="id" title="variable">rT</span></a>) <span class="id" title="var">y</span> <span class="id" title="var">D</span> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pT"><span class="id" title="variable">pT</span></a>) <span class="id" title="var">f</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a>)).<br/>
+
+<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/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#5be79ec294433194842565db57cbc361"><span class="id" title="notation">support</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#image"><span class="id" title="abbreviation">image</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.ssreflect.finfun.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y"><span class="id" title="variable">y</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#EqTheory"><span class="id" title="section">EqTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="pfamily"><span class="id" title="abbreviation">pfamily</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">F</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily_mem"><span class="id" title="definition">pfamily_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#fun_of_simpl"><span class="id" title="definition">fun_of_simpl</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#fmem"><span class="id" title="definition">fmem</span></a> <span class="id" title="var">F</span>))).<br/>
+<span class="id" title="keyword">Notation</span> <a name="pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <span class="id" title="var">y</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on_mem"><span class="id" title="definition">pffun_on_mem</span></a> <span class="id" title="var">y</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">D</span>) (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> <span class="id" title="var">R</span>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finfun_choiceMixin"><span class="id" title="definition">finfun_choiceMixin</span></a> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_choiceType</span> <span class="id" title="var">aT</span> <span class="id" title="var">rT</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_choiceMixin"><span class="id" title="definition">finfun_choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_choiceType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.choiceType"><span class="id" title="abbreviation">choiceType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finfun_countMixin"><span class="id" title="definition">finfun_countMixin</span></a> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_countType</span> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_countMixin"><span class="id" title="definition">finfun_countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a>).<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_countType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#be2fb44e85835140c455bc256ce18d4c"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subCountType</span> <span class="id" title="var">aT</span> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subCountType</span> (<span class="id" title="var">aT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.countType"><span class="id" title="abbreviation">countType</span></a>) :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="FinTheory"><span class="id" title="section">FinTheory</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> <a name="FinTheory.aT"><span class="id" title="variable">aT</span></a> <a name="FinTheory.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="fT"><span class="id" title="abbreviation">fT</span></a> := <a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#9f24a6f16bf73832c2d9aa4e2c16f692"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="ffT"><span class="id" title="abbreviation">ffT</span></a> := (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_type"><span class="id" title="inductive">finfun_type</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">D</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>) (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="finfun_finMixin"><span class="id" title="definition">finfun_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_finMixin"><span class="id" title="definition">finfun_finMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#ffT"><span class="id" title="abbreviation">ffT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#finfun_finType"><span class="id" title="definition">finfun_finType</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8adb1b225d027f6dfac99128a373179e"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">finfun_of_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+
+<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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pfamily"><span class="id" title="abbreviation">pfamily</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fb029fd23b6fc39e014fe7658d797041"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_family"><span class="id" title="lemma">card_family</span></a> <span class="id" title="var">F</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#family"><span class="id" title="abbreviation">family</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#foldr"><span class="id" title="definition">foldr</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#muln"><span class="id" title="definition">muln</span></a> 1 <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">seq</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#76a709b85ab118a35d217f357d4e8877"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_pffun_on"><span class="id" title="lemma">card_pffun_on</span></a> <span class="id" title="var">y0</span> <span class="id" title="var">D</span> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#pffun_on"><span class="id" title="abbreviation">pffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#y0"><span class="id" title="variable">y0</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#D"><span class="id" title="variable">D</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_ffun_on"><span class="id" title="lemma">card_ffun_on</span></a> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#ffun_on"><span class="id" title="abbreviation">ffun_on</span></a> <a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="card_ffun"><span class="id" title="lemma">card_ffun</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#fT"><span class="id" title="abbreviation">fT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.ssreflect.finfun.html#FinTheory"><span class="id" title="section">FinTheory</span></a>.<br/>
+
+<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
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.ssreflect.finfun.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)