-
Notifications
You must be signed in to change notification settings - Fork 11
Expand file tree
/
Copy pathCombi.Combi.fibered_set.html
More file actions
141 lines (98 loc) · 30.7 KB
/
Copy pathCombi.Combi.fibered_set.html
File metadata and controls
141 lines (98 loc) · 30.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
<!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=iso-8859-1" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>Combi.Combi.fibered_set: Bijection beetween fibered sets</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Combi.Combi.fibered_set: Bijection beetween fibered sets</h1>
<div class="code">
</div>
<div class="doc">
</div>
<div class="code">
</div>
<div class="doc">
<a id="lab31"></a><h1 class="section">Bijection beetween fibered sets</h1>
<div class="paragraph"> </div>
Given a type with equality <span class="inlinecode"><span class="id" title="var">I</span></span> a fiberedset is a set <span class="inlinecode"><span class="id" title="var">fbset</span></span> in an ihnabited
fintype <span class="inlinecode"><span class="id" title="var">T</span></span> equiped with a function <span class="inlinecode"><span class="id" title="var">fbfun</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">fbset</span></span> <span class="inlinecode">-></span> <span class="inlinecode"><span class="id" title="var">I</span></span>. The preimage of some
<span class="inlinecode"><span class="id" title="var">i</span></span> under <span class="inlinecode"><span class="id" title="var">fbfun</span></span> is called the fiber of <span class="inlinecode"><span class="id" title="var">i</span></span>. The goal of this file is to show
that if two fibered set <span class="inlinecode"><span class="id" title="var">S1</span></span> <span class="inlinecode"><span class="id" title="var">S2</span></span> have their fiber of <span class="inlinecode"><span class="id" title="var">i</span></span> of the same
cardinality for all <span class="inlinecode"><span class="id" title="var">i</span></span>, then there there exists a bijection <span class="inlinecode"><span class="id" title="var">fbbij</span></span> from <span class="inlinecode"><span class="id" title="var">S1</span></span>
to <span class="inlinecode"><span class="id" title="var">S2</span></span> which sends the fiber of <span class="inlinecode"><span class="id" title="var">i</span></span> to the fiber of <span class="inlinecode"><span class="id" title="var">i</span></span>. That is <span class="inlinecode"><span class="id" title="var">fbbij</span></span>
commute with the <span class="inlinecode"><span class="id" title="var">fbfun</span></span> : <span class="inlinecode"><span class="id" title="keyword">forall</span></span> <span class="inlinecode"><span class="id" title="var">x</span>,</span> <span class="inlinecode"><span class="id" title="var">fbfun2</span></span> <span class="inlinecode">(<span class="id" title="var">fbbij</span></span> <span class="inlinecode"><span class="id" title="var">x</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">fbfun1</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span>.
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">fibered_set</span></span> == record for fibered sets on a carrier <span class="inlinecode"><span class="id" title="var">finType</span></span>
</li>
<li> <span class="inlinecode"><span class="id" title="var">fiber</span></span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> == the <span class="inlinecode"><span class="id" title="var">i</span></span>-fiber of <span class="inlinecode"><span class="id" title="var">S</span></span>
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" title="var">fbbij</span></span> <span class="inlinecode"><span class="id" title="var">U</span></span> <span class="inlinecode"><span class="id" title="var">V</span></span> == a bijection from <span class="inlinecode"><span class="id" title="var">U</span></span> to <span class="inlinecode"><span class="id" title="var">V</span></span> provided the two fibered sets
<span class="inlinecode"><span class="id" title="var">U</span></span> and <span class="inlinecode"><span class="id" title="var">V</span></span> have their fiber of <span class="inlinecode"><span class="id" title="var">i</span></span> of the same cardinality:
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" title="keyword">Hypothesis</span></span> <span class="inlinecode"><span class="id" title="var">HcardEq</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="keyword">forall</span></span> <span class="inlinecode"><span class="id" title="var">i</span>,</span> <span class="inlinecode">#|<span class="id" title="var">fiber</span></span> <span class="inlinecode"><span class="id" title="var">U</span></span> <span class="inlinecode"><span class="id" title="var">i</span>|</span> <span class="inlinecode">=</span> <span class="inlinecode">#|<span class="id" title="var">fiber</span></span> <span class="inlinecode"><span class="id" title="var">V</span></span> <span class="inlinecode"><span class="id" title="var">i</span>|.</span>
</li>
</ul>
<div class="paragraph"> </div>
</div>
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Corelib</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Setoids.Setoid.html#"><span class="id" title="library">Setoid</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">mathcomp</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">ssreflect</span> <span class="id" title="library">ssrfun</span> <span class="id" title="library">ssrbool</span> <span class="id" title="library">eqtype</span> <span class="id" title="library">ssrnat</span> <span class="id" title="library">seq</span> <span class="id" title="library">fintype</span> <span class="id" title="library">finset</span>.<br/>
<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a id="BijFiberedSet" class="idref" href="#BijFiberedSet"><span class="id" title="section">BijFiberedSet</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a id="BijFiberedSet.I" class="idref" href="#BijFiberedSet.I"><span class="id" title="variable">I</span></a> : <span class="id" title="abbreviation">eqType</span>.<br/>
<br/>
<span class="id" title="keyword">Record</span> <a id="fibered_set" class="idref" href="#fibered_set"><span class="id" title="record">fibered_set</span></a> := <span class="id" title="var">FiberedSet</span> {<br/>
<a id="carrier" class="idref" href="#carrier"><span class="id" title="projection">carrier</span></a> : <span class="id" title="abbreviation">finType</span>;<br/>
<a id="elt" class="idref" href="#elt"><span class="id" title="projection">elt</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#carrier:4"><span class="id" title="method">carrier</span></a>;<br/>
<a id="fbset" class="idref" href="#fbset"><span class="id" title="projection">fbset</span></a> :> <span class="id" title="notation">{</span><span class="id" title="notation">set</span> <a class="idref" href="Combi.Combi.fibered_set.html#carrier:4"><span class="id" title="method">carrier</span></a><span class="id" title="notation">}</span>;<br/>
<a id="fbfun" class="idref" href="#fbfun"><span class="id" title="projection">fbfun</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#carrier:4"><span class="id" title="method">carrier</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.I"><span class="id" title="variable">I</span></a> }.<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="fiber" class="idref" href="#fiber"><span class="id" title="definition">fiber</span></a> (<a id="S:8" class="idref" href="#S:8"><span class="id" title="binder">S</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#fibered_set"><span class="id" title="record">fibered_set</span></a>) <a id="v:9" class="idref" href="#v:9"><span class="id" title="binder">v</span></a> := <span class="id" title="notation">[</span><span class="id" title="notation">set</span> <a class="idref" href="Combi.Combi.fibered_set.html#x:10"><span class="id" title="variable">x</span></a> <span class="id" title="notation">|</span> <a id="x:10" class="idref" href="#x:10"><span class="id" title="binder"><span id="x:11" class="id"><span id="x:12" class="id"><span id="x:13" class="id">x</span></span></span></span></a> <span class="id" title="notation">in</span> <a class="idref" href="Combi.Combi.fibered_set.html#S:8"><span class="id" title="variable">S</span></a> <span class="id" title="notation">&</span> <a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:11"><span class="id" title="variable">x</span></a> <span class="id" title="notation">==</span> <a class="idref" href="Combi.Combi.fibered_set.html#v:9"><span class="id" title="variable">v</span></a><span class="id" title="notation">]</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="mem_fiber" class="idref" href="#mem_fiber"><span class="id" title="lemma">mem_fiber</span></a> (<a id="S:14" class="idref" href="#S:14"><span class="id" title="binder">S</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#fibered_set"><span class="id" title="record">fibered_set</span></a>) <a id="x:15" class="idref" href="#x:15"><span class="id" title="binder">x</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#x:15"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#S:14"><span class="id" title="variable">S</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:15"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#S:14"><span class="id" title="variable">S</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:15"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Definition</span> <a id="fbbij" class="idref" href="#fbbij"><span class="id" title="definition">fbbij</span></a> (<a id="U:16" class="idref" href="#U:16"><span class="id" title="binder">U</span></a> <a id="V:17" class="idref" href="#V:17"><span class="id" title="binder">V</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#fibered_set"><span class="id" title="record">fibered_set</span></a>) (<a id="x:18" class="idref" href="#x:18"><span class="id" title="binder">x</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#carrier"><span class="id" title="projection">carrier</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#U:16"><span class="id" title="variable">U</span></a>) : <a class="idref" href="Combi.Combi.fibered_set.html#carrier"><span class="id" title="projection">carrier</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:17"><span class="id" title="variable">V</span></a> :=<br/>
<span class="id" title="definition">nth</span> (<a class="idref" href="Combi.Combi.fibered_set.html#elt"><span class="id" title="projection">elt</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:17"><span class="id" title="variable">V</span></a>) (<span class="id" title="abbreviation">enum</span> (<a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:17"><span class="id" title="variable">V</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:18"><span class="id" title="variable">x</span></a>))) (<span class="id" title="definition">index</span> <a class="idref" href="Combi.Combi.fibered_set.html#x:18"><span class="id" title="variable">x</span></a> (<span class="id" title="abbreviation">enum</span> (<a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#U:16"><span class="id" title="variable">U</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:18"><span class="id" title="variable">x</span></a>)))).<br/>
<br/>
<span class="id" title="keyword">Section</span> <a id="BijFiberedSet.Defs" class="idref" href="#BijFiberedSet.Defs"><span class="id" title="section">Defs</span></a>.<br/>
<br/>
<span class="id" title="keyword">Variable</span> <a id="BijFiberedSet.Defs.U" class="idref" href="#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a> <a id="BijFiberedSet.Defs.V" class="idref" href="#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#fibered_set"><span class="id" title="record">fibered_set</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a id="BijFiberedSet.Defs.HcardEq" class="idref" href="#BijFiberedSet.Defs.HcardEq"><span class="id" title="variable">HcardEq</span></a> : <span class="id" title="keyword">forall</span> <a id="i:23" class="idref" href="#i:23"><span class="id" title="binder">i</span></a>, <span class="id" title="notation">#|</span><a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#i:23"><span class="id" title="variable">i</span></a><span class="id" title="notation">|</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">#|</span><a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#i:23"><span class="id" title="variable">i</span></a><span class="id" title="notation">|</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="fbbij_in_fiber" class="idref" href="#fbbij_in_fiber"><span class="id" title="lemma">fbbij_in_fiber</span></a> <a id="x:26" class="idref" href="#x:26"><span class="id" title="binder">x</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#x:26"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:26"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:26"><span class="id" title="variable">x</span></a>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="fbset_fbbij" class="idref" href="#fbset_fbbij"><span class="id" title="lemma">fbset_fbbij</span></a> <a id="x:27" class="idref" href="#x:27"><span class="id" title="binder">x</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#x:27"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:27"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="equi_fbbij" class="idref" href="#equi_fbbij"><span class="id" title="lemma">equi_fbbij</span></a> <a id="x:28" class="idref" href="#x:28"><span class="id" title="binder">x</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#x:28"><span class="id" title="variable">x</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:28"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:28"><span class="id" title="variable">x</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="fbbijK" class="idref" href="#fbbijK"><span class="id" title="lemma">fbbijK</span></a> : <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.V"><span class="id" title="variable">V</span></a>) (<a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs.U"><span class="id" title="variable">U</span></a>)<a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet.Defs"><span class="id" title="section">Defs</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="fbbijP" class="idref" href="#fbbijP"><span class="id" title="lemma">fbbijP</span></a> (<a id="U:29" class="idref" href="#U:29"><span class="id" title="binder">U</span></a> <a id="V:30" class="idref" href="#V:30"><span class="id" title="binder">V</span></a> : <a class="idref" href="Combi.Combi.fibered_set.html#fibered_set"><span class="id" title="record">fibered_set</span></a>) :<br/>
<a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">forall</span> <a id="i:31" class="idref" href="#i:31"><span class="id" title="binder">i</span></a>, <span class="id" title="notation">#|</span><a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#U:29"><span class="id" title="variable">U</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#i:31"><span class="id" title="variable">i</span></a><span class="id" title="notation">|</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="notation">#|</span><a class="idref" href="Combi.Combi.fibered_set.html#fiber"><span class="id" title="definition">fiber</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:30"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#i:31"><span class="id" title="variable">i</span></a><span class="id" title="notation">|</span><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#U:29"><span class="id" title="variable">U</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:30"><span class="id" title="variable">V</span></a>)<a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a><br/>
<span class="id" title="notation">[</span><span class="id" title="notation">set</span> <a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:30"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:32"><span class="id" title="variable">x</span></a> <span class="id" title="notation">|</span> <a id="x:32" class="idref" href="#x:32"><span class="id" title="binder">x</span></a> <span class="id" title="notation">in</span> <a class="idref" href="Combi.Combi.fibered_set.html#U:29"><span class="id" title="variable">U</span></a><span class="id" title="notation">]</span> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:30"><span class="id" title="variable">V</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a><br/>
<a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#U:29"><span class="id" title="variable">U</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">forall</span> <a id="x:33" class="idref" href="#x:33"><span class="id" title="binder">x</span></a>, <a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> (<a class="idref" href="Combi.Combi.fibered_set.html#fbbij"><span class="id" title="definition">fbbij</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#V:30"><span class="id" title="variable">V</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:33"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#fbfun"><span class="id" title="projection">fbfun</span></a> <a class="idref" href="Combi.Combi.fibered_set.html#x:33"><span class="id" title="variable">x</span></a><a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a> <a class="idref" href="http://rocq-prover.org/doc/V9.1.1/stdlib//Corelib.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Combi.Combi.fibered_set.html#BijFiberedSet"><span class="id" title="section">BijFiberedSet</span></a>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://rocq-prover.org/">coqdoc</a>
</div>
</div>
</body>
</html>